Append one actual selected parent entry while preserving every earlier selected entry in the same new beta code.
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.
forall b c w rb rc cb cc q ub uc l a. (forall mdr_i_prefix_previous. (exists mdr_gap_prefix_previousbound. mdr_gap_prefix_previousbound + S (mdr_i_prefix_previous) = (l)) -> exists mdr_a_prefix_previous. (((exists mdr_r_prefix_previouspoint mdr_s_prefix_previouspoint mdr_u_prefix_previouspoint mdr_v_prefix_previouspoint. ((mdr_i_prefix_previous = (q) * mdr_r_prefix_previouspoint + mdr_s_prefix_previouspoint) /\ ((exists mdr_gap_prefix_previouspointcolumn. mdr_gap_prefix_previouspointcolumn + S (mdr_s_prefix_previouspoint) = (q)) /\ ((((exists ff_h_mdr_prefix_previouspointrow_index. ff_h_mdr_prefix_previouspointrow_index + S (mdr_u_prefix_previouspoint) = S ((S (mdr_r_prefix_previouspoint)) * rc)) /\ exists ff_q_mdr_prefix_previouspointrow_index. rb = ff_q_mdr_prefix_previouspointrow_index * S ((S (mdr_r_prefix_previouspoint)) * rc) + (mdr_u_prefix_previouspoint))) /\ ((((exists ff_h_mdr_prefix_previouspointcolumn_index. ff_h_mdr_prefix_previouspointcolumn_index + S (mdr_v_prefix_previouspoint) = S ((S (mdr_s_prefix_previouspoint)) * cc)) /\ exists ff_q_mdr_prefix_previouspointcolumn_index. cb = ff_q_mdr_prefix_previouspointcolumn_index * S ((S (mdr_s_prefix_previouspoint)) * cc) + (mdr_v_prefix_previouspoint))) /\ (((exists ff_h_mdr_prefix_previouspointsource. ff_h_mdr_prefix_previouspointsource + S (mdr_a_prefix_previous) = S ((S ((mdr_u_prefix_previouspoint) * (w) + (mdr_v_prefix_previouspoint))) * c)) /\ exists ff_q_mdr_prefix_previouspointsource. b = ff_q_mdr_prefix_previouspointsource * S ((S ((mdr_u_prefix_previouspoint) * (w) + (mdr_v_prefix_previouspoint))) * c) + (mdr_a_prefix_previous)))))))) /\ (((exists ff_h_mdr_prefix_previousoutput. ff_h_mdr_prefix_previousoutput + S (mdr_a_prefix_previous) = S ((S (mdr_i_prefix_previous)) * uc)) /\ exists ff_q_mdr_prefix_previousoutput. ub = ff_q_mdr_prefix_previousoutput * S ((S (mdr_i_prefix_previous)) * uc) + (mdr_a_prefix_previous)))))) -> (exists mdr_r_prefix_last mdr_s_prefix_last mdr_u_prefix_last mdr_v_prefix_last. ((l = (q) * mdr_r_prefix_last + mdr_s_prefix_last) /\ ((exists mdr_gap_prefix_lastcolumn. mdr_gap_prefix_lastcolumn + S (mdr_s_prefix_last) = (q)) /\ ((((exists ff_h_mdr_prefix_lastrow_index. ff_h_mdr_prefix_lastrow_index + S (mdr_u_prefix_last) = S ((S (mdr_r_prefix_last)) * rc)) /\ exists ff_q_mdr_prefix_lastrow_index. rb = ff_q_mdr_prefix_lastrow_index * S ((S (mdr_r_prefix_last)) * rc) + (mdr_u_prefix_last))) /\ ((((exists ff_h_mdr_prefix_lastcolumn_index. ff_h_mdr_prefix_lastcolumn_index + S (mdr_v_prefix_last) = S ((S (mdr_s_prefix_last)) * cc)) /\ exists ff_q_mdr_prefix_lastcolumn_index. cb = ff_q_mdr_prefix_lastcolumn_index * S ((S (mdr_s_prefix_last)) * cc) + (mdr_v_prefix_last))) /\ (((exists ff_h_mdr_prefix_lastsource. ff_h_mdr_prefix_lastsource + S (a) = S ((S ((mdr_u_prefix_last) * (w) + (mdr_v_prefix_last))) * c)) /\ exists ff_q_mdr_prefix_lastsource. b = ff_q_mdr_prefix_lastsource * S ((S ((mdr_u_prefix_last) * (w) + (mdr_v_prefix_last))) * c) + (a)))))))) -> exists vb vc. (forall mdr_i_prefix_successor. (exists mdr_gap_prefix_successorbound. mdr_gap_prefix_successorbound + S (mdr_i_prefix_successor) = (S l)) -> exists mdr_a_prefix_successor. (((exists mdr_r_prefix_successorpoint mdr_s_prefix_successorpoint mdr_u_prefix_successorpoint mdr_v_prefix_successorpoint. ((mdr_i_prefix_successor = (q) * mdr_r_prefix_successorpoint + mdr_s_prefix_successorpoint) /\ ((exists mdr_gap_prefix_successorpointcolumn. mdr_gap_prefix_successorpointcolumn + S (mdr_s_prefix_successorpoint) = (q)) /\ ((((exists ff_h_mdr_prefix_successorpointrow_index. ff_h_mdr_prefix_successorpointrow_index + S (mdr_u_prefix_successorpoint) = S ((S (mdr_r_prefix_successorpoint)) * rc)) /\ exists ff_q_mdr_prefix_successorpointrow_index. rb = ff_q_mdr_prefix_successorpointrow_index * S ((S (mdr_r_prefix_successorpoint)) * rc) + (mdr_u_prefix_successorpoint))) /\ ((((exists ff_h_mdr_prefix_successorpointcolumn_index. ff_h_mdr_prefix_successorpointcolumn_index + S (mdr_v_prefix_successorpoint) = S ((S (mdr_s_prefix_successorpoint)) * cc)) /\ exists ff_q_mdr_prefix_successorpointcolumn_index. cb = ff_q_mdr_prefix_successorpointcolumn_index * S ((S (mdr_s_prefix_successorpoint)) * cc) + (mdr_v_prefix_successorpoint))) /\ (((exists ff_h_mdr_prefix_successorpointsource. ff_h_mdr_prefix_successorpointsource + S (mdr_a_prefix_successor) = S ((S ((mdr_u_prefix_successorpoint) * (w) + (mdr_v_prefix_successorpoint))) * c)) /\ exists ff_q_mdr_prefix_successorpointsource. b = ff_q_mdr_prefix_successorpointsource * S ((S ((mdr_u_prefix_successorpoint) * (w) + (mdr_v_prefix_successorpoint))) * c) + (mdr_a_prefix_successor)))))))) /\ (((exists ff_h_mdr_prefix_successoroutput. ff_h_mdr_prefix_successoroutput + S (mdr_a_prefix_successor) = S ((S (mdr_i_prefix_successor)) * vc)) /\ exists ff_q_mdr_prefix_successoroutput. vb = ff_q_mdr_prefix_successoroutput * S ((S (mdr_i_prefix_successor)) * vc) + (mdr_a_prefix_successor))))))
Complete tactic proof in conservative notation
All 54 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.
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.