SS0019

divisor_signed_table_reindex_data_exists

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

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

These are actual signed-table and finite-sum foundations. Equality compares represented signed values, not arbitrary encodings. MatrixMinorFourCode is reused solely as generic nested pairing, without a matrix hypothesis. Full finite signed G007 is established separately in the Möbius-inversion family.

Exact theorem in conservative defined notation

∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ r. ∀ s. ∀ l. ∃ qb. ∃ qc. ∃ mb. ∃ mc. (∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(r,s,x,y) → BetaAt(pb,pc,y,z) → BetaAt(qb,qc,x,z)) ∧ (∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(r,s,x,y) → BetaAt(nb,nc,y,z) → BetaAt(mb,mc,x,z))

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

Definition DAG

Lt(a,b) · 4BetaAt(b,c,i,x) · 12

Actual proof prerequisites

finite_beta_composition_exists · checked external prerequisite
Original expanded first-order 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))))))

Complete tactic proof in conservative notation

All 32 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

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–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: Lt(x,l)BetaAt(r,s,x,y)BetaAt(pb,pc,y,z)BetaAt(q,c,x,z)Original native command in the exact edition
  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: Lt(x,l)BetaAt(r,s,x,y)BetaAt(nb,nc,y,z)BetaAt(m,c,x,z)Original native command in the exact edition
  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 defined 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 : ∃ q. ∃ c. ∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(r,s,x,y) → BetaAt(pb,pc,y,z) → BetaAt(q,c,x,z)
  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 : ∃ m. ∃ c. ∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(r,s,x,y) → BetaAt(nb,nc,y,z) → BetaAt(m,c,x,z)
  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