SS0019

divisor_signed_table_reindex_data_exists

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Two real finite beta compositions are constructed before any permutation argument; no supplied composed table is assumed.

Exact expanded first-order arithmetic statement

forall pb pc nb nc r s l. exists qb qc mb mc. (((forall fms_i_datapositive fms_j_datapositive fms_v_datapositive. (exists fms_gap_datapositive. fms_gap_datapositive + S (fms_i_datapositive) = (l)) -> (((exists fs_h_fms_datapositive_index. fs_h_fms_datapositive_index + S (fms_j_datapositive) = S ((S (fms_i_datapositive)) * s)) /\ exists fs_q_fms_datapositive_index. r = fs_q_fms_datapositive_index * S ((S (fms_i_datapositive)) * s) + (fms_j_datapositive))) -> (((exists fs_h_fms_datapositive_source. fs_h_fms_datapositive_source + S (fms_v_datapositive) = S ((S (fms_j_datapositive)) * pc)) /\ exists fs_q_fms_datapositive_source. pb = fs_q_fms_datapositive_source * S ((S (fms_j_datapositive)) * pc) + (fms_v_datapositive))) -> (((exists fs_h_fms_datapositive_target. fs_h_fms_datapositive_target + S (fms_v_datapositive) = S ((S (fms_i_datapositive)) * qc)) /\ exists fs_q_fms_datapositive_target. qb = fs_q_fms_datapositive_target * S ((S (fms_i_datapositive)) * qc) + (fms_v_datapositive)))) /\ (forall fms_i_datanegative fms_j_datanegative fms_v_datanegative. (exists fms_gap_datanegative. fms_gap_datanegative + S (fms_i_datanegative) = (l)) -> (((exists fs_h_fms_datanegative_index. fs_h_fms_datanegative_index + S (fms_j_datanegative) = S ((S (fms_i_datanegative)) * s)) /\ exists fs_q_fms_datanegative_index. r = fs_q_fms_datanegative_index * S ((S (fms_i_datanegative)) * s) + (fms_j_datanegative))) -> (((exists fs_h_fms_datanegative_source. fs_h_fms_datanegative_source + S (fms_v_datanegative) = S ((S (fms_j_datanegative)) * nc)) /\ exists fs_q_fms_datanegative_source. nb = fs_q_fms_datanegative_source * S ((S (fms_j_datanegative)) * nc) + (fms_v_datanegative))) -> (((exists fs_h_fms_datanegative_target. fs_h_fms_datanegative_target + S (fms_v_datanegative) = S ((S (fms_i_datanegative)) * mc)) /\ exists fs_q_fms_datanegative_target. mb = fs_q_fms_datanegative_target * S ((S (fms_i_datanegative)) * mc) + (fms_v_datanegative))))))

Constructive proof overview

Generated structural guide

Two real finite beta compositions are constructed before any permutation argument; no supplied composed table is assumed.

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Proof neighborhood

Direct dependencies

finite_beta_composition_exists Alpha theorem; checked-use authorized

Direct dependents

SS001B divisor_signed_table_reindex_exists SS001E divisor_signed_sum_permutation_invariant

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. The literal dependency-closed bundle is checked by original HA and the independently compiled Lean verifier. Public delivery grants no Alpha checked-use authority or Stable membership.

Read the argument

Proof checkpoints

32 script commands · 8 reading checkpoints · 2 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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–7

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

  1. L1
    intro pb
  2. L2
    intro pc
  3. L3
    intro nb
  4. L4
    intro nc
  5. L5
    intro r
  6. L6
    intro s
  7. L7
    intro l
02Establish hpL8–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite beta composition exists.

  1. L8
    have hp : ∃ q. ∃ c. ∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(r,s,x,y) → BetaAt(pb,pc,y,z) → BetaAt(q,c,x,z)Definitions: LtBetaAt
  2. L9
    specialize finite_beta_composition_exists (r)
  3. L10
    specialize finite_beta_composition_exists (s)
  4. L11
    specialize finite_beta_composition_exists (pb)
  5. L12
    specialize finite_beta_composition_exists (pc)
  6. L13
    specialize finite_beta_composition_exists (l)
  7. L14
    apply finite_beta_composition_exists
03Separate the logical casesL15–16

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

  1. L15
    cases hp
  2. L16
    cases hp_witness
