CE0014

signed_alternating_product_prefix_restrict

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

An exact signed alternating cofactor prefix of successor length restricts to its genuine earlier prefix.

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.

Exact expanded first-order arithmetic 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)))))))))))

Constructive proof overview

Generated structural guide

An exact signed alternating cofactor prefix of successor length restricts to its genuine earlier prefix.

The unchanged tactic script uses 1 declared prerequisite and contains 22 exact native proof lines.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

le_succ Stable theorem; checked-use authorized

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 ub
  10. L10
    intro uc
02Fix variables and assumptionsL11–16

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

  1. L11
    intro vb
  2. L12
    intro vc
  3. L13
    intro l
  4. L14
    intro hprefix
  5. L15
    intro i
  6. L16
    intro hi
03Use earlier factsL17–22

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

  1. L17
    specialize hprefix i
  2. L18
    apply hprefix
  3. L19
    specialize le_succ (S i)
  4. L20
    specialize le_succ l
  5. L21
    apply le_succ
  6. L22
    exact hi

Library-wide reading audit

Original exact command ledger · 22 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 ub
  10. 0010intro uc
  11. 0011intro vb
  12. 0012intro vc
  13. 0013intro l
  14. 0014intro hprefix
  15. 0015intro i
  16. 0016intro hi
  17. 0017specialize hprefix i
  18. 0018apply hprefix
  19. 0019specialize le_succ (S i)
  20. 0020specialize le_succ l
  21. 0021apply le_succ
  22. 0022exact hi

Separate complete second-wave branches: Full T13 proof · Alpha v27.