SS000A

divisor_signed_sum_to_components

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

Every signed sum unpacks into actual natural prefix sums against its proved table representation.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

These are genuine signed-table and finite-sum foundations, not full divisor-sum cancellation or Möbius inversion. G007 remains open. The historical MatrixMinorFourCode definition is reused solely as generic nested pairing of four beta parameters; no matrix-specific hypothesis is imported. Equality is equality of represented signed values, not equality of arbitrary component codes.

Exact theorem in conservative defined notation

∀ F. ∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ l. ∀ z. MatrixMinorFourCode(F,pb,pc,nb,nc) → SignedPrefixSum(F,l,z) → ∃ x. ∃ y. Sum(pb,pc,l,x) ∧ (Sum(nb,nc,l,y) ∧ SignedBalance(z,x,y))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

MatrixMinorFourCode(z,up,us,un,ut) · 1SignedBalance(z,p,n) · 1SignedPrefixSum(F,l,z) · 1Sum(b,c,l,z) · 2

Actual proof prerequisites

matrix_minor_four_code_components_injective · checked external prerequisite
Original expanded first-order statement 
forall F pb pc nb nc l z. ((F) = (((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) * S ((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) + ((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))))) -> (exists dst_positive_code_sum_unpacked_input dst_positive_scale_sum_unpacked_input dst_negative_code_sum_unpacked_input dst_negative_scale_sum_unpacked_input dst_positive_sum_sum_unpacked_input dst_negative_sum_sum_unpacked_input. (((F) = (((((dst_positive_code_sum_unpacked_input) + (dst_positive_scale_sum_unpacked_input)) * S ((dst_positive_code_sum_unpacked_input) + (dst_positive_scale_sum_unpacked_input)) + ((dst_positive_scale_sum_unpacked_input) + (dst_positive_scale_sum_unpacked_input))) + (((dst_negative_code_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)) * S ((dst_negative_code_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)) + ((dst_negative_scale_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)))) * S ((((dst_positive_code_sum_unpacked_input) + (dst_positive_scale_sum_unpacked_input)) * S ((dst_positive_code_sum_unpacked_input) + (dst_positive_scale_sum_unpacked_input)) + ((dst_positive_scale_sum_unpacked_input) + (dst_positive_scale_sum_unpacked_input))) + (((dst_negative_code_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)) * S ((dst_negative_code_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)) + ((dst_negative_scale_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)))) + ((((dst_negative_code_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)) * S ((dst_negative_code_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)) + ((dst_negative_scale_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input))) + (((dst_negative_code_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)) * S ((dst_negative_code_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)) + ((dst_negative_scale_sum_unpacked_input) + (dst_negative_scale_sum_unpacked_input)))))) /\ (((exists fs_u_dst_sum_unpacked_inputpositive fs_v_dst_sum_unpacked_inputpositive. ((((exists fs_h_dst_sum_unpacked_inputpositive_body_start. fs_h_dst_sum_unpacked_inputpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unpacked_inputpositive)) /\ exists fs_q_dst_sum_unpacked_inputpositive_body_start. fs_u_dst_sum_unpacked_inputpositive = fs_q_dst_sum_unpacked_inputpositive_body_start * S ((S (0)) * fs_v_dst_sum_unpacked_inputpositive) + (0))) /\ ((((exists fs_h_dst_sum_unpacked_inputpositive_body_terminal. fs_h_dst_sum_unpacked_inputpositive_body_terminal + S (dst_positive_sum_sum_unpacked_input) = S ((S (l)) * fs_v_dst_sum_unpacked_inputpositive)) /\ exists fs_q_dst_sum_unpacked_inputpositive_body_terminal. fs_u_dst_sum_unpacked_inputpositive = fs_q_dst_sum_unpacked_inputpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_unpacked_inputpositive) + (dst_positive_sum_sum_unpacked_input))) /\ forall fs_i_dst_sum_unpacked_inputpositive_body_steps. (exists fs_lt_dst_sum_unpacked_inputpositive_body_steps_bound. fs_lt_dst_sum_unpacked_inputpositive_body_steps_bound + S fs_i_dst_sum_unpacked_inputpositive_body_steps = l) -> exists fs_a_dst_sum_unpacked_inputpositive_body_steps fs_r_dst_sum_unpacked_inputpositive_body_steps fs_s_dst_sum_unpacked_inputpositive_body_steps. ((((exists fs_h_dst_sum_unpacked_inputpositive_body_steps_summand. fs_h_dst_sum_unpacked_inputpositive_body_steps_summand + S (fs_a_dst_sum_unpacked_inputpositive_body_steps) = S ((S (fs_i_dst_sum_unpacked_inputpositive_body_steps)) * dst_positive_scale_sum_unpacked_input)) /\ exists fs_q_dst_sum_unpacked_inputpositive_body_steps_summand. dst_positive_code_sum_unpacked_input = fs_q_dst_sum_unpacked_inputpositive_body_steps_summand * S ((S (fs_i_dst_sum_unpacked_inputpositive_body_steps)) * dst_positive_scale_sum_unpacked_input) + (fs_a_dst_sum_unpacked_inputpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unpacked_inputpositive_body_steps_partial. fs_h_dst_sum_unpacked_inputpositive_body_steps_partial + S (fs_r_dst_sum_unpacked_inputpositive_body_steps) = S ((S (fs_i_dst_sum_unpacked_inputpositive_body_steps)) * fs_v_dst_sum_unpacked_inputpositive)) /\ exists fs_q_dst_sum_unpacked_inputpositive_body_steps_partial. fs_u_dst_sum_unpacked_inputpositive = fs_q_dst_sum_unpacked_inputpositive_body_steps_partial * S ((S (fs_i_dst_sum_unpacked_inputpositive_body_steps)) * fs_v_dst_sum_unpacked_inputpositive) + (fs_r_dst_sum_unpacked_inputpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unpacked_inputpositive_body_steps_successor. fs_h_dst_sum_unpacked_inputpositive_body_steps_successor + S (fs_s_dst_sum_unpacked_inputpositive_body_steps) = S ((S (S fs_i_dst_sum_unpacked_inputpositive_body_steps)) * fs_v_dst_sum_unpacked_inputpositive)) /\ exists fs_q_dst_sum_unpacked_inputpositive_body_steps_successor. fs_u_dst_sum_unpacked_inputpositive = fs_q_dst_sum_unpacked_inputpositive_body_steps_successor * S ((S (S fs_i_dst_sum_unpacked_inputpositive_body_steps)) * fs_v_dst_sum_unpacked_inputpositive) + (fs_s_dst_sum_unpacked_inputpositive_body_steps))) /\ fs_s_dst_sum_unpacked_inputpositive_body_steps = fs_r_dst_sum_unpacked_inputpositive_body_steps + fs_a_dst_sum_unpacked_inputpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_unpacked_inputnegative fs_v_dst_sum_unpacked_inputnegative. ((((exists fs_h_dst_sum_unpacked_inputnegative_body_start. fs_h_dst_sum_unpacked_inputnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unpacked_inputnegative)) /\ exists fs_q_dst_sum_unpacked_inputnegative_body_start. fs_u_dst_sum_unpacked_inputnegative = fs_q_dst_sum_unpacked_inputnegative_body_start * S ((S (0)) * fs_v_dst_sum_unpacked_inputnegative) + (0))) /\ ((((exists fs_h_dst_sum_unpacked_inputnegative_body_terminal. fs_h_dst_sum_unpacked_inputnegative_body_terminal + S (dst_negative_sum_sum_unpacked_input) = S ((S (l)) * fs_v_dst_sum_unpacked_inputnegative)) /\ exists fs_q_dst_sum_unpacked_inputnegative_body_terminal. fs_u_dst_sum_unpacked_inputnegative = fs_q_dst_sum_unpacked_inputnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_unpacked_inputnegative) + (dst_negative_sum_sum_unpacked_input))) /\ forall fs_i_dst_sum_unpacked_inputnegative_body_steps. (exists fs_lt_dst_sum_unpacked_inputnegative_body_steps_bound. fs_lt_dst_sum_unpacked_inputnegative_body_steps_bound + S fs_i_dst_sum_unpacked_inputnegative_body_steps = l) -> exists fs_a_dst_sum_unpacked_inputnegative_body_steps fs_r_dst_sum_unpacked_inputnegative_body_steps fs_s_dst_sum_unpacked_inputnegative_body_steps. ((((exists fs_h_dst_sum_unpacked_inputnegative_body_steps_summand. fs_h_dst_sum_unpacked_inputnegative_body_steps_summand + S (fs_a_dst_sum_unpacked_inputnegative_body_steps) = S ((S (fs_i_dst_sum_unpacked_inputnegative_body_steps)) * dst_negative_scale_sum_unpacked_input)) /\ exists fs_q_dst_sum_unpacked_inputnegative_body_steps_summand. dst_negative_code_sum_unpacked_input = fs_q_dst_sum_unpacked_inputnegative_body_steps_summand * S ((S (fs_i_dst_sum_unpacked_inputnegative_body_steps)) * dst_negative_scale_sum_unpacked_input) + (fs_a_dst_sum_unpacked_inputnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unpacked_inputnegative_body_steps_partial. fs_h_dst_sum_unpacked_inputnegative_body_steps_partial + S (fs_r_dst_sum_unpacked_inputnegative_body_steps) = S ((S (fs_i_dst_sum_unpacked_inputnegative_body_steps)) * fs_v_dst_sum_unpacked_inputnegative)) /\ exists fs_q_dst_sum_unpacked_inputnegative_body_steps_partial. fs_u_dst_sum_unpacked_inputnegative = fs_q_dst_sum_unpacked_inputnegative_body_steps_partial * S ((S (fs_i_dst_sum_unpacked_inputnegative_body_steps)) * fs_v_dst_sum_unpacked_inputnegative) + (fs_r_dst_sum_unpacked_inputnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unpacked_inputnegative_body_steps_successor. fs_h_dst_sum_unpacked_inputnegative_body_steps_successor + S (fs_s_dst_sum_unpacked_inputnegative_body_steps) = S ((S (S fs_i_dst_sum_unpacked_inputnegative_body_steps)) * fs_v_dst_sum_unpacked_inputnegative)) /\ exists fs_q_dst_sum_unpacked_inputnegative_body_steps_successor. fs_u_dst_sum_unpacked_inputnegative = fs_q_dst_sum_unpacked_inputnegative_body_steps_successor * S ((S (S fs_i_dst_sum_unpacked_inputnegative_body_steps)) * fs_v_dst_sum_unpacked_inputnegative) + (fs_s_dst_sum_unpacked_inputnegative_body_steps))) /\ fs_s_dst_sum_unpacked_inputnegative_body_steps = fs_r_dst_sum_unpacked_inputnegative_body_steps + fs_a_dst_sum_unpacked_inputnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_unpacked_inputresult ge_balance_negative_sum_unpacked_inputresult. (((((z) = 2 * (ge_balance_positive_sum_unpacked_inputresult) /\ (ge_balance_negative_sum_unpacked_inputresult) = 0) \/ exists ge_signed_half_sum_unpacked_inputresultdecode. (((z) = 2 * ge_signed_half_sum_unpacked_inputresultdecode + 1 /\ (ge_balance_positive_sum_unpacked_inputresult) = 0) /\ (ge_balance_negative_sum_unpacked_inputresult) = S ge_signed_half_sum_unpacked_inputresultdecode))) /\ ((dst_positive_sum_sum_unpacked_input) + ge_balance_negative_sum_unpacked_inputresult = (dst_negative_sum_sum_unpacked_input) + ge_balance_positive_sum_unpacked_inputresult))))))))) -> exists p n. ((exists fs_u_dst_sum_unpacked_positive fs_v_dst_sum_unpacked_positive. ((((exists fs_h_dst_sum_unpacked_positive_body_start. fs_h_dst_sum_unpacked_positive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unpacked_positive)) /\ exists fs_q_dst_sum_unpacked_positive_body_start. fs_u_dst_sum_unpacked_positive = fs_q_dst_sum_unpacked_positive_body_start * S ((S (0)) * fs_v_dst_sum_unpacked_positive) + (0))) /\ ((((exists fs_h_dst_sum_unpacked_positive_body_terminal. fs_h_dst_sum_unpacked_positive_body_terminal + S (p) = S ((S (l)) * fs_v_dst_sum_unpacked_positive)) /\ exists fs_q_dst_sum_unpacked_positive_body_terminal. fs_u_dst_sum_unpacked_positive = fs_q_dst_sum_unpacked_positive_body_terminal * S ((S (l)) * fs_v_dst_sum_unpacked_positive) + (p))) /\ forall fs_i_dst_sum_unpacked_positive_body_steps. (exists fs_lt_dst_sum_unpacked_positive_body_steps_bound. fs_lt_dst_sum_unpacked_positive_body_steps_bound + S fs_i_dst_sum_unpacked_positive_body_steps = l) -> exists fs_a_dst_sum_unpacked_positive_body_steps fs_r_dst_sum_unpacked_positive_body_steps fs_s_dst_sum_unpacked_positive_body_steps. ((((exists fs_h_dst_sum_unpacked_positive_body_steps_summand. fs_h_dst_sum_unpacked_positive_body_steps_summand + S (fs_a_dst_sum_unpacked_positive_body_steps) = S ((S (fs_i_dst_sum_unpacked_positive_body_steps)) * pc)) /\ exists fs_q_dst_sum_unpacked_positive_body_steps_summand. pb = fs_q_dst_sum_unpacked_positive_body_steps_summand * S ((S (fs_i_dst_sum_unpacked_positive_body_steps)) * pc) + (fs_a_dst_sum_unpacked_positive_body_steps))) /\ ((((exists fs_h_dst_sum_unpacked_positive_body_steps_partial. fs_h_dst_sum_unpacked_positive_body_steps_partial + S (fs_r_dst_sum_unpacked_positive_body_steps) = S ((S (fs_i_dst_sum_unpacked_positive_body_steps)) * fs_v_dst_sum_unpacked_positive)) /\ exists fs_q_dst_sum_unpacked_positive_body_steps_partial. fs_u_dst_sum_unpacked_positive = fs_q_dst_sum_unpacked_positive_body_steps_partial * S ((S (fs_i_dst_sum_unpacked_positive_body_steps)) * fs_v_dst_sum_unpacked_positive) + (fs_r_dst_sum_unpacked_positive_body_steps))) /\ ((((exists fs_h_dst_sum_unpacked_positive_body_steps_successor. fs_h_dst_sum_unpacked_positive_body_steps_successor + S (fs_s_dst_sum_unpacked_positive_body_steps) = S ((S (S fs_i_dst_sum_unpacked_positive_body_steps)) * fs_v_dst_sum_unpacked_positive)) /\ exists fs_q_dst_sum_unpacked_positive_body_steps_successor. fs_u_dst_sum_unpacked_positive = fs_q_dst_sum_unpacked_positive_body_steps_successor * S ((S (S fs_i_dst_sum_unpacked_positive_body_steps)) * fs_v_dst_sum_unpacked_positive) + (fs_s_dst_sum_unpacked_positive_body_steps))) /\ fs_s_dst_sum_unpacked_positive_body_steps = fs_r_dst_sum_unpacked_positive_body_steps + fs_a_dst_sum_unpacked_positive_body_steps)))))) /\ (((exists fs_u_dst_sum_unpacked_negative fs_v_dst_sum_unpacked_negative. ((((exists fs_h_dst_sum_unpacked_negative_body_start. fs_h_dst_sum_unpacked_negative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unpacked_negative)) /\ exists fs_q_dst_sum_unpacked_negative_body_start. fs_u_dst_sum_unpacked_negative = fs_q_dst_sum_unpacked_negative_body_start * S ((S (0)) * fs_v_dst_sum_unpacked_negative) + (0))) /\ ((((exists fs_h_dst_sum_unpacked_negative_body_terminal. fs_h_dst_sum_unpacked_negative_body_terminal + S (n) = S ((S (l)) * fs_v_dst_sum_unpacked_negative)) /\ exists fs_q_dst_sum_unpacked_negative_body_terminal. fs_u_dst_sum_unpacked_negative = fs_q_dst_sum_unpacked_negative_body_terminal * S ((S (l)) * fs_v_dst_sum_unpacked_negative) + (n))) /\ forall fs_i_dst_sum_unpacked_negative_body_steps. (exists fs_lt_dst_sum_unpacked_negative_body_steps_bound. fs_lt_dst_sum_unpacked_negative_body_steps_bound + S fs_i_dst_sum_unpacked_negative_body_steps = l) -> exists fs_a_dst_sum_unpacked_negative_body_steps fs_r_dst_sum_unpacked_negative_body_steps fs_s_dst_sum_unpacked_negative_body_steps. ((((exists fs_h_dst_sum_unpacked_negative_body_steps_summand. fs_h_dst_sum_unpacked_negative_body_steps_summand + S (fs_a_dst_sum_unpacked_negative_body_steps) = S ((S (fs_i_dst_sum_unpacked_negative_body_steps)) * nc)) /\ exists fs_q_dst_sum_unpacked_negative_body_steps_summand. nb = fs_q_dst_sum_unpacked_negative_body_steps_summand * S ((S (fs_i_dst_sum_unpacked_negative_body_steps)) * nc) + (fs_a_dst_sum_unpacked_negative_body_steps))) /\ ((((exists fs_h_dst_sum_unpacked_negative_body_steps_partial. fs_h_dst_sum_unpacked_negative_body_steps_partial + S (fs_r_dst_sum_unpacked_negative_body_steps) = S ((S (fs_i_dst_sum_unpacked_negative_body_steps)) * fs_v_dst_sum_unpacked_negative)) /\ exists fs_q_dst_sum_unpacked_negative_body_steps_partial. fs_u_dst_sum_unpacked_negative = fs_q_dst_sum_unpacked_negative_body_steps_partial * S ((S (fs_i_dst_sum_unpacked_negative_body_steps)) * fs_v_dst_sum_unpacked_negative) + (fs_r_dst_sum_unpacked_negative_body_steps))) /\ ((((exists fs_h_dst_sum_unpacked_negative_body_steps_successor. fs_h_dst_sum_unpacked_negative_body_steps_successor + S (fs_s_dst_sum_unpacked_negative_body_steps) = S ((S (S fs_i_dst_sum_unpacked_negative_body_steps)) * fs_v_dst_sum_unpacked_negative)) /\ exists fs_q_dst_sum_unpacked_negative_body_steps_successor. fs_u_dst_sum_unpacked_negative = fs_q_dst_sum_unpacked_negative_body_steps_successor * S ((S (S fs_i_dst_sum_unpacked_negative_body_steps)) * fs_v_dst_sum_unpacked_negative) + (fs_s_dst_sum_unpacked_negative_body_steps))) /\ fs_s_dst_sum_unpacked_negative_body_steps = fs_r_dst_sum_unpacked_negative_body_steps + fs_a_dst_sum_unpacked_negative_body_steps)))))) /\ (exists ge_balance_positive_sum_unpacked_balance ge_balance_negative_sum_unpacked_balance. (((((z) = 2 * (ge_balance_positive_sum_unpacked_balance) /\ (ge_balance_negative_sum_unpacked_balance) = 0) \/ exists ge_signed_half_sum_unpacked_balancedecode. (((z) = 2 * ge_signed_half_sum_unpacked_balancedecode + 1 /\ (ge_balance_positive_sum_unpacked_balance) = 0) /\ (ge_balance_negative_sum_unpacked_balance) = S ge_signed_half_sum_unpacked_balancedecode))) /\ ((p) + ge_balance_negative_sum_unpacked_balance = (n) + ge_balance_positive_sum_unpacked_balance))))))