04Establish hnL17–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite beta composition exists.

  1. L17
    have hn : ∃ m. ∃ c. ∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(r,s,x,y) → BetaAt(nb,nc,y,z) → BetaAt(m,c,x,z)Definitions: LtBetaAt
  2. L18
    specialize finite_beta_composition_exists (r)
  3. L19
    specialize finite_beta_composition_exists (s)
  4. L20
    specialize finite_beta_composition_exists (nb)
  5. L21
    specialize finite_beta_composition_exists (nc)
  6. L22
    specialize finite_beta_composition_exists (l)
  7. L23
    apply finite_beta_composition_exists
05Separate the logical casesL24–25

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

  1. L24
    cases hn
  2. L25
    cases hn_witness
06Construct an explicit witnessL26–29

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

  1. L26
    exists x
  2. L27
    exists x1
  3. L28
    exists x2
  4. L29
    exists x3
07Separate the logical casesL30–30

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

  1. L30
    split
08Use earlier factsL31–32

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

  1. L31
    exact hp_witness_witness
  2. L32
    exact hn_witness_witness

Library-wide reading audit

Original exact command ledger · 32 lines
  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro nb
  4. 0004intro nc
  5. 0005intro r
  6. 0006intro s
  7. 0007intro l
  8. 0008have hp : exists q c. (forall fms_i_data_first fms_j_data_first fms_v_data_first. (exists fms_gap_data_first. fms_gap_data_first + S (fms_i_data_first) = (l)) -> (((exists fs_h_fms_data_first_index. fs_h_fms_data_first_index + S (fms_j_data_first) = S ((S (fms_i_data_first)) * s)) /\ exists fs_q_fms_data_first_index. r = fs_q_fms_data_first_index * S ((S (fms_i_data_first)) * s) + (fms_j_data_first))) -> (((exists fs_h_fms_data_first_source. fs_h_fms_data_first_source + S (fms_v_data_first) = S ((S (fms_j_data_first)) * pc)) /\ exists fs_q_fms_data_first_source. pb = fs_q_fms_data_first_source * S ((S (fms_j_data_first)) * pc) + (fms_v_data_first))) -> (((exists fs_h_fms_data_first_target. fs_h_fms_data_first_target + S (fms_v_data_first) = S ((S (fms_i_data_first)) * c)) /\ exists fs_q_fms_data_first_target. q = fs_q_fms_data_first_target * S ((S (fms_i_data_first)) * c) + (fms_v_data_first))))
  9. 0009specialize finite_beta_composition_exists (r)
  10. 0010specialize finite_beta_composition_exists (s)
  11. 0011specialize finite_beta_composition_exists (pb)
  12. 0012specialize finite_beta_composition_exists (pc)
  13. 0013specialize finite_beta_composition_exists (l)
  14. 0014apply finite_beta_composition_exists
  15. 0015cases hp
  16. 0016cases hp_witness
  17. 0017have hn : exists m c. (forall fms_i_data_second fms_j_data_second fms_v_data_second. (exists fms_gap_data_second. fms_gap_data_second + S (fms_i_data_second) = (l)) -> (((exists fs_h_fms_data_second_index. fs_h_fms_data_second_index + S (fms_j_data_second) = S ((S (fms_i_data_second)) * s)) /\ exists fs_q_fms_data_second_index. r = fs_q_fms_data_second_index * S ((S (fms_i_data_second)) * s) + (fms_j_data_second))) -> (((exists fs_h_fms_data_second_source. fs_h_fms_data_second_source + S (fms_v_data_second) = S ((S (fms_j_data_second)) * nc)) /\ exists fs_q_fms_data_second_source. nb = fs_q_fms_data_second_source * S ((S (fms_j_data_second)) * nc) + (fms_v_data_second))) -> (((exists fs_h_fms_data_second_target. fs_h_fms_data_second_target + S (fms_v_data_second) = S ((S (fms_i_data_second)) * c)) /\ exists fs_q_fms_data_second_target. m = fs_q_fms_data_second_target * S ((S (fms_i_data_second)) * c) + (fms_v_data_second))))
  18. 0018specialize finite_beta_composition_exists (r)
  19. 0019specialize finite_beta_composition_exists (s)
  20. 0020specialize finite_beta_composition_exists (nb)
  21. 0021specialize finite_beta_composition_exists (nc)
  22. 0022specialize finite_beta_composition_exists (l)
  23. 0023apply finite_beta_composition_exists
  24. 0024cases hn
  25. 0025cases hn_witness
  26. 0026exists x
  27. 0027exists x1
  28. 0028exists x2
  29. 0029exists x3
  30. 0030split
  31. 0031exact hp_witness_witness
  32. 0032exact hn_witness_witness