CE001A

signed_alternating_cofactor_fold_empty

The arbitrary signed alternating cofactor fold has the exact empty value (0,0).

Alpha v34 checked-use · first admitted v25 · 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.

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. ∀ p. ∀ n. SignedAlternatingCofactorFold(ab,ac,db,dc,eb,ec,fb,fc,0,p,n) → p = 0 ∧ n = 0

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

Definition DAG

SignedAlternatingCofactorFold(ab,ac,db,dc,eb,ec,fb,fc,l,p,n) · 1

Actual proof prerequisites

beta_sum_zero · checked external prerequisite
Original expanded first-order statement 
forall ab ac db dc eb ec fb fc p n. (exists ff_ub_mce_fold_empty ff_uc_mce_fold_empty ff_vb_mce_fold_empty ff_vc_mce_fold_empty. ((forall ff_index_mce_alternating_empty_prefix. (exists ff_gap_mce_empty_prefix_index. ff_gap_mce_empty_prefix_index + S (ff_index_mce_alternating_empty_prefix) = (0)) -> exists ff_ap_mce_alternating_empty_prefix ff_an_mce_alternating_empty_prefix ff_bp_mce_alternating_empty_prefix ff_bn_mce_alternating_empty_prefix ff_p_mce_alternating_empty_prefix ff_n_mce_alternating_empty_prefix. ((((exists ff_h_mce_empty_prefix_ap. ff_h_mce_empty_prefix_ap + S (ff_ap_mce_alternating_empty_prefix) = S ((S (ff_index_mce_alternating_empty_prefix)) * ac)) /\ exists ff_q_mce_empty_prefix_ap. ab = ff_q_mce_empty_prefix_ap * S ((S (ff_index_mce_alternating_empty_prefix)) * ac) + (ff_ap_mce_alternating_empty_prefix))) /\ ((((exists ff_h_mce_empty_prefix_an. ff_h_mce_empty_prefix_an + S (ff_an_mce_alternating_empty_prefix) = S ((S (ff_index_mce_alternating_empty_prefix)) * dc)) /\ exists ff_q_mce_empty_prefix_an. db = ff_q_mce_empty_prefix_an * S ((S (ff_index_mce_alternating_empty_prefix)) * dc) + (ff_an_mce_alternating_empty_prefix))) /\ ((((exists ff_h_mce_empty_prefix_bp. ff_h_mce_empty_prefix_bp + S (ff_bp_mce_alternating_empty_prefix) = S ((S (ff_index_mce_alternating_empty_prefix)) * ec)) /\ exists ff_q_mce_empty_prefix_bp. eb = ff_q_mce_empty_prefix_bp * S ((S (ff_index_mce_alternating_empty_prefix)) * ec) + (ff_bp_mce_alternating_empty_prefix))) /\ ((((exists ff_h_mce_empty_prefix_bn. ff_h_mce_empty_prefix_bn + S (ff_bn_mce_alternating_empty_prefix) = S ((S (ff_index_mce_alternating_empty_prefix)) * fc)) /\ exists ff_q_mce_empty_prefix_bn. fb = ff_q_mce_empty_prefix_bn * S ((S (ff_index_mce_alternating_empty_prefix)) * fc) + (ff_bn_mce_alternating_empty_prefix))) /\ ((((exists ff_h_mce_empty_prefix_positive. ff_h_mce_empty_prefix_positive + S (ff_p_mce_alternating_empty_prefix) = S ((S (ff_index_mce_alternating_empty_prefix)) * ff_uc_mce_fold_empty)) /\ exists ff_q_mce_empty_prefix_positive. ff_ub_mce_fold_empty = ff_q_mce_empty_prefix_positive * S ((S (ff_index_mce_alternating_empty_prefix)) * ff_uc_mce_fold_empty) + (ff_p_mce_alternating_empty_prefix))) /\ ((((exists ff_h_mce_empty_prefix_negative. ff_h_mce_empty_prefix_negative + S (ff_n_mce_alternating_empty_prefix) = S ((S (ff_index_mce_alternating_empty_prefix)) * ff_vc_mce_fold_empty)) /\ exists ff_q_mce_empty_prefix_negative. ff_vb_mce_fold_empty = ff_q_mce_empty_prefix_negative * S ((S (ff_index_mce_alternating_empty_prefix)) * ff_vc_mce_fold_empty) + (ff_n_mce_alternating_empty_prefix))) /\ (((exists ff_even_mce_term_empty_prefix_term. ff_index_mce_alternating_empty_prefix = 2 * ff_even_mce_term_empty_prefix_term) /\ (ff_p_mce_alternating_empty_prefix = (ff_ap_mce_alternating_empty_prefix) * (ff_bp_mce_alternating_empty_prefix) + (ff_an_mce_alternating_empty_prefix) * (ff_bn_mce_alternating_empty_prefix) /\ ff_n_mce_alternating_empty_prefix = (ff_ap_mce_alternating_empty_prefix) * (ff_bn_mce_alternating_empty_prefix) + (ff_an_mce_alternating_empty_prefix) * (ff_bp_mce_alternating_empty_prefix))) \/ ((exists ff_odd_mce_term_empty_prefix_term. ff_index_mce_alternating_empty_prefix = 2 * ff_odd_mce_term_empty_prefix_term + 1) /\ (ff_p_mce_alternating_empty_prefix = (ff_ap_mce_alternating_empty_prefix) * (ff_bn_mce_alternating_empty_prefix) + (ff_an_mce_alternating_empty_prefix) * (ff_bp_mce_alternating_empty_prefix) /\ ff_n_mce_alternating_empty_prefix = (ff_ap_mce_alternating_empty_prefix) * (ff_bp_mce_alternating_empty_prefix) + (ff_an_mce_alternating_empty_prefix) * (ff_bn_mce_alternating_empty_prefix))))))))))) /\ ((exists ff_u_mce_empty_positive ff_v_mce_empty_positive. ((((exists ff_h_mce_empty_positive_start. ff_h_mce_empty_positive_start + S (0) = S ((S (0)) * ff_v_mce_empty_positive)) /\ exists ff_q_mce_empty_positive_start. ff_u_mce_empty_positive = ff_q_mce_empty_positive_start * S ((S (0)) * ff_v_mce_empty_positive) + (0))) /\ ((((exists ff_h_mce_empty_positive_terminal. ff_h_mce_empty_positive_terminal + S (p) = S ((S ((0))) * ff_v_mce_empty_positive)) /\ exists ff_q_mce_empty_positive_terminal. ff_u_mce_empty_positive = ff_q_mce_empty_positive_terminal * S ((S ((0))) * ff_v_mce_empty_positive) + (p))) /\ forall ff_i_mce_empty_positive. (exists ff_lt_mce_empty_positive_bound. ff_lt_mce_empty_positive_bound + S ff_i_mce_empty_positive = (0)) -> exists ff_a_mce_empty_positive ff_r_mce_empty_positive ff_s_mce_empty_positive. ((((exists ff_h_mce_empty_positive_summand. ff_h_mce_empty_positive_summand + S (ff_a_mce_empty_positive) = S ((S (ff_i_mce_empty_positive)) * ff_uc_mce_fold_empty)) /\ exists ff_q_mce_empty_positive_summand. ff_ub_mce_fold_empty = ff_q_mce_empty_positive_summand * S ((S (ff_i_mce_empty_positive)) * ff_uc_mce_fold_empty) + (ff_a_mce_empty_positive))) /\ ((((exists ff_h_mce_empty_positive_partial. ff_h_mce_empty_positive_partial + S (ff_r_mce_empty_positive) = S ((S (ff_i_mce_empty_positive)) * ff_v_mce_empty_positive)) /\ exists ff_q_mce_empty_positive_partial. ff_u_mce_empty_positive = ff_q_mce_empty_positive_partial * S ((S (ff_i_mce_empty_positive)) * ff_v_mce_empty_positive) + (ff_r_mce_empty_positive))) /\ ((((exists ff_h_mce_empty_positive_successor. ff_h_mce_empty_positive_successor + S (ff_s_mce_empty_positive) = S ((S (S ff_i_mce_empty_positive)) * ff_v_mce_empty_positive)) /\ exists ff_q_mce_empty_positive_successor. ff_u_mce_empty_positive = ff_q_mce_empty_positive_successor * S ((S (S ff_i_mce_empty_positive)) * ff_v_mce_empty_positive) + (ff_s_mce_empty_positive))) /\ ff_s_mce_empty_positive = ff_r_mce_empty_positive + ff_a_mce_empty_positive)))))) /\ (exists ff_u_mce_empty_negative ff_v_mce_empty_negative. ((((exists ff_h_mce_empty_negative_start. ff_h_mce_empty_negative_start + S (0) = S ((S (0)) * ff_v_mce_empty_negative)) /\ exists ff_q_mce_empty_negative_start. ff_u_mce_empty_negative = ff_q_mce_empty_negative_start * S ((S (0)) * ff_v_mce_empty_negative) + (0))) /\ ((((exists ff_h_mce_empty_negative_terminal. ff_h_mce_empty_negative_terminal + S (n) = S ((S ((0))) * ff_v_mce_empty_negative)) /\ exists ff_q_mce_empty_negative_terminal. ff_u_mce_empty_negative = ff_q_mce_empty_negative_terminal * S ((S ((0))) * ff_v_mce_empty_negative) + (n))) /\ forall ff_i_mce_empty_negative. (exists ff_lt_mce_empty_negative_bound. ff_lt_mce_empty_negative_bound + S ff_i_mce_empty_negative = (0)) -> exists ff_a_mce_empty_negative ff_r_mce_empty_negative ff_s_mce_empty_negative. ((((exists ff_h_mce_empty_negative_summand. ff_h_mce_empty_negative_summand + S (ff_a_mce_empty_negative) = S ((S (ff_i_mce_empty_negative)) * ff_vc_mce_fold_empty)) /\ exists ff_q_mce_empty_negative_summand. ff_vb_mce_fold_empty = ff_q_mce_empty_negative_summand * S ((S (ff_i_mce_empty_negative)) * ff_vc_mce_fold_empty) + (ff_a_mce_empty_negative))) /\ ((((exists ff_h_mce_empty_negative_partial. ff_h_mce_empty_negative_partial + S (ff_r_mce_empty_negative) = S ((S (ff_i_mce_empty_negative)) * ff_v_mce_empty_negative)) /\ exists ff_q_mce_empty_negative_partial. ff_u_mce_empty_negative = ff_q_mce_empty_negative_partial * S ((S (ff_i_mce_empty_negative)) * ff_v_mce_empty_negative) + (ff_r_mce_empty_negative))) /\ ((((exists ff_h_mce_empty_negative_successor. ff_h_mce_empty_negative_successor + S (ff_s_mce_empty_negative) = S ((S (S ff_i_mce_empty_negative)) * ff_v_mce_empty_negative)) /\ exists ff_q_mce_empty_negative_successor. ff_u_mce_empty_negative = ff_q_mce_empty_negative_successor * S ((S (S ff_i_mce_empty_negative)) * ff_v_mce_empty_negative) + (ff_s_mce_empty_negative))) /\ ff_s_mce_empty_negative = ff_r_mce_empty_negative + ff_a_mce_empty_negative))))))))) -> (p = 0 /\ n = 0)

