DL008B

matrix_integer_alternating_prefix_balance

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Every actual alternating-product stream respects integer equality, including all decoded input and output streams and the parity-correct product rule.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded first-order arithmetic statement

forall ab ac bb bc cb cc db dc eb ec fb fc gb gc hb hc ub uc vb vc Ub Uc Vb Vc l. (forall ics_index_prefix_rows_equal ics_value0_prefix_rows_equal ics_value1_prefix_rows_equal ics_value2_prefix_rows_equal ics_value3_prefix_rows_equal. (exists ics_gap_prefix_rows_equal_bound. ics_gap_prefix_rows_equal_bound + S (ics_index_prefix_rows_equal) = (l)) -> (((exists fs_h_ics_prefix_rows_equal_at0. fs_h_ics_prefix_rows_equal_at0 + S (ics_value0_prefix_rows_equal) = S ((S (ics_index_prefix_rows_equal)) * ac)) /\ exists fs_q_ics_prefix_rows_equal_at0. ab = fs_q_ics_prefix_rows_equal_at0 * S ((S (ics_index_prefix_rows_equal)) * ac) + (ics_value0_prefix_rows_equal))) -> (((exists fs_h_ics_prefix_rows_equal_at1. fs_h_ics_prefix_rows_equal_at1 + S (ics_value1_prefix_rows_equal) = S ((S (ics_index_prefix_rows_equal)) * bc)) /\ exists fs_q_ics_prefix_rows_equal_at1. bb = fs_q_ics_prefix_rows_equal_at1 * S ((S (ics_index_prefix_rows_equal)) * bc) + (ics_value1_prefix_rows_equal))) -> (((exists fs_h_ics_prefix_rows_equal_at2. fs_h_ics_prefix_rows_equal_at2 + S (ics_value2_prefix_rows_equal) = S ((S (ics_index_prefix_rows_equal)) * ec)) /\ exists fs_q_ics_prefix_rows_equal_at2. eb = fs_q_ics_prefix_rows_equal_at2 * S ((S (ics_index_prefix_rows_equal)) * ec) + (ics_value2_prefix_rows_equal))) -> (((exists fs_h_ics_prefix_rows_equal_at3. fs_h_ics_prefix_rows_equal_at3 + S (ics_value3_prefix_rows_equal) = S ((S (ics_index_prefix_rows_equal)) * fc)) /\ exists fs_q_ics_prefix_rows_equal_at3. fb = fs_q_ics_prefix_rows_equal_at3 * S ((S (ics_index_prefix_rows_equal)) * fc) + (ics_value3_prefix_rows_equal))) -> ics_value0_prefix_rows_equal + ics_value3_prefix_rows_equal = ics_value2_prefix_rows_equal + ics_value1_prefix_rows_equal) -> (forall ics_index_prefix_cofactors_equal ics_value0_prefix_cofactors_equal ics_value1_prefix_cofactors_equal ics_value2_prefix_cofactors_equal ics_value3_prefix_cofactors_equal. (exists ics_gap_prefix_cofactors_equal_bound. ics_gap_prefix_cofactors_equal_bound + S (ics_index_prefix_cofactors_equal) = (l)) -> (((exists fs_h_ics_prefix_cofactors_equal_at0. fs_h_ics_prefix_cofactors_equal_at0 + S (ics_value0_prefix_cofactors_equal) = S ((S (ics_index_prefix_cofactors_equal)) * cc)) /\ exists fs_q_ics_prefix_cofactors_equal_at0. cb = fs_q_ics_prefix_cofactors_equal_at0 * S ((S (ics_index_prefix_cofactors_equal)) * cc) + (ics_value0_prefix_cofactors_equal))) -> (((exists fs_h_ics_prefix_cofactors_equal_at1. fs_h_ics_prefix_cofactors_equal_at1 + S (ics_value1_prefix_cofactors_equal) = S ((S (ics_index_prefix_cofactors_equal)) * dc)) /\ exists fs_q_ics_prefix_cofactors_equal_at1. db = fs_q_ics_prefix_cofactors_equal_at1 * S ((S (ics_index_prefix_cofactors_equal)) * dc) + (ics_value1_prefix_cofactors_equal))) -> (((exists fs_h_ics_prefix_cofactors_equal_at2. fs_h_ics_prefix_cofactors_equal_at2 + S (ics_value2_prefix_cofactors_equal) = S ((S (ics_index_prefix_cofactors_equal)) * gc)) /\ exists fs_q_ics_prefix_cofactors_equal_at2. gb = fs_q_ics_prefix_cofactors_equal_at2 * S ((S (ics_index_prefix_cofactors_equal)) * gc) + (ics_value2_prefix_cofactors_equal))) -> (((exists fs_h_ics_prefix_cofactors_equal_at3. fs_h_ics_prefix_cofactors_equal_at3 + S (ics_value3_prefix_cofactors_equal) = S ((S (ics_index_prefix_cofactors_equal)) * hc)) /\ exists fs_q_ics_prefix_cofactors_equal_at3. hb = fs_q_ics_prefix_cofactors_equal_at3 * S ((S (ics_index_prefix_cofactors_equal)) * hc) + (ics_value3_prefix_cofactors_equal))) -> ics_value0_prefix_cofactors_equal + ics_value3_prefix_cofactors_equal = ics_value2_prefix_cofactors_equal + ics_value1_prefix_cofactors_equal) -> (forall ff_index_mce_alternating_integer_prefix_first. (exists ff_gap_mce_integer_prefix_first_index. ff_gap_mce_integer_prefix_first_index + S (ff_index_mce_alternating_integer_prefix_first) = (l)) -> exists ff_ap_mce_alternating_integer_prefix_first ff_an_mce_alternating_integer_prefix_first ff_bp_mce_alternating_integer_prefix_first ff_bn_mce_alternating_integer_prefix_first ff_p_mce_alternating_integer_prefix_first ff_n_mce_alternating_integer_prefix_first. ((((exists ff_h_mce_integer_prefix_first_ap. ff_h_mce_integer_prefix_first_ap + S (ff_ap_mce_alternating_integer_prefix_first) = S ((S (ff_index_mce_alternating_integer_prefix_first)) * ac)) /\ exists ff_q_mce_integer_prefix_first_ap. ab = ff_q_mce_integer_prefix_first_ap * S ((S (ff_index_mce_alternating_integer_prefix_first)) * ac) + (ff_ap_mce_alternating_integer_prefix_first))) /\ ((((exists ff_h_mce_integer_prefix_first_an. ff_h_mce_integer_prefix_first_an + S (ff_an_mce_alternating_integer_prefix_first) = S ((S (ff_index_mce_alternating_integer_prefix_first)) * bc)) /\ exists ff_q_mce_integer_prefix_first_an. bb = ff_q_mce_integer_prefix_first_an * S ((S (ff_index_mce_alternating_integer_prefix_first)) * bc) + (ff_an_mce_alternating_integer_prefix_first))) /\ ((((exists ff_h_mce_integer_prefix_first_bp. ff_h_mce_integer_prefix_first_bp + S (ff_bp_mce_alternating_integer_prefix_first) = S ((S (ff_index_mce_alternating_integer_prefix_first)) * cc)) /\ exists ff_q_mce_integer_prefix_first_bp. cb = ff_q_mce_integer_prefix_first_bp * S ((S (ff_index_mce_alternating_integer_prefix_first)) * cc) + (ff_bp_mce_alternating_integer_prefix_first))) /\ ((((exists ff_h_mce_integer_prefix_first_bn. ff_h_mce_integer_prefix_first_bn + S (ff_bn_mce_alternating_integer_prefix_first) = S ((S (ff_index_mce_alternating_integer_prefix_first)) * dc)) /\ exists ff_q_mce_integer_prefix_first_bn. db = ff_q_mce_integer_prefix_first_bn * S ((S (ff_index_mce_alternating_integer_prefix_first)) * dc) + (ff_bn_mce_alternating_integer_prefix_first))) /\ ((((exists ff_h_mce_integer_prefix_first_positive. ff_h_mce_integer_prefix_first_positive + S (ff_p_mce_alternating_integer_prefix_first) = S ((S (ff_index_mce_alternating_integer_prefix_first)) * uc)) /\ exists ff_q_mce_integer_prefix_first_positive. ub = ff_q_mce_integer_prefix_first_positive * S ((S (ff_index_mce_alternating_integer_prefix_first)) * uc) + (ff_p_mce_alternating_integer_prefix_first))) /\ ((((exists ff_h_mce_integer_prefix_first_negative. ff_h_mce_integer_prefix_first_negative + S (ff_n_mce_alternating_integer_prefix_first) = S ((S (ff_index_mce_alternating_integer_prefix_first)) * vc)) /\ exists ff_q_mce_integer_prefix_first_negative. vb = ff_q_mce_integer_prefix_first_negative * S ((S (ff_index_mce_alternating_integer_prefix_first)) * vc) + (ff_n_mce_alternating_integer_prefix_first))) /\ (((exists ff_even_mce_term_integer_prefix_first_term. ff_index_mce_alternating_integer_prefix_first = 2 * ff_even_mce_term_integer_prefix_first_term) /\ (ff_p_mce_alternating_integer_prefix_first = (ff_ap_mce_alternating_integer_prefix_first) * (ff_bp_mce_alternating_integer_prefix_first) + (ff_an_mce_alternating_integer_prefix_first) * (ff_bn_mce_alternating_integer_prefix_first) /\ ff_n_mce_alternating_integer_prefix_first = (ff_ap_mce_alternating_integer_prefix_first) * (ff_bn_mce_alternating_integer_prefix_first) + (ff_an_mce_alternating_integer_prefix_first) * (ff_bp_mce_alternating_integer_prefix_first))) \/ ((exists ff_odd_mce_term_integer_prefix_first_term. ff_index_mce_alternating_integer_prefix_first = 2 * ff_odd_mce_term_integer_prefix_first_term + 1) /\ (ff_p_mce_alternating_integer_prefix_first = (ff_ap_mce_alternating_integer_prefix_first) * (ff_bn_mce_alternating_integer_prefix_first) + (ff_an_mce_alternating_integer_prefix_first) * (ff_bp_mce_alternating_integer_prefix_first) /\ ff_n_mce_alternating_integer_prefix_first = (ff_ap_mce_alternating_integer_prefix_first) * (ff_bp_mce_alternating_integer_prefix_first) + (ff_an_mce_alternating_integer_prefix_first) * (ff_bn_mce_alternating_integer_prefix_first))))))))))) -> (forall ff_index_mce_alternating_integer_prefix_second. (exists ff_gap_mce_integer_prefix_second_index. ff_gap_mce_integer_prefix_second_index + S (ff_index_mce_alternating_integer_prefix_second) = (l)) -> exists ff_ap_mce_alternating_integer_prefix_second ff_an_mce_alternating_integer_prefix_second ff_bp_mce_alternating_integer_prefix_second ff_bn_mce_alternating_integer_prefix_second ff_p_mce_alternating_integer_prefix_second ff_n_mce_alternating_integer_prefix_second. ((((exists ff_h_mce_integer_prefix_second_ap. ff_h_mce_integer_prefix_second_ap + S (ff_ap_mce_alternating_integer_prefix_second) = S ((S (ff_index_mce_alternating_integer_prefix_second)) * ec)) /\ exists ff_q_mce_integer_prefix_second_ap. eb = ff_q_mce_integer_prefix_second_ap * S ((S (ff_index_mce_alternating_integer_prefix_second)) * ec) + (ff_ap_mce_alternating_integer_prefix_second))) /\ ((((exists ff_h_mce_integer_prefix_second_an. ff_h_mce_integer_prefix_second_an + S (ff_an_mce_alternating_integer_prefix_second) = S ((S (ff_index_mce_alternating_integer_prefix_second)) * fc)) /\ exists ff_q_mce_integer_prefix_second_an. fb = ff_q_mce_integer_prefix_second_an * S ((S (ff_index_mce_alternating_integer_prefix_second)) * fc) + (ff_an_mce_alternating_integer_prefix_second))) /\ ((((exists ff_h_mce_integer_prefix_second_bp. ff_h_mce_integer_prefix_second_bp + S (ff_bp_mce_alternating_integer_prefix_second) = S ((S (ff_index_mce_alternating_integer_prefix_second)) * gc)) /\ exists ff_q_mce_integer_prefix_second_bp. gb = ff_q_mce_integer_prefix_second_bp * S ((S (ff_index_mce_alternating_integer_prefix_second)) * gc) + (ff_bp_mce_alternating_integer_prefix_second))) /\ ((((exists ff_h_mce_integer_prefix_second_bn. ff_h_mce_integer_prefix_second_bn + S (ff_bn_mce_alternating_integer_prefix_second) = S ((S (ff_index_mce_alternating_integer_prefix_second)) * hc)) /\ exists ff_q_mce_integer_prefix_second_bn. hb = ff_q_mce_integer_prefix_second_bn * S ((S (ff_index_mce_alternating_integer_prefix_second)) * hc) + (ff_bn_mce_alternating_integer_prefix_second))) /\ ((((exists ff_h_mce_integer_prefix_second_positive. ff_h_mce_integer_prefix_second_positive + S (ff_p_mce_alternating_integer_prefix_second) = S ((S (ff_index_mce_alternating_integer_prefix_second)) * Uc)) /\ exists ff_q_mce_integer_prefix_second_positive. Ub = ff_q_mce_integer_prefix_second_positive * S ((S (ff_index_mce_alternating_integer_prefix_second)) * Uc) + (ff_p_mce_alternating_integer_prefix_second))) /\ ((((exists ff_h_mce_integer_prefix_second_negative. ff_h_mce_integer_prefix_second_negative + S (ff_n_mce_alternating_integer_prefix_second) = S ((S (ff_index_mce_alternating_integer_prefix_second)) * Vc)) /\ exists ff_q_mce_integer_prefix_second_negative. Vb = ff_q_mce_integer_prefix_second_negative * S ((S (ff_index_mce_alternating_integer_prefix_second)) * Vc) + (ff_n_mce_alternating_integer_prefix_second))) /\ (((exists ff_even_mce_term_integer_prefix_second_term. ff_index_mce_alternating_integer_prefix_second = 2 * ff_even_mce_term_integer_prefix_second_term) /\ (ff_p_mce_alternating_integer_prefix_second = (ff_ap_mce_alternating_integer_prefix_second) * (ff_bp_mce_alternating_integer_prefix_second) + (ff_an_mce_alternating_integer_prefix_second) * (ff_bn_mce_alternating_integer_prefix_second) /\ ff_n_mce_alternating_integer_prefix_second = (ff_ap_mce_alternating_integer_prefix_second) * (ff_bn_mce_alternating_integer_prefix_second) + (ff_an_mce_alternating_integer_prefix_second) * (ff_bp_mce_alternating_integer_prefix_second))) \/ ((exists ff_odd_mce_term_integer_prefix_second_term. ff_index_mce_alternating_integer_prefix_second = 2 * ff_odd_mce_term_integer_prefix_second_term + 1) /\ (ff_p_mce_alternating_integer_prefix_second = (ff_ap_mce_alternating_integer_prefix_second) * (ff_bn_mce_alternating_integer_prefix_second) + (ff_an_mce_alternating_integer_prefix_second) * (ff_bp_mce_alternating_integer_prefix_second) /\ ff_n_mce_alternating_integer_prefix_second = (ff_ap_mce_alternating_integer_prefix_second) * (ff_bp_mce_alternating_integer_prefix_second) + (ff_an_mce_alternating_integer_prefix_second) * (ff_bn_mce_alternating_integer_prefix_second))))))))))) -> (forall ics_index_prefix_outputs_equal ics_value0_prefix_outputs_equal ics_value1_prefix_outputs_equal ics_value2_prefix_outputs_equal ics_value3_prefix_outputs_equal. (exists ics_gap_prefix_outputs_equal_bound. ics_gap_prefix_outputs_equal_bound + S (ics_index_prefix_outputs_equal) = (l)) -> (((exists fs_h_ics_prefix_outputs_equal_at0. fs_h_ics_prefix_outputs_equal_at0 + S (ics_value0_prefix_outputs_equal) = S ((S (ics_index_prefix_outputs_equal)) * uc)) /\ exists fs_q_ics_prefix_outputs_equal_at0. ub = fs_q_ics_prefix_outputs_equal_at0 * S ((S (ics_index_prefix_outputs_equal)) * uc) + (ics_value0_prefix_outputs_equal))) -> (((exists fs_h_ics_prefix_outputs_equal_at1. fs_h_ics_prefix_outputs_equal_at1 + S (ics_value1_prefix_outputs_equal) = S ((S (ics_index_prefix_outputs_equal)) * vc)) /\ exists fs_q_ics_prefix_outputs_equal_at1. vb = fs_q_ics_prefix_outputs_equal_at1 * S ((S (ics_index_prefix_outputs_equal)) * vc) + (ics_value1_prefix_outputs_equal))) -> (((exists fs_h_ics_prefix_outputs_equal_at2. fs_h_ics_prefix_outputs_equal_at2 + S (ics_value2_prefix_outputs_equal) = S ((S (ics_index_prefix_outputs_equal)) * Uc)) /\ exists fs_q_ics_prefix_outputs_equal_at2. Ub = fs_q_ics_prefix_outputs_equal_at2 * S ((S (ics_index_prefix_outputs_equal)) * Uc) + (ics_value2_prefix_outputs_equal))) -> (((exists fs_h_ics_prefix_outputs_equal_at3. fs_h_ics_prefix_outputs_equal_at3 + S (ics_value3_prefix_outputs_equal) = S ((S (ics_index_prefix_outputs_equal)) * Vc)) /\ exists fs_q_ics_prefix_outputs_equal_at3. Vb = fs_q_ics_prefix_outputs_equal_at3 * S ((S (ics_index_prefix_outputs_equal)) * Vc) + (ics_value3_prefix_outputs_equal))) -> ics_value0_prefix_outputs_equal + ics_value3_prefix_outputs_equal = ics_value2_prefix_outputs_equal + ics_value1_prefix_outputs_equal)