Complete tactic proof in conservative notation

All 47 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

47 script commands · 12 reading checkpoints · 1 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

01Fix variables and assumptionsL1–9

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

  1. L1
    intro F
  2. L2
    intro pb
  3. L3
    intro pc
  4. L4
    intro nb
  5. L5
    intro nc
  6. L6
    intro l
  7. L7
    intro z
  8. L8
    intro hrep
  9. L9
    intro hsum
02Separate the logical casesL10–18

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

  1. L10
    cases hsum
  2. L11
    cases hsum_witness
  3. L12
    cases hsum_witness_witness
  4. L13
    cases hsum_witness_witness_witness
  5. L14
    cases hsum_witness_witness_witness_witness
  6. L15
    cases hsum_witness_witness_witness_witness_witness
  7. L16
    cases hsum_witness_witness_witness_witness_witness_witness
  8. L17
    cases hsum_witness_witness_witness_witness_witness_witness_right
  9. L18
    cases hsum_witness_witness_witness_witness_witness_witness_right_right
03Establish heqL19–28

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

  1. L19
    have heq : ((x = pb) /\ (((x1 = pc) /\ (((x2 = nb) /\ (x3 = nc))))))
  2. L20
    specialize matrix_minor_four_code_components_injective (F)
  3. L21
    specialize matrix_minor_four_code_components_injective (x)
  4. L22
    specialize matrix_minor_four_code_components_injective (x1)
  5. L23
    specialize matrix_minor_four_code_components_injective (x2)
  6. L24
    specialize matrix_minor_four_code_components_injective (x3)
  7. L25
    specialize matrix_minor_four_code_components_injective (pb)
  8. L26
    specialize matrix_minor_four_code_components_injective (pc)
  9. L27
    specialize matrix_minor_four_code_components_injective (nb)
  10. L28
    specialize matrix_minor_four_code_components_injective (nc)
