JT0011

jordan_tuple_all_divisible_extend

Adjoining an actually decoded divisible entry preserves common divisibility.

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

95 new Alpha admissions come from 96 source lemmas: tuple equality reflexivity reuses an already-admitted theorem and is not counted twice. All counts use actual finite beta-coded enumerations. G008 multiplicativity is proved; the general prime-power count and distinct-prime product formula are further goals. General prime-power fields (G091) remain open. Stable is unchanged.

Exact theorem in conservative defined notation

∀ d. ∀ b. ∀ c. ∀ k. ∀ a. JordanTupleAllDivisible(d,b,c,k) → BetaAt(b,c,k,a) → Dvd(d,a) → JordanTupleAllDivisible(d,b,c,S k)

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

Definition DAG

JordanTupleAllDivisible(d,b,c,k) · 2Lt(a,b) · 1Dvd(d,n) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

finite_lt_succ_eq_or_lt · checked external prerequisitebeta_at_unique · checked external prerequisite
Original expanded first-order statement 
forall d b c k a. (forall jt_index_allprefix jt_value_allprefix. (exists jt_gap_allprefixindex. jt_gap_allprefixindex+S (jt_index_allprefix)=(k)) -> (((exists fs_h_jt_allprefixat. fs_h_jt_allprefixat + S (jt_value_allprefix) = S ((S (jt_index_allprefix)) * c)) /\ exists fs_q_jt_allprefixat. b = fs_q_jt_allprefixat * S ((S (jt_index_allprefix)) * c) + (jt_value_allprefix))) -> (exists jt_factor_allprefixdivides. (jt_value_allprefix)=(d)*jt_factor_allprefixdivides)) -> (((exists fs_h_jt_allentry. fs_h_jt_allentry + S (a) = S ((S (k)) * c)) /\ exists fs_q_jt_allentry. b = fs_q_jt_allentry * S ((S (k)) * c) + (a))) -> (exists jt_factor_allvalue. (a)=(d)*jt_factor_allvalue) -> (forall jt_index_allsuccessor jt_value_allsuccessor. (exists jt_gap_allsuccessorindex. jt_gap_allsuccessorindex+S (jt_index_allsuccessor)=(S k)) -> (((exists fs_h_jt_allsuccessorat. fs_h_jt_allsuccessorat + S (jt_value_allsuccessor) = S ((S (jt_index_allsuccessor)) * c)) /\ exists fs_q_jt_allsuccessorat. b = fs_q_jt_allsuccessorat * S ((S (jt_index_allsuccessor)) * c) + (jt_value_allsuccessor))) -> (exists jt_factor_allsuccessordivides. (jt_value_allsuccessor)=(d)*jt_factor_allsuccessordivides))

Complete tactic proof in conservative notation

All 36 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

36 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–10

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

  1. L1
    intro d
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro k
  5. L5
    intro a
  6. L6
    intro hprefix
  7. L7
    intro ha
  8. L8
    intro hda
  9. L9
    intro i
  10. L10
    intro z
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hi
  2. L12
    intro hz
03Establish hcasesL13–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L13
    have hcases : i = k ∨ Lt(i,k)Definitions: Lt(i,k)Original native command in the exact edition
  2. L14
    specialize finite_lt_succ_eq_or_lt (k)
  3. L15
    specialize finite_lt_succ_eq_or_lt (i)
  4. L16
    apply finite_lt_succ_eq_or_lt
  5. L17
    exact hi
04Separate the logical casesL18–18

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

  1. L18
    cases hcases
05Establish heqL19–28

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

  1. L19
    have heq : z=a
  2. L20
    specialize beta_at_unique (b)
  3. L21
    specialize beta_at_unique (c)
  4. L22
    specialize beta_at_unique (k)
  5. L23
    specialize beta_at_unique (z)
  6. L24
    specialize beta_at_unique (a)
  7. L25
    apply beta_at_unique
  8. L26
    rewrite hcases_left at hz
  9. L27
    rewrite hcases_left at hz
  10. L28
    exact hz
06Use earlier factsL29–29

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

  1. L29
    exact ha
07Calculate and transport equalitiesL30–30

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L30
    rewrite <- heq at hda
08Use earlier factsL31–36

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

  1. L31
    exact hda
  2. L32
    specialize hprefix (i)
  3. L33
    specialize hprefix (z)
  4. L34
    apply hprefix
  5. L35
    exact hcases_right
  6. L36
    exact hz

Library-wide reading audit

Original defined command ledger · 36 lines
  1. 0001intro d
  2. 0002intro b
  3. 0003intro c
  4. 0004intro k
  5. 0005intro a
  6. 0006intro hprefix
  7. 0007intro ha
  8. 0008intro hda
  9. 0009intro i
  10. 0010intro z
  11. 0011intro hi
  12. 0012intro hz
  13. 0013have hcases : i = k ∨ Lt(i,k)
  14. 0014specialize finite_lt_succ_eq_or_lt (k)
  15. 0015specialize finite_lt_succ_eq_or_lt (i)
  16. 0016apply finite_lt_succ_eq_or_lt
  17. 0017exact hi
  18. 0018cases hcases
  19. 0019have heq : z=a
  20. 0020specialize beta_at_unique (b)
  21. 0021specialize beta_at_unique (c)
  22. 0022specialize beta_at_unique (k)
  23. 0023specialize beta_at_unique (z)
  24. 0024specialize beta_at_unique (a)
  25. 0025apply beta_at_unique
  26. 0026rewrite hcases_left at hz
  27. 0027rewrite hcases_left at hz
  28. 0028exact hz
  29. 0029exact ha
  30. 0030rewrite <- heq at hda
  31. 0031exact hda
  32. 0032specialize hprefix (i)
  33. 0033specialize hprefix (z)
  34. 0034apply hprefix
  35. 0035exact hcases_right
  36. 0036exact hz