Constructive proof overview

Generated structural guide

Every actual alternating-product stream respects integer equality, including all decoded input and output streams and the parity-correct product rule.

The unchanged tactic script uses 2 declared prerequisites and contains 151 exact native proof lines.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

DL0089 matrix_integer_cofactor_term_balance beta_at_unique Stable theorem; checked-use authorized

Direct dependents

DL008C matrix_integer_cofactor_fold_balance

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

151 script commands · 20 reading checkpoints · 7 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (1)
matrix integer cofactor term balance

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro ab
  2. L2
    intro ac
  3. L3
    intro bb
  4. L4
    intro bc
  5. L5
    intro cb
  6. L6
    intro cc
  7. L7
    intro db
  8. L8
    intro dc
  9. L9
    intro eb
  10. L10
    intro ec
02Fix variables and assumptionsL11–20

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro fb
  2. L12
    intro fc
  3. L13
    intro gb
  4. L14
    intro gc
  5. L15
    intro hb
  6. L16
    intro hc
  7. L17
    intro ub
  8. L18
    intro uc
  9. L19
    intro vb
  10. L20
    intro vc
03Fix variables and assumptionsL21–30

Work with arbitrary variables or the premises of the current implication.

  1. L21
    intro Ub
  2. L22
    intro Uc
  3. L23
    intro Vb
  4. L24
    intro Vc
  5. L25
    intro l
  6. L26
    intro hrows
  7. L27
    intro hcofactors
  8. L28
    intro hfirst
  9. L29
    intro hsecond
  10. L30
    intro i