04Use earlier factsL29–31

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

  1. L29
    apply matrix_minor_four_code_components_injective
  2. L30
    exact hsum_witness_witness_witness_witness_witness_witness_left
  3. L31
    exact hrep
05Separate the logical casesL32–34

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

  1. L32
    cases heq
  2. L33
    cases heq_right
  3. L34
    cases heq_right_right
06Construct an explicit witnessL35–36

Supply the displayed value, then prove that it has the required property.

  1. L35
    exists x4
  2. L36
    exists x5
07Separate the logical casesL37–37

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

  1. L37
    split
08Calculate and transport equalitiesL38–40

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

  1. L38
    rewrite heq_left at hsum_witness_witness_witness_witness_witness_witness_right_left
  2. L39
    rewrite heq_right_left at hsum_witness_witness_witness_witness_witness_witness_right_left
  3. L40
    rewrite heq_right_left at hsum_witness_witness_witness_witness_witness_witness_right_left
09Use earlier factsL41–41

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

  1. L41
    exact hsum_witness_witness_witness_witness_witness_witness_right_left
10Separate the logical casesL42–42

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

  1. L42
    split
11Calculate and transport equalitiesL43–45

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

  1. L43
    rewrite heq_right_right_left at hsum_witness_witness_witness_witness_witness_witness_right_right_left
  2. L44
    rewrite heq_right_right_right at hsum_witness_witness_witness_witness_witness_witness_right_right_left
  3. L45
    rewrite heq_right_right_right at hsum_witness_witness_witness_witness_witness_witness_right_right_left
