DL0003

matrix_recursive_prefix_trans

Actual beta-prefix preservation composes without changing any encoded entry.

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

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.

This branch proves the finite determinant/rank/span substrate. It does not claim Smith or Hermite normal form, lattice index equals determinant, determinant multiplicativity, lattice reduction, or geometry-of-numbers theorems.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ u. ∀ v. ∀ w. ∀ z. ∀ l. (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(u,v,x,y)) → (∀ x. ∀ y. Lt(x,l) → BetaAt(u,v,x,y) → BetaAt(w,z,x,y)) → ∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(w,z,x,y)

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

Definition DAG

Lt(a,b) · 3BetaAt(b,c,i,x) · 6

Actual proof prerequisites

none
Original expanded first-order statement 
forall b c u v w z l. (forall mdr_i_source mdr_a_source. (exists mdr_gap_sourceb. mdr_gap_sourceb + S (mdr_i_source) = (l)) -> (((exists ff_h_mdr_sourceo. ff_h_mdr_sourceo + S (mdr_a_source) = S ((S (mdr_i_source)) * c)) /\ exists ff_q_mdr_sourceo. b = ff_q_mdr_sourceo * S ((S (mdr_i_source)) * c) + (mdr_a_source))) -> (((exists ff_h_mdr_sourcen. ff_h_mdr_sourcen + S (mdr_a_source) = S ((S (mdr_i_source)) * v)) /\ exists ff_q_mdr_sourcen. u = ff_q_mdr_sourcen * S ((S (mdr_i_source)) * v) + (mdr_a_source)))) -> (forall mdr_i_middle mdr_a_middle. (exists mdr_gap_middleb. mdr_gap_middleb + S (mdr_i_middle) = (l)) -> (((exists ff_h_mdr_middleo. ff_h_mdr_middleo + S (mdr_a_middle) = S ((S (mdr_i_middle)) * v)) /\ exists ff_q_mdr_middleo. u = ff_q_mdr_middleo * S ((S (mdr_i_middle)) * v) + (mdr_a_middle))) -> (((exists ff_h_mdr_middlen. ff_h_mdr_middlen + S (mdr_a_middle) = S ((S (mdr_i_middle)) * z)) /\ exists ff_q_mdr_middlen. w = ff_q_mdr_middlen * S ((S (mdr_i_middle)) * z) + (mdr_a_middle)))) -> (forall mdr_i_result mdr_a_result. (exists mdr_gap_resultb. mdr_gap_resultb + S (mdr_i_result) = (l)) -> (((exists ff_h_mdr_resulto. ff_h_mdr_resulto + S (mdr_a_result) = S ((S (mdr_i_result)) * c)) /\ exists ff_q_mdr_resulto. b = ff_q_mdr_resulto * S ((S (mdr_i_result)) * c) + (mdr_a_result))) -> (((exists ff_h_mdr_resultn. ff_h_mdr_resultn + S (mdr_a_result) = S ((S (mdr_i_result)) * z)) /\ exists ff_q_mdr_resultn. w = ff_q_mdr_resultn * S ((S (mdr_i_result)) * z) + (mdr_a_result))))

Complete tactic proof in conservative notation

All 22 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

22 script commands · 3 reading checkpoints · 0 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–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro u
  4. L4
    intro v
  5. L5
    intro w
  6. L6
    intro z
  7. L7
    intro l
  8. L8
    intro hfirst
  9. L9
    intro hsecond
  10. L10
    intro i
02Fix variables and assumptionsL11–13

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

  1. L11
    intro a
  2. L12
    intro hi
  3. L13
    intro ha
03Use earlier factsL14–22

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

  1. L14
    specialize hsecond (i)
  2. L15
    specialize hsecond (a)
  3. L16
    apply hsecond
  4. L17
    exact hi
  5. L18
    specialize hfirst (i)
  6. L19
    specialize hfirst (a)
  7. L20
    apply hfirst
  8. L21
    exact hi
  9. L22
    exact ha

Library-wide reading audit

Original defined command ledger · 22 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro u
  4. 0004intro v
  5. 0005intro w
  6. 0006intro z
  7. 0007intro l
  8. 0008intro hfirst
  9. 0009intro hsecond
  10. 0010intro i
  11. 0011intro a
  12. 0012intro hi
  13. 0013intro ha
  14. 0014specialize hsecond (i)
  15. 0015specialize hsecond (a)
  16. 0016apply hsecond
  17. 0017exact hi
  18. 0018specialize hfirst (i)
  19. 0019specialize hfirst (a)
  20. 0020apply hfirst
  21. 0021exact hi
  22. 0022exact ha