CE0013

signed_alternating_product_prefix_exists

Every arbitrary finite signed row and signed cofactor-value stream has complete beta-coded positive and negative alternating-product streams.

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. ∀ l. ∃ ub. ∃ uc. ∃ vb. ∃ vc. 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) · 1

Actual proof prerequisites

beta_at_exists · checked external prerequisitesigned_alternating_cofactor_term_existssigned_alternating_product_prefix_emptysigned_alternating_product_prefix_extend
Original expanded first-order statement 
forall ab ac db dc eb ec fb fc l. exists ub uc vb vc. (forall ff_index_mce_alternating_existence. (exists ff_gap_mce_existence_index. ff_gap_mce_existence_index + S (ff_index_mce_alternating_existence) = (l)) -> exists ff_ap_mce_alternating_existence ff_an_mce_alternating_existence ff_bp_mce_alternating_existence ff_bn_mce_alternating_existence ff_p_mce_alternating_existence ff_n_mce_alternating_existence. ((((exists ff_h_mce_existence_ap. ff_h_mce_existence_ap + S (ff_ap_mce_alternating_existence) = S ((S (ff_index_mce_alternating_existence)) * ac)) /\ exists ff_q_mce_existence_ap. ab = ff_q_mce_existence_ap * S ((S (ff_index_mce_alternating_existence)) * ac) + (ff_ap_mce_alternating_existence))) /\ ((((exists ff_h_mce_existence_an. ff_h_mce_existence_an + S (ff_an_mce_alternating_existence) = S ((S (ff_index_mce_alternating_existence)) * dc)) /\ exists ff_q_mce_existence_an. db = ff_q_mce_existence_an * S ((S (ff_index_mce_alternating_existence)) * dc) + (ff_an_mce_alternating_existence))) /\ ((((exists ff_h_mce_existence_bp. ff_h_mce_existence_bp + S (ff_bp_mce_alternating_existence) = S ((S (ff_index_mce_alternating_existence)) * ec)) /\ exists ff_q_mce_existence_bp. eb = ff_q_mce_existence_bp * S ((S (ff_index_mce_alternating_existence)) * ec) + (ff_bp_mce_alternating_existence))) /\ ((((exists ff_h_mce_existence_bn. ff_h_mce_existence_bn + S (ff_bn_mce_alternating_existence) = S ((S (ff_index_mce_alternating_existence)) * fc)) /\ exists ff_q_mce_existence_bn. fb = ff_q_mce_existence_bn * S ((S (ff_index_mce_alternating_existence)) * fc) + (ff_bn_mce_alternating_existence))) /\ ((((exists ff_h_mce_existence_positive. ff_h_mce_existence_positive + S (ff_p_mce_alternating_existence) = S ((S (ff_index_mce_alternating_existence)) * uc)) /\ exists ff_q_mce_existence_positive. ub = ff_q_mce_existence_positive * S ((S (ff_index_mce_alternating_existence)) * uc) + (ff_p_mce_alternating_existence))) /\ ((((exists ff_h_mce_existence_negative. ff_h_mce_existence_negative + S (ff_n_mce_alternating_existence) = S ((S (ff_index_mce_alternating_existence)) * vc)) /\ exists ff_q_mce_existence_negative. vb = ff_q_mce_existence_negative * S ((S (ff_index_mce_alternating_existence)) * vc) + (ff_n_mce_alternating_existence))) /\ (((exists ff_even_mce_term_existence_term. ff_index_mce_alternating_existence = 2 * ff_even_mce_term_existence_term) /\ (ff_p_mce_alternating_existence = (ff_ap_mce_alternating_existence) * (ff_bp_mce_alternating_existence) + (ff_an_mce_alternating_existence) * (ff_bn_mce_alternating_existence) /\ ff_n_mce_alternating_existence = (ff_ap_mce_alternating_existence) * (ff_bn_mce_alternating_existence) + (ff_an_mce_alternating_existence) * (ff_bp_mce_alternating_existence))) \/ ((exists ff_odd_mce_term_existence_term. ff_index_mce_alternating_existence = 2 * ff_odd_mce_term_existence_term + 1) /\ (ff_p_mce_alternating_existence = (ff_ap_mce_alternating_existence) * (ff_bn_mce_alternating_existence) + (ff_an_mce_alternating_existence) * (ff_bp_mce_alternating_existence) /\ ff_n_mce_alternating_existence = (ff_ap_mce_alternating_existence) * (ff_bp_mce_alternating_existence) + (ff_an_mce_alternating_existence) * (ff_bn_mce_alternating_existence)))))))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

89 script commands · 19 reading checkpoints · 5 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.

Named ingredients (3)
signed alternating product prefix emptysigned alternating cofactor term existssigned alternating product prefix extend
01Fix variables and assumptionsL1–8

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
02Induction on lL9–9

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L9
    induction l
03Construct an explicit witnessL10–13

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

  1. L10
    exists 0
  2. L11
    exists 0
  3. L12
    exists 0
  4. L13
    exists 0
04Use earlier factsL14–23

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

  1. L14
    specialize signed_alternating_product_prefix_empty ab
  2. L15
    specialize signed_alternating_product_prefix_empty ac
  3. L16
    specialize signed_alternating_product_prefix_empty db
  4. L17
    specialize signed_alternating_product_prefix_empty dc
  5. L18
    specialize signed_alternating_product_prefix_empty eb
  6. L19
    specialize signed_alternating_product_prefix_empty ec
  7. L20
    specialize signed_alternating_product_prefix_empty fb
  8. L21
    specialize signed_alternating_product_prefix_empty fc
  9. L22
    specialize signed_alternating_product_prefix_empty 0
  10. L23
    specialize signed_alternating_product_prefix_empty 0
05Use earlier factsL24–26

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

  1. L24
    specialize signed_alternating_product_prefix_empty 0
  2. L25
    specialize signed_alternating_product_prefix_empty 0
  3. L26
    exact signed_alternating_product_prefix_empty
06Separate the logical casesL27–30

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

  1. L27
    cases IH
  2. L28
    cases IH_witness
  3. L29
    cases IH_witness_witness
  4. L30
    cases IH_witness_witness_witness
07Establish hapL31–35

Establish this local claim before using it. It is not an additional assumption.

  1. L31
    have hap : exists a. (((exists ff_h_mce_exists_ap. ff_h_mce_exists_ap + S (a) = S ((S (l)) * ac)) /\ exists ff_q_mce_exists_ap. ab = ff_q_mce_exists_ap * S ((S (l)) * ac) + (a)))
  2. L32
    specialize beta_at_exists ab
  3. L33
    specialize beta_at_exists ac
  4. L34
    specialize beta_at_exists l
  5. L35
    exact beta_at_exists
08Separate the logical casesL36–36

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

  1. L36
    cases hap
09Establish hanL37–41

Establish this local claim before using it. It is not an additional assumption.

  1. L37
    have han : exists a. (((exists ff_h_mce_exists_an. ff_h_mce_exists_an + S (a) = S ((S (l)) * dc)) /\ exists ff_q_mce_exists_an. db = ff_q_mce_exists_an * S ((S (l)) * dc) + (a)))
  2. L38
    specialize beta_at_exists db
  3. L39
    specialize beta_at_exists dc
  4. L40
    specialize beta_at_exists l
  5. L41
    exact beta_at_exists
10Separate the logical casesL42–42

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

  1. L42
    cases han
11Establish hbpL43–47

Establish this local claim before using it. It is not an additional assumption.

  1. L43
    have hbp : exists a. (((exists ff_h_mce_exists_bp. ff_h_mce_exists_bp + S (a) = S ((S (l)) * ec)) /\ exists ff_q_mce_exists_bp. eb = ff_q_mce_exists_bp * S ((S (l)) * ec) + (a)))
  2. L44
    specialize beta_at_exists eb
  3. L45
    specialize beta_at_exists ec
  4. L46
    specialize beta_at_exists l
  5. L47
    exact beta_at_exists
12Separate the logical casesL48–48

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

  1. L48
    cases hbp
13Establish hbnL49–53

Establish this local claim before using it. It is not an additional assumption.

  1. L49
    have hbn : exists a. (((exists ff_h_mce_exists_bn. ff_h_mce_exists_bn + S (a) = S ((S (l)) * fc)) /\ exists ff_q_mce_exists_bn. fb = ff_q_mce_exists_bn * S ((S (l)) * fc) + (a)))
  2. L50
    specialize beta_at_exists fb
  3. L51
    specialize beta_at_exists fc
  4. L52
    specialize beta_at_exists l
  5. L53
    exact beta_at_exists
14Separate the logical casesL54–54

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

  1. L54
    cases hbn
15Establish htermL55–61

Establish this local claim before using it. It is not an additional assumption.

  1. L55
    have hterm : exists p n. (((exists ff_even_mce_term_exists_term. l = 2 * ff_even_mce_term_exists_term) /\ (p = (x4) * (x6) + (x5) * (x7) /\ n = (x4) * (x7) + (x5) * (x6))) \/ ((exists ff_odd_mce_term_exists_term. l = 2 * ff_odd_mce_term_exists_term + 1) /\ (p = (x4) * (x7) + (x5) * (x6) /\ n = (x4) * (x6) + (x5) * (x7))))
  2. L56
    specialize signed_alternating_cofactor_term_exists x4
  3. L57
    specialize signed_alternating_cofactor_term_exists x5
  4. L58
    specialize signed_alternating_cofactor_term_exists x6
  5. L59
    specialize signed_alternating_cofactor_term_exists x7
  6. L60
    specialize signed_alternating_cofactor_term_exists l
  7. L61
    exact signed_alternating_cofactor_term_exists
16Separate the logical casesL62–63

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

  1. L62
    cases hterm
  2. L63
    cases hterm_witness
17Use earlier factsL64–73

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

  1. L64
    specialize signed_alternating_product_prefix_extend ab
  2. L65
    specialize signed_alternating_product_prefix_extend ac
  3. L66
    specialize signed_alternating_product_prefix_extend db
  4. L67
    specialize signed_alternating_product_prefix_extend dc
  5. L68
    specialize signed_alternating_product_prefix_extend eb
  6. L69
    specialize signed_alternating_product_prefix_extend ec
  7. L70
    specialize signed_alternating_product_prefix_extend fb
  8. L71
    specialize signed_alternating_product_prefix_extend fc
  9. L72
    specialize signed_alternating_product_prefix_extend x
  10. L73
    specialize signed_alternating_product_prefix_extend x1
18Use earlier factsL74–83

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

  1. L74
    specialize signed_alternating_product_prefix_extend x2
  2. L75
    specialize signed_alternating_product_prefix_extend x3
  3. L76
    specialize signed_alternating_product_prefix_extend l
  4. L77
    specialize signed_alternating_product_prefix_extend x4
  5. L78
    specialize signed_alternating_product_prefix_extend x5
  6. L79
    specialize signed_alternating_product_prefix_extend x6
  7. L80
    specialize signed_alternating_product_prefix_extend x7
  8. L81
    specialize signed_alternating_product_prefix_extend x8
  9. L82
    specialize signed_alternating_product_prefix_extend x9
  10. L83
    apply signed_alternating_product_prefix_extend
19Use earlier factsL84–89

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

  1. L84
    exact IH_witness_witness_witness_witness
  2. L85
    exact hap_witness
  3. L86
    exact han_witness
  4. L87
    exact hbp_witness
  5. L88
    exact hbn_witness
  6. L89
    exact hterm_witness_witness

Library-wide reading audit

Original defined command ledger · 89 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. 0009induction l
  10. 0010exists 0
  11. 0011exists 0
  12. 0012exists 0
  13. 0013exists 0
  14. 0014specialize signed_alternating_product_prefix_empty ab
  15. 0015specialize signed_alternating_product_prefix_empty ac
  16. 0016specialize signed_alternating_product_prefix_empty db
  17. 0017specialize signed_alternating_product_prefix_empty dc
  18. 0018specialize signed_alternating_product_prefix_empty eb
  19. 0019specialize signed_alternating_product_prefix_empty ec
  20. 0020specialize signed_alternating_product_prefix_empty fb
  21. 0021specialize signed_alternating_product_prefix_empty fc
  22. 0022specialize signed_alternating_product_prefix_empty 0
  23. 0023specialize signed_alternating_product_prefix_empty 0
  24. 0024specialize signed_alternating_product_prefix_empty 0
  25. 0025specialize signed_alternating_product_prefix_empty 0
  26. 0026exact signed_alternating_product_prefix_empty
  27. 0027cases IH
  28. 0028cases IH_witness
  29. 0029cases IH_witness_witness
  30. 0030cases IH_witness_witness_witness
  31. 0031have hap : exists a. (((exists ff_h_mce_exists_ap. ff_h_mce_exists_ap + S (a) = S ((S (l)) * ac)) /\ exists ff_q_mce_exists_ap. ab = ff_q_mce_exists_ap * S ((S (l)) * ac) + (a)))
  32. 0032specialize beta_at_exists ab
  33. 0033specialize beta_at_exists ac
  34. 0034specialize beta_at_exists l
  35. 0035exact beta_at_exists
  36. 0036cases hap
  37. 0037have han : exists a. (((exists ff_h_mce_exists_an. ff_h_mce_exists_an + S (a) = S ((S (l)) * dc)) /\ exists ff_q_mce_exists_an. db = ff_q_mce_exists_an * S ((S (l)) * dc) + (a)))
  38. 0038specialize beta_at_exists db
  39. 0039specialize beta_at_exists dc
  40. 0040specialize beta_at_exists l
  41. 0041exact beta_at_exists
  42. 0042cases han
  43. 0043have hbp : exists a. (((exists ff_h_mce_exists_bp. ff_h_mce_exists_bp + S (a) = S ((S (l)) * ec)) /\ exists ff_q_mce_exists_bp. eb = ff_q_mce_exists_bp * S ((S (l)) * ec) + (a)))
  44. 0044specialize beta_at_exists eb
  45. 0045specialize beta_at_exists ec
  46. 0046specialize beta_at_exists l
  47. 0047exact beta_at_exists
  48. 0048cases hbp
  49. 0049have hbn : exists a. (((exists ff_h_mce_exists_bn. ff_h_mce_exists_bn + S (a) = S ((S (l)) * fc)) /\ exists ff_q_mce_exists_bn. fb = ff_q_mce_exists_bn * S ((S (l)) * fc) + (a)))
  50. 0050specialize beta_at_exists fb
  51. 0051specialize beta_at_exists fc
  52. 0052specialize beta_at_exists l
  53. 0053exact beta_at_exists
  54. 0054cases hbn
  55. 0055have hterm : exists p n. (((exists ff_even_mce_term_exists_term. l = 2 * ff_even_mce_term_exists_term) /\ (p = (x4) * (x6) + (x5) * (x7) /\ n = (x4) * (x7) + (x5) * (x6))) \/ ((exists ff_odd_mce_term_exists_term. l = 2 * ff_odd_mce_term_exists_term + 1) /\ (p = (x4) * (x7) + (x5) * (x6) /\ n = (x4) * (x6) + (x5) * (x7))))
  56. 0056specialize signed_alternating_cofactor_term_exists x4
  57. 0057specialize signed_alternating_cofactor_term_exists x5
  58. 0058specialize signed_alternating_cofactor_term_exists x6
  59. 0059specialize signed_alternating_cofactor_term_exists x7
  60. 0060specialize signed_alternating_cofactor_term_exists l
  61. 0061exact signed_alternating_cofactor_term_exists
  62. 0062cases hterm
  63. 0063cases hterm_witness
  64. 0064specialize signed_alternating_product_prefix_extend ab
  65. 0065specialize signed_alternating_product_prefix_extend ac
  66. 0066specialize signed_alternating_product_prefix_extend db
  67. 0067specialize signed_alternating_product_prefix_extend dc
  68. 0068specialize signed_alternating_product_prefix_extend eb
  69. 0069specialize signed_alternating_product_prefix_extend ec
  70. 0070specialize signed_alternating_product_prefix_extend fb
  71. 0071specialize signed_alternating_product_prefix_extend fc
  72. 0072specialize signed_alternating_product_prefix_extend x
  73. 0073specialize signed_alternating_product_prefix_extend x1
  74. 0074specialize signed_alternating_product_prefix_extend x2
  75. 0075specialize signed_alternating_product_prefix_extend x3
  76. 0076specialize signed_alternating_product_prefix_extend l
  77. 0077specialize signed_alternating_product_prefix_extend x4
  78. 0078specialize signed_alternating_product_prefix_extend x5
  79. 0079specialize signed_alternating_product_prefix_extend x6
  80. 0080specialize signed_alternating_product_prefix_extend x7
  81. 0081specialize signed_alternating_product_prefix_extend x8
  82. 0082specialize signed_alternating_product_prefix_extend x9
  83. 0083apply signed_alternating_product_prefix_extend
  84. 0084exact IH_witness_witness_witness_witness
  85. 0085exact hap_witness
  86. 0086exact han_witness
  87. 0087exact hbp_witness
  88. 0088exact hbn_witness
  89. 0089exact hterm_witness_witness