04Fix variables and assumptionsL31–39

Work with arbitrary variables or the premises of the current implication.

  1. L31
    intro p
  2. L32
    intro n
  3. L33
    intro P
  4. L34
    intro N
  5. L35
    intro hi
  6. L36
    intro hp
  7. L37
    intro hn
  8. L38
    intro hP
  9. L39
    intro hN
05Establish hfirstentryL40–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hfirst.

  1. L40
    have hfirstentry : ∃ ap. ∃ an. ∃ bp. ∃ bn. ∃ tp. ∃ tn. BetaAt(ab,ac,i,ap) ∧ (BetaAt(bb,bc,i,an) ∧ (BetaAt(cb,cc,i,bp) ∧ (BetaAt(db,dc,i,bn) ∧ (BetaAt(ub,uc,i,tp) ∧ (BetaAt(vb,vc,i,tn) ∧ SignedAlternatingCofactorTerm(ap,an,bp,bn,i,tp,tn))))))Definitions: SignedAlternatingCofactorTermBetaAt
  2. L41
    specialize hfirst (i)
  3. L42
    apply hfirst
  4. L43
    exact hi
06Separate the logical casesL44–53

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L44
    cases hfirstentry
  2. L45
    cases hfirstentry_witness
  3. L46
    cases hfirstentry_witness_witness
  4. L47
    cases hfirstentry_witness_witness_witness
  5. L48
    cases hfirstentry_witness_witness_witness_witness
  6. L49
    cases hfirstentry_witness_witness_witness_witness_witness
  7. L50
    cases hfirstentry_witness_witness_witness_witness_witness_witness
  8. L51
    cases hfirstentry_witness_witness_witness_witness_witness_witness_right
  9. L52
    cases hfirstentry_witness_witness_witness_witness_witness_witness_right_right
  10. L53
    cases hfirstentry_witness_witness_witness_witness_witness_witness_right_right_right