Complete unchanged native tactic proof

All 28 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

28 script commands · 4 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 ab
  2. L2
    intro ac
  3. L3
    intro db
  4. L4
    intro dc
  5. L5
    intro eb
  6. L6
    intro ec
  7. L7
    intro fb
  8. L8
    intro fc
  9. L9
    intro p
  10. L10
    intro n
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hfold
03Separate the logical casesL12–18

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

  1. L12
    cases hfold
  2. L13
    cases hfold_witness
  3. L14
    cases hfold_witness_witness
  4. L15
    cases hfold_witness_witness_witness
  5. L16
    cases hfold_witness_witness_witness_witness
  6. L17
    cases hfold_witness_witness_witness_witness_right
  7. L18
    split
04Use earlier factsL19–28

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

  1. L19
    specialize beta_sum_zero x
  2. L20
    specialize beta_sum_zero x1
  3. L21
    specialize beta_sum_zero p
  4. L22
    apply beta_sum_zero
  5. L23
    exact hfold_witness_witness_witness_witness_right_left
  6. L24
    specialize beta_sum_zero x2
  7. L25
    specialize beta_sum_zero x3
  8. L26
    specialize beta_sum_zero n
  9. L27
    apply beta_sum_zero
  10. L28
    exact hfold_witness_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 28 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro db
  4. 0004intro dc
  5. 0005intro eb
  6. 0006intro ec
  7. 0007intro fb
  8. 0008intro fc
  9. 0009intro p
  10. 0010intro n
  11. 0011intro hfold
  12. 0012cases hfold
  13. 0013cases hfold_witness
  14. 0014cases hfold_witness_witness
  15. 0015cases hfold_witness_witness_witness
  16. 0016cases hfold_witness_witness_witness_witness
  17. 0017cases hfold_witness_witness_witness_witness_right
  18. 0018split
  19. 0019specialize beta_sum_zero x
  20. 0020specialize beta_sum_zero x1
  21. 0021specialize beta_sum_zero p
  22. 0022apply beta_sum_zero
  23. 0023exact hfold_witness_witness_witness_witness_right_left
  24. 0024specialize beta_sum_zero x2
  25. 0025specialize beta_sum_zero x3
  26. 0026specialize beta_sum_zero n
  27. 0027apply beta_sum_zero
  28. 0028exact hfold_witness_witness_witness_witness_right_right