DL0030 — matrix_rank_recode_congruences_exists

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

∀ k. ∀ c. ∀ b. ∀ e. (∀ x. (∃ y. S x + S y = S k) → ∃ y. c = S x · y) → ∃ x. ∀ y. ∀ z. Lt(y,k) → BetaAt(b,e,y,z) → ∃ n. ∃ m. x + S (S y · c) · n = z + S (S y · c) · m

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

Definition DAG

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

Actual proof prerequisites

bounded_beta_exclusive_recode_invariant · checked external prerequisitele_refl · checked external prerequisite

Original expanded first-order statement

forall k c b e. (forall mdr_t_recode_common. (exists mdr_h_recode_common. S mdr_t_recode_common + S mdr_h_recode_common = S (k)) -> exists mdr_q_recode_common. c = S mdr_t_recode_common * mdr_q_recode_common) -> exists z. (forall mdr_i_recode_result mdr_a_recode_result. (exists mdr_gap_recode_resulti. mdr_gap_recode_resulti + S (mdr_i_recode_result) = (k)) -> (((exists ff_h_mdr_recode_resulta. ff_h_mdr_recode_resulta + S (mdr_a_recode_result) = S ((S (mdr_i_recode_result)) * e)) /\ exists ff_q_mdr_recode_resulta. b = ff_q_mdr_recode_resulta * S ((S (mdr_i_recode_result)) * e) + (mdr_a_recode_result))) -> (exists mdr_u_recode_resultm mdr_v_recode_resultm. (z) + (S ((S (mdr_i_recode_result)) * (c))) * mdr_u_recode_resultm = (mdr_a_recode_result) + (S ((S (mdr_i_recode_result)) * (c))) * mdr_v_recode_resultm))

Complete tactic proof in conservative notation

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

24 script commands · 6 reading checkpoints · 2 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–5

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

L1
intro k
L2
intro c
L3
intro b
L4
intro e
L5
intro hcommon

02Establish hallL6–12

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bounded beta exclusive recode invariant.

L6
have hall : ∀ n. Le(n,k) → ∃ x. ∃ y. ¬x = 0 ∧ ((∀ z. Lt(z,n) → ∃ m. x = S (S z · c) · m) ∧ ((∀ z. ∀ m. Lt(z,n) → BetaAt(b,e,z,m) → ∃ i. ∃ j. y + S (S z · c) · i = m + S (S z · c) · j) ∧ (∀ z. Le(n,z) → Le(z,k) → ∀ m. (∃ i. x = m · i) → (∃ i. S (S z · c) = m · i) → m = 1)))Definitions: Le(n,k)Lt(z,n)BetaAt(b,e,z,m)Le(n,z)Le(z,k)Original native command in the exact edition
L7
specialize bounded_beta_exclusive_recode_invariant (k)
L8
specialize bounded_beta_exclusive_recode_invariant (c)
L9
specialize bounded_beta_exclusive_recode_invariant (b)
L10
specialize bounded_beta_exclusive_recode_invariant (e)
L11
apply bounded_beta_exclusive_recode_invariant
L12
exact hcommon

03Establish hinvL13–17

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

L13
have hinv : ∃ P. ∃ z. ¬P = 0 ∧ ((∀ x. Lt(x,k) → ∃ y. P = S (S x · c) · y) ∧ ((∀ x. ∀ y. Lt(x,k) → BetaAt(b,e,x,y) → ∃ n. ∃ m. z + S (S x · c) · n = y + S (S x · c) · m) ∧ (∀ x. Le(k,x) → Le(x,k) → ∀ y. (∃ n. P = y · n) → (∃ n. S (S x · c) = y · n) → y = 1)))Definitions: Lt(x,k)BetaAt(b,e,x,y)Le(k,x)Le(x,k)Original native command in the exact edition
L14
specialize hall (k)
L15
apply hall
L16
specialize le_refl (k)
L17
apply le_refl

04Separate the logical casesL18–22

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

L18
cases hinv
L19
cases hinv_witness
L20
cases hinv_witness_witness
L21
cases hinv_witness_witness_right
L22
cases hinv_witness_witness_right_right

05Construct an explicit witnessL23–23

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

L23
exists x1

06Use earlier factsL24–24

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

L24
exact hinv_witness_witness_right_right_left

Library-wide reading audit

Original defined command ledger · 24 lines

0001intro k
0002intro c
0003intro b
0004intro e
0005intro hcommon
0006have hall : ∀ n. Le(n,k) → ∃ x. ∃ y. ¬x = 0 ∧ ((∀ z. Lt(z,n) → ∃ m. x = S (S z · c) · m) ∧ ((∀ z. ∀ m. Lt(z,n) → BetaAt(b,e,z,m) → ∃ i. ∃ j. y + S (S z · c) · i = m + S (S z · c) · j) ∧ (∀ z. Le(n,z) → Le(z,k) → ∀ m. (∃ i. x = m · i) → (∃ i. S (S z · c) = m · i) → m = 1)))
0007specialize bounded_beta_exclusive_recode_invariant (k)
0008specialize bounded_beta_exclusive_recode_invariant (c)
0009specialize bounded_beta_exclusive_recode_invariant (b)
0010specialize bounded_beta_exclusive_recode_invariant (e)
0011apply bounded_beta_exclusive_recode_invariant
0012exact hcommon
0013have hinv : ∃ P. ∃ z. ¬P = 0 ∧ ((∀ x. Lt(x,k) → ∃ y. P = S (S x · c) · y) ∧ ((∀ x. ∀ y. Lt(x,k) → BetaAt(b,e,x,y) → ∃ n. ∃ m. z + S (S x · c) · n = y + S (S x · c) · m) ∧ (∀ x. Le(k,x) → Le(x,k) → ∀ y. (∃ n. P = y · n) → (∃ n. S (S x · c) = y · n) → y = 1)))
0014specialize hall (k)
0015apply hall
0016specialize le_refl (k)
0017apply le_refl
0018cases hinv
0019cases hinv_witness
0020cases hinv_witness_witness
0021cases hinv_witness_witness_right
0022cases hinv_witness_witness_right_right
0023exists x1
0024exact hinv_witness_witness_right_right_left