07Separate the logical casesL54–55

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L54
    cases hfirstentry_witness_witness_witness_witness_witness_witness_right_right_right_right
  2. L55
    cases hfirstentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right
08Establish hsecondentryL56–59

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hsecond.

  1. L56
    have hsecondentry : ∃ ap. ∃ an. ∃ bp. ∃ bn. ∃ tp. ∃ tn. BetaAt(eb,ec,i,ap) ∧ (BetaAt(fb,fc,i,an) ∧ (BetaAt(gb,gc,i,bp) ∧ (BetaAt(hb,hc,i,bn) ∧ (BetaAt(Ub,Uc,i,tp) ∧ (BetaAt(Vb,Vc,i,tn) ∧ SignedAlternatingCofactorTerm(ap,an,bp,bn,i,tp,tn))))))Definitions: SignedAlternatingCofactorTermBetaAt
  2. L57
    specialize hsecond (i)
  3. L58
    apply hsecond
  4. L59
    exact hi
09Separate the logical casesL60–69

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L60
    cases hsecondentry
  2. L61
    cases hsecondentry_witness
  3. L62
    cases hsecondentry_witness_witness
  4. L63
    cases hsecondentry_witness_witness_witness
  5. L64
    cases hsecondentry_witness_witness_witness_witness
  6. L65
    cases hsecondentry_witness_witness_witness_witness_witness
  7. L66
    cases hsecondentry_witness_witness_witness_witness_witness_witness
  8. L67
    cases hsecondentry_witness_witness_witness_witness_witness_witness_right
  9. L68
    cases hsecondentry_witness_witness_witness_witness_witness_witness_right_right
  10. L69
    cases hsecondentry_witness_witness_witness_witness_witness_witness_right_right_right