12Use earlier factsL46–47

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

  1. L46
    exact hsum_witness_witness_witness_witness_witness_witness_right_right_left
  2. L47
    exact hsum_witness_witness_witness_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 47 lines
  1. 0001intro F
  2. 0002intro pb
  3. 0003intro pc
  4. 0004intro nb
  5. 0005intro nc
  6. 0006intro l
  7. 0007intro z
  8. 0008intro hrep
  9. 0009intro hsum
  10. 0010cases hsum
  11. 0011cases hsum_witness
  12. 0012cases hsum_witness_witness
  13. 0013cases hsum_witness_witness_witness
  14. 0014cases hsum_witness_witness_witness_witness
  15. 0015cases hsum_witness_witness_witness_witness_witness
  16. 0016cases hsum_witness_witness_witness_witness_witness_witness
  17. 0017cases hsum_witness_witness_witness_witness_witness_witness_right
  18. 0018cases hsum_witness_witness_witness_witness_witness_witness_right_right
  19. 0019have heq : ((x = pb) /\ (((x1 = pc) /\ (((x2 = nb) /\ (x3 = nc))))))
  20. 0020specialize matrix_minor_four_code_components_injective (F)
  21. 0021specialize matrix_minor_four_code_components_injective (x)
  22. 0022specialize matrix_minor_four_code_components_injective (x1)
  23. 0023specialize matrix_minor_four_code_components_injective (x2)
  24. 0024specialize matrix_minor_four_code_components_injective (x3)
  25. 0025specialize matrix_minor_four_code_components_injective (pb)
  26. 0026specialize matrix_minor_four_code_components_injective (pc)
  27. 0027specialize matrix_minor_four_code_components_injective (nb)
  28. 0028specialize matrix_minor_four_code_components_injective (nc)
  29. 0029apply matrix_minor_four_code_components_injective
  30. 0030exact hsum_witness_witness_witness_witness_witness_witness_left
  31. 0031exact hrep
  32. 0032cases heq
  33. 0033cases heq_right
  34. 0034cases heq_right_right
  35. 0035exists x4
  36. 0036exists x5
  37. 0037split
  38. 0038rewrite heq_left at hsum_witness_witness_witness_witness_witness_witness_right_left
  39. 0039rewrite heq_right_left at hsum_witness_witness_witness_witness_witness_witness_right_left
  40. 0040rewrite heq_right_left at hsum_witness_witness_witness_witness_witness_witness_right_left
  41. 0041exact hsum_witness_witness_witness_witness_witness_witness_right_left
  42. 0042split
  43. 0043rewrite heq_right_right_left at hsum_witness_witness_witness_witness_witness_witness_right_right_left
  44. 0044rewrite heq_right_right_right at hsum_witness_witness_witness_witness_witness_witness_right_right_left
  45. 0045rewrite heq_right_right_right at hsum_witness_witness_witness_witness_witness_witness_right_right_left
  46. 0046exact hsum_witness_witness_witness_witness_witness_witness_right_right_left
  47. 0047exact hsum_witness_witness_witness_witness_witness_witness_right_right_right