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 .
Historical partial components only: this chapter proves genuine signed first-row minors and unique alternating folds, with supplied cofactor values. T13 is now closed in the separate Alpha-v27 integer-linear-algebra branch with actual arbitrary determinant data, rank, and integer column spans; lattice index and normal forms are not claimed. Full T13 proof · Alpha v27
Exact theorem in conservative defined notation
∀ ab. ∀ ac. ∀ db. ∀ dc. ∀ eb. ∀ ec. ∀ fb. ∀ fc. ∀ ub. ∀ uc. ∀ vb. ∀ vc. ∀ l. SignedAlternatingProductPrefix(ab,ac,db,dc,eb,ec,fb,fc,ub,uc,vb,vc,S l) → SignedAlternatingProductPrefix(ab,ac,db,dc,eb,ec,fb,fc,ub,uc,vb,vc,l) Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG SignedAlternatingProductPrefix(ab,ac,db,dc,eb,ec,fb,fc,ub,uc,vb,vc,l) · 2 Actual proof prerequisites le_succ · checked external prerequisite
Original expanded first-order statement
forall ab ac db dc eb ec fb fc ub uc vb vc l. (forall ff_index_mce_alternating_successor. (exists ff_gap_mce_successor_index. ff_gap_mce_successor_index + S (ff_index_mce_alternating_successor) = (S l)) -> exists ff_ap_mce_alternating_successor ff_an_mce_alternating_successor ff_bp_mce_alternating_successor ff_bn_mce_alternating_successor ff_p_mce_alternating_successor ff_n_mce_alternating_successor. ((((exists ff_h_mce_successor_ap. ff_h_mce_successor_ap + S (ff_ap_mce_alternating_successor) = S ((S (ff_index_mce_alternating_successor)) * ac)) /\ exists ff_q_mce_successor_ap. ab = ff_q_mce_successor_ap * S ((S (ff_index_mce_alternating_successor)) * ac) + (ff_ap_mce_alternating_successor))) /\ ((((exists ff_h_mce_successor_an. ff_h_mce_successor_an + S (ff_an_mce_alternating_successor) = S ((S (ff_index_mce_alternating_successor)) * dc)) /\ exists ff_q_mce_successor_an. db = ff_q_mce_successor_an * S ((S (ff_index_mce_alternating_successor)) * dc) + (ff_an_mce_alternating_successor))) /\ ((((exists ff_h_mce_successor_bp. ff_h_mce_successor_bp + S (ff_bp_mce_alternating_successor) = S ((S (ff_index_mce_alternating_successor)) * ec)) /\ exists ff_q_mce_successor_bp. eb = ff_q_mce_successor_bp * S ((S (ff_index_mce_alternating_successor)) * ec) + (ff_bp_mce_alternating_successor))) /\ ((((exists ff_h_mce_successor_bn. ff_h_mce_successor_bn + S (ff_bn_mce_alternating_successor) = S ((S (ff_index_mce_alternating_successor)) * fc)) /\ exists ff_q_mce_successor_bn. fb = ff_q_mce_successor_bn * S ((S (ff_index_mce_alternating_successor)) * fc) + (ff_bn_mce_alternating_successor))) /\ ((((exists ff_h_mce_successor_positive. ff_h_mce_successor_positive + S (ff_p_mce_alternating_successor) = S ((S (ff_index_mce_alternating_successor)) * uc)) /\ exists ff_q_mce_successor_positive. ub = ff_q_mce_successor_positive * S ((S (ff_index_mce_alternating_successor)) * uc) + (ff_p_mce_alternating_successor))) /\ ((((exists ff_h_mce_successor_negative. ff_h_mce_successor_negative + S (ff_n_mce_alternating_successor) = S ((S (ff_index_mce_alternating_successor)) * vc)) /\ exists ff_q_mce_successor_negative. vb = ff_q_mce_successor_negative * S ((S (ff_index_mce_alternating_successor)) * vc) + (ff_n_mce_alternating_successor))) /\ (((exists ff_even_mce_term_successor_term. ff_index_mce_alternating_successor = 2 * ff_even_mce_term_successor_term) /\ (ff_p_mce_alternating_successor = (ff_ap_mce_alternating_successor) * (ff_bp_mce_alternating_successor) + (ff_an_mce_alternating_successor) * (ff_bn_mce_alternating_successor) /\ ff_n_mce_alternating_successor = (ff_ap_mce_alternating_successor) * (ff_bn_mce_alternating_successor) + (ff_an_mce_alternating_successor) * (ff_bp_mce_alternating_successor))) \/ ((exists ff_odd_mce_term_successor_term. ff_index_mce_alternating_successor = 2 * ff_odd_mce_term_successor_term + 1) /\ (ff_p_mce_alternating_successor = (ff_ap_mce_alternating_successor) * (ff_bn_mce_alternating_successor) + (ff_an_mce_alternating_successor) * (ff_bp_mce_alternating_successor) /\ ff_n_mce_alternating_successor = (ff_ap_mce_alternating_successor) * (ff_bp_mce_alternating_successor) + (ff_an_mce_alternating_successor) * (ff_bn_mce_alternating_successor))))))))))) -> (forall ff_index_mce_alternating_restricted. (exists ff_gap_mce_restricted_index. ff_gap_mce_restricted_index + S (ff_index_mce_alternating_restricted) = (l)) -> exists ff_ap_mce_alternating_restricted ff_an_mce_alternating_restricted ff_bp_mce_alternating_restricted ff_bn_mce_alternating_restricted ff_p_mce_alternating_restricted ff_n_mce_alternating_restricted. ((((exists ff_h_mce_restricted_ap. ff_h_mce_restricted_ap + S (ff_ap_mce_alternating_restricted) = S ((S (ff_index_mce_alternating_restricted)) * ac)) /\ exists ff_q_mce_restricted_ap. ab = ff_q_mce_restricted_ap * S ((S (ff_index_mce_alternating_restricted)) * ac) + (ff_ap_mce_alternating_restricted))) /\ ((((exists ff_h_mce_restricted_an. ff_h_mce_restricted_an + S (ff_an_mce_alternating_restricted) = S ((S (ff_index_mce_alternating_restricted)) * dc)) /\ exists ff_q_mce_restricted_an. db = ff_q_mce_restricted_an * S ((S (ff_index_mce_alternating_restricted)) * dc) + (ff_an_mce_alternating_restricted))) /\ ((((exists ff_h_mce_restricted_bp. ff_h_mce_restricted_bp + S (ff_bp_mce_alternating_restricted) = S ((S (ff_index_mce_alternating_restricted)) * ec)) /\ exists ff_q_mce_restricted_bp. eb = ff_q_mce_restricted_bp * S ((S (ff_index_mce_alternating_restricted)) * ec) + (ff_bp_mce_alternating_restricted))) /\ ((((exists ff_h_mce_restricted_bn. ff_h_mce_restricted_bn + S (ff_bn_mce_alternating_restricted) = S ((S (ff_index_mce_alternating_restricted)) * fc)) /\ exists ff_q_mce_restricted_bn. fb = ff_q_mce_restricted_bn * S ((S (ff_index_mce_alternating_restricted)) * fc) + (ff_bn_mce_alternating_restricted))) /\ ((((exists ff_h_mce_restricted_positive. ff_h_mce_restricted_positive + S (ff_p_mce_alternating_restricted) = S ((S (ff_index_mce_alternating_restricted)) * uc)) /\ exists ff_q_mce_restricted_positive. ub = ff_q_mce_restricted_positive * S ((S (ff_index_mce_alternating_restricted)) * uc) + (ff_p_mce_alternating_restricted))) /\ ((((exists ff_h_mce_restricted_negative. ff_h_mce_restricted_negative + S (ff_n_mce_alternating_restricted) = S ((S (ff_index_mce_alternating_restricted)) * vc)) /\ exists ff_q_mce_restricted_negative. vb = ff_q_mce_restricted_negative * S ((S (ff_index_mce_alternating_restricted)) * vc) + (ff_n_mce_alternating_restricted))) /\ (((exists ff_even_mce_term_restricted_term. ff_index_mce_alternating_restricted = 2 * ff_even_mce_term_restricted_term) /\ (ff_p_mce_alternating_restricted = (ff_ap_mce_alternating_restricted) * (ff_bp_mce_alternating_restricted) + (ff_an_mce_alternating_restricted) * (ff_bn_mce_alternating_restricted) /\ ff_n_mce_alternating_restricted = (ff_ap_mce_alternating_restricted) * (ff_bn_mce_alternating_restricted) + (ff_an_mce_alternating_restricted) * (ff_bp_mce_alternating_restricted))) \/ ((exists ff_odd_mce_term_restricted_term. ff_index_mce_alternating_restricted = 2 * ff_odd_mce_term_restricted_term + 1) /\ (ff_p_mce_alternating_restricted = (ff_ap_mce_alternating_restricted) * (ff_bn_mce_alternating_restricted) + (ff_an_mce_alternating_restricted) * (ff_bp_mce_alternating_restricted) /\ ff_n_mce_alternating_restricted = (ff_ap_mce_alternating_restricted) * (ff_bp_mce_alternating_restricted) + (ff_an_mce_alternating_restricted) * (ff_bn_mce_alternating_restricted)))))))))))Complete unchanged native tactic proof
All 22 lines are the exact independently kernel-checked original 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.
Expand checkpoints Collapse checkpoints Show original steps Find a step
01 Fix variables and assumptions L1–10 Work with arbitrary variables or the premises of the current implication.
L1 intro ab
L2 intro ac
L3 intro db
L4 intro dc
L5 intro eb
L6 intro ec
L7 intro fb
L8 intro fc
L9 intro ub
L10 intro uc
02 Fix variables and assumptions L11–16 Work with arbitrary variables or the premises of the current implication.
L11 intro vb
L12 intro vc
L13 intro l
L14 intro hprefix
L15 intro i
L16 intro hi
03 Use earlier facts L17–22 Instantiate or apply named facts and discharge the corresponding proof obligations.
L17 specialize hprefix i
L18 apply hprefix
L19 specialize le_succ (S i)
L20 specialize le_succ l
L21 apply le_succ
L22 exact hi
Library-wide reading audit
Original defined command ledger · 22 lines 0001 intro ab0002 intro ac0003 intro db0004 intro dc0005 intro eb0006 intro ec0007 intro fb0008 intro fc0009 intro ub0010 intro uc0011 intro vb0012 intro vc0013 intro l0014 intro hprefix0015 intro i0016 intro hi0017 specialize hprefix i0018 apply hprefix0019 specialize le_succ (S i)0020 specialize le_succ l0021 apply le_succ0022 exact hi