10Separate the logical casesL70–71

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L70
    cases hsecondentry_witness_witness_witness_witness_witness_witness_right_right_right_right
  2. L71
    cases hsecondentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right
11Establish hbalanceL72–81

Establish this local claim before using it. It is not an additional assumption.

  1. L72
    have hbalance : x4 + x11 = x10 + x5
  2. L73
    specialize matrix_integer_cofactor_term_balance (x)
  3. L74
    specialize matrix_integer_cofactor_term_balance (x1)
  4. L75
    specialize matrix_integer_cofactor_term_balance (x2)
  5. L76
    specialize matrix_integer_cofactor_term_balance (x3)
  6. L77
    specialize matrix_integer_cofactor_term_balance (x6)
  7. L78
    specialize matrix_integer_cofactor_term_balance (x7)
  8. L79
    specialize matrix_integer_cofactor_term_balance (x8)
  9. L80
    specialize matrix_integer_cofactor_term_balance (x9)
  10. L81
    specialize matrix_integer_cofactor_term_balance (i)
12Use earlier factsL82–91

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L82
    specialize matrix_integer_cofactor_term_balance (x4)
  2. L83
    specialize matrix_integer_cofactor_term_balance (x5)
  3. L84
    specialize matrix_integer_cofactor_term_balance (x10)
  4. L85
    specialize matrix_integer_cofactor_term_balance (x11)
  5. L86
    apply matrix_integer_cofactor_term_balance
  6. L87
    specialize hrows (i)
  7. L88
    specialize hrows (x)
  8. L89
    specialize hrows (x1)
  9. L90
    specialize hrows (x6)
  10. L91
    specialize hrows (x7)
13Use earlier factsL92–101

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L92
    apply hrows
  2. L93
    exact hi
  3. L94
    exact hfirstentry_witness_witness_witness_witness_witness_witness_left
  4. L95
    exact hfirstentry_witness_witness_witness_witness_witness_witness_right_left
  5. L96
    exact hsecondentry_witness_witness_witness_witness_witness_witness_left
  6. L97
    exact hsecondentry_witness_witness_witness_witness_witness_witness_right_left
  7. L98
    specialize hcofactors (i)
  8. L99
    specialize hcofactors (x2)
  9. L100
    specialize hcofactors (x3)
  10. L101
    specialize hcofactors (x8)
14Use earlier factsL102–110

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L102
    specialize hcofactors (x9)
  2. L103
    apply hcofactors
  3. L104
    exact hi
  4. L105
    exact hfirstentry_witness_witness_witness_witness_witness_witness_right_right_left
  5. L106
    exact hfirstentry_witness_witness_witness_witness_witness_witness_right_right_right_left
  6. L107
    exact hsecondentry_witness_witness_witness_witness_witness_witness_right_right_left
  7. L108
    exact hsecondentry_witness_witness_witness_witness_witness_witness_right_right_right_left
  8. L109
    exact hfirstentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  9. L110
    exact hsecondentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
15Establish hpositiveL111–119

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L111
    have hpositive : p = x4
  2. L112
    specialize beta_at_unique (ub)
  3. L113
    specialize beta_at_unique (uc)
  4. L114
    specialize beta_at_unique (i)
  5. L115
    specialize beta_at_unique (p)
  6. L116
    specialize beta_at_unique (x4)
  7. L117
    apply beta_at_unique
  8. L118
    exact hp
  9. L119
    exact hfirstentry_witness_witness_witness_witness_witness_witness_right_right_right_right_left
16Establish hnegativeL120–128

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L120
    have hnegative : n = x5
  2. L121
    specialize beta_at_unique (vb)
  3. L122
    specialize beta_at_unique (vc)
  4. L123
    specialize beta_at_unique (i)
  5. L124
    specialize beta_at_unique (n)
  6. L125
    specialize beta_at_unique (x5)
  7. L126
    apply beta_at_unique
  8. L127
    exact hn
  9. L128
    exact hfirstentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
17Establish hotherpositiveL129–137

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L129
    have hotherpositive : P = x10
  2. L130
    specialize beta_at_unique (Ub)
  3. L131
    specialize beta_at_unique (Uc)
  4. L132
    specialize beta_at_unique (i)
  5. L133
    specialize beta_at_unique (P)
  6. L134
    specialize beta_at_unique (x10)
  7. L135
    apply beta_at_unique
  8. L136
    exact hP
  9. L137
    exact hsecondentry_witness_witness_witness_witness_witness_witness_right_right_right_right_left
18Establish hothernegativeL138–147

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L138
    have hothernegative : N = x11
  2. L139
    specialize beta_at_unique (Vb)
  3. L140
    specialize beta_at_unique (Vc)
  4. L141
    specialize beta_at_unique (i)
  5. L142
    specialize beta_at_unique (N)
  6. L143
    specialize beta_at_unique (x11)
  7. L144
    apply beta_at_unique
  8. L145
    exact hN
  9. L146
    exact hsecondentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  10. L147
    rewrite hpositive
19Calculate and transport equalitiesL148–150

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L148
    rewrite hnegative
  2. L149
    rewrite hotherpositive
  3. L150
    rewrite hothernegative
20Use earlier factsL151–151

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L151
    exact hbalance

Library-wide reading audit

Original exact command ledger · 151 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro bb
  4. 0004intro bc
  5. 0005intro cb
  6. 0006intro cc
  7. 0007intro db
  8. 0008intro dc
  9. 0009intro eb
  10. 0010intro ec
  11. 0011intro fb
  12. 0012intro fc
  13. 0013intro gb
  14. 0014intro gc
  15. 0015intro hb
  16. 0016intro hc
  17. 0017intro ub
  18. 0018intro uc
  19. 0019intro vb
  20. 0020intro vc
  21. 0021intro Ub
  22. 0022intro Uc
  23. 0023intro Vb
  24. 0024intro Vc
  25. 0025intro l
  26. 0026intro hrows
  27. 0027intro hcofactors
  28. 0028intro hfirst
  29. 0029intro hsecond
  30. 0030intro i
  31. 0031intro p
  32. 0032intro n
  33. 0033intro P
  34. 0034intro N
  35. 0035intro hi
  36. 0036intro hp
  37. 0037intro hn
  38. 0038intro hP
  39. 0039intro hN
  40. 0040have hfirstentry : exists ap an bp bn tp tn. ((((exists ff_h_mdr_integer_first_entry0. ff_h_mdr_integer_first_entry0 + S (ap) = S ((S (i)) * ac)) /\ exists ff_q_mdr_integer_first_entry0. ab = ff_q_mdr_integer_first_entry0 * S ((S (i)) * ac) + (ap))) /\ ((((exists ff_h_mdr_integer_first_entry1. ff_h_mdr_integer_first_entry1 + S (an) = S ((S (i)) * bc)) /\ exists ff_q_mdr_integer_first_entry1. bb = ff_q_mdr_integer_first_entry1 * S ((S (i)) * bc) + (an))) /\ ((((exists ff_h_mdr_integer_first_entry2. ff_h_mdr_integer_first_entry2 + S (bp) = S ((S (i)) * cc)) /\ exists ff_q_mdr_integer_first_entry2. cb = ff_q_mdr_integer_first_entry2 * S ((S (i)) * cc) + (bp))) /\ ((((exists ff_h_mdr_integer_first_entry3. ff_h_mdr_integer_first_entry3 + S (bn) = S ((S (i)) * dc)) /\ exists ff_q_mdr_integer_first_entry3. db = ff_q_mdr_integer_first_entry3 * S ((S (i)) * dc) + (bn))) /\ ((((exists ff_h_mdr_integer_first_entrypositive. ff_h_mdr_integer_first_entrypositive + S (tp) = S ((S (i)) * uc)) /\ exists ff_q_mdr_integer_first_entrypositive. ub = ff_q_mdr_integer_first_entrypositive * S ((S (i)) * uc) + (tp))) /\ ((((exists ff_h_mdr_integer_first_entrynegative. ff_h_mdr_integer_first_entrynegative + S (tn) = S ((S (i)) * vc)) /\ exists ff_q_mdr_integer_first_entrynegative. vb = ff_q_mdr_integer_first_entrynegative * S ((S (i)) * vc) + (tn))) /\ (((exists ff_even_mce_term_integer_first_entryterm. i = 2 * ff_even_mce_term_integer_first_entryterm) /\ (tp = (ap) * (bp) + (an) * (bn) /\ tn = (ap) * (bn) + (an) * (bp))) \/ ((exists ff_odd_mce_term_integer_first_entryterm. i = 2 * ff_odd_mce_term_integer_first_entryterm + 1) /\ (tp = (ap) * (bn) + (an) * (bp) /\ tn = (ap) * (bp) + (an) * (bn))))))))))
  41. 0041specialize hfirst (i)
  42. 0042apply hfirst
  43. 0043exact hi
  44. 0044cases hfirstentry
  45. 0045cases hfirstentry_witness
  46. 0046cases hfirstentry_witness_witness
  47. 0047cases hfirstentry_witness_witness_witness
  48. 0048cases hfirstentry_witness_witness_witness_witness
  49. 0049cases hfirstentry_witness_witness_witness_witness_witness
  50. 0050cases hfirstentry_witness_witness_witness_witness_witness_witness
  51. 0051cases hfirstentry_witness_witness_witness_witness_witness_witness_right
  52. 0052cases hfirstentry_witness_witness_witness_witness_witness_witness_right_right
  53. 0053cases hfirstentry_witness_witness_witness_witness_witness_witness_right_right_right
  54. 0054cases hfirstentry_witness_witness_witness_witness_witness_witness_right_right_right_right
  55. 0055cases hfirstentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  56. 0056have hsecondentry : exists ap an bp bn tp tn. ((((exists ff_h_mdr_integer_second_entry0. ff_h_mdr_integer_second_entry0 + S (ap) = S ((S (i)) * ec)) /\ exists ff_q_mdr_integer_second_entry0. eb = ff_q_mdr_integer_second_entry0 * S ((S (i)) * ec) + (ap))) /\ ((((exists ff_h_mdr_integer_second_entry1. ff_h_mdr_integer_second_entry1 + S (an) = S ((S (i)) * fc)) /\ exists ff_q_mdr_integer_second_entry1. fb = ff_q_mdr_integer_second_entry1 * S ((S (i)) * fc) + (an))) /\ ((((exists ff_h_mdr_integer_second_entry2. ff_h_mdr_integer_second_entry2 + S (bp) = S ((S (i)) * gc)) /\ exists ff_q_mdr_integer_second_entry2. gb = ff_q_mdr_integer_second_entry2 * S ((S (i)) * gc) + (bp))) /\ ((((exists ff_h_mdr_integer_second_entry3. ff_h_mdr_integer_second_entry3 + S (bn) = S ((S (i)) * hc)) /\ exists ff_q_mdr_integer_second_entry3. hb = ff_q_mdr_integer_second_entry3 * S ((S (i)) * hc) + (bn))) /\ ((((exists ff_h_mdr_integer_second_entrypositive. ff_h_mdr_integer_second_entrypositive + S (tp) = S ((S (i)) * Uc)) /\ exists ff_q_mdr_integer_second_entrypositive. Ub = ff_q_mdr_integer_second_entrypositive * S ((S (i)) * Uc) + (tp))) /\ ((((exists ff_h_mdr_integer_second_entrynegative. ff_h_mdr_integer_second_entrynegative + S (tn) = S ((S (i)) * Vc)) /\ exists ff_q_mdr_integer_second_entrynegative. Vb = ff_q_mdr_integer_second_entrynegative * S ((S (i)) * Vc) + (tn))) /\ (((exists ff_even_mce_term_integer_second_entryterm. i = 2 * ff_even_mce_term_integer_second_entryterm) /\ (tp = (ap) * (bp) + (an) * (bn) /\ tn = (ap) * (bn) + (an) * (bp))) \/ ((exists ff_odd_mce_term_integer_second_entryterm. i = 2 * ff_odd_mce_term_integer_second_entryterm + 1) /\ (tp = (ap) * (bn) + (an) * (bp) /\ tn = (ap) * (bp) + (an) * (bn))))))))))
  57. 0057specialize hsecond (i)
  58. 0058apply hsecond
  59. 0059exact hi
  60. 0060cases hsecondentry
  61. 0061cases hsecondentry_witness
  62. 0062cases hsecondentry_witness_witness
  63. 0063cases hsecondentry_witness_witness_witness
  64. 0064cases hsecondentry_witness_witness_witness_witness
  65. 0065cases hsecondentry_witness_witness_witness_witness_witness
  66. 0066cases hsecondentry_witness_witness_witness_witness_witness_witness
  67. 0067cases hsecondentry_witness_witness_witness_witness_witness_witness_right
  68. 0068cases hsecondentry_witness_witness_witness_witness_witness_witness_right_right
  69. 0069cases hsecondentry_witness_witness_witness_witness_witness_witness_right_right_right
  70. 0070cases hsecondentry_witness_witness_witness_witness_witness_witness_right_right_right_right
  71. 0071cases hsecondentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  72. 0072have hbalance : x4 + x11 = x10 + x5
  73. 0073specialize matrix_integer_cofactor_term_balance (x)
  74. 0074specialize matrix_integer_cofactor_term_balance (x1)
  75. 0075specialize matrix_integer_cofactor_term_balance (x2)
  76. 0076specialize matrix_integer_cofactor_term_balance (x3)
  77. 0077specialize matrix_integer_cofactor_term_balance (x6)
  78. 0078specialize matrix_integer_cofactor_term_balance (x7)
  79. 0079specialize matrix_integer_cofactor_term_balance (x8)
  80. 0080specialize matrix_integer_cofactor_term_balance (x9)
  81. 0081specialize matrix_integer_cofactor_term_balance (i)
  82. 0082specialize matrix_integer_cofactor_term_balance (x4)
  83. 0083specialize matrix_integer_cofactor_term_balance (x5)
  84. 0084specialize matrix_integer_cofactor_term_balance (x10)
  85. 0085specialize matrix_integer_cofactor_term_balance (x11)
  86. 0086apply matrix_integer_cofactor_term_balance
  87. 0087specialize hrows (i)
  88. 0088specialize hrows (x)
  89. 0089specialize hrows (x1)
  90. 0090specialize hrows (x6)
  91. 0091specialize hrows (x7)
  92. 0092apply hrows
  93. 0093exact hi
  94. 0094exact hfirstentry_witness_witness_witness_witness_witness_witness_left
  95. 0095exact hfirstentry_witness_witness_witness_witness_witness_witness_right_left
  96. 0096exact hsecondentry_witness_witness_witness_witness_witness_witness_left
  97. 0097exact hsecondentry_witness_witness_witness_witness_witness_witness_right_left
  98. 0098specialize hcofactors (i)
  99. 0099specialize hcofactors (x2)
  100. 0100specialize hcofactors (x3)
  101. 0101specialize hcofactors (x8)
  102. 0102specialize hcofactors (x9)
  103. 0103apply hcofactors
  104. 0104exact hi
  105. 0105exact hfirstentry_witness_witness_witness_witness_witness_witness_right_right_left
  106. 0106exact hfirstentry_witness_witness_witness_witness_witness_witness_right_right_right_left
  107. 0107exact hsecondentry_witness_witness_witness_witness_witness_witness_right_right_left
  108. 0108exact hsecondentry_witness_witness_witness_witness_witness_witness_right_right_right_left
  109. 0109exact hfirstentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  110. 0110exact hsecondentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  111. 0111have hpositive : p = x4
  112. 0112specialize beta_at_unique (ub)
  113. 0113specialize beta_at_unique (uc)
  114. 0114specialize beta_at_unique (i)
  115. 0115specialize beta_at_unique (p)
  116. 0116specialize beta_at_unique (x4)
  117. 0117apply beta_at_unique
  118. 0118exact hp
  119. 0119exact hfirstentry_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  120. 0120have hnegative : n = x5
  121. 0121specialize beta_at_unique (vb)
  122. 0122specialize beta_at_unique (vc)
  123. 0123specialize beta_at_unique (i)
  124. 0124specialize beta_at_unique (n)
  125. 0125specialize beta_at_unique (x5)
  126. 0126apply beta_at_unique
  127. 0127exact hn
  128. 0128exact hfirstentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  129. 0129have hotherpositive : P = x10
  130. 0130specialize beta_at_unique (Ub)
  131. 0131specialize beta_at_unique (Uc)
  132. 0132specialize beta_at_unique (i)
  133. 0133specialize beta_at_unique (P)
  134. 0134specialize beta_at_unique (x10)
  135. 0135apply beta_at_unique
  136. 0136exact hP
  137. 0137exact hsecondentry_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  138. 0138have hothernegative : N = x11
  139. 0139specialize beta_at_unique (Vb)
  140. 0140specialize beta_at_unique (Vc)
  141. 0141specialize beta_at_unique (i)
  142. 0142specialize beta_at_unique (N)
  143. 0143specialize beta_at_unique (x11)
  144. 0144apply beta_at_unique
  145. 0145exact hN
  146. 0146exact hsecondentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  147. 0147rewrite hpositive
  148. 0148rewrite hnegative
  149. 0149rewrite hotherpositive
  150. 0150rewrite hothernegative
  151. 0151exact hbalance