JT0012

jordan_tuple_all_divisible_decidable

Finite induction decides common divisibility from genuine beta entries; no bounded-code oracle.

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. JordanTupleAllDivisible(d,b,c,k) ∨ ¬JordanTupleAllDivisible(d,b,c,k)

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

Definition DAG

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

Actual proof prerequisites

jordan_tuple_all_divisible_emptybeta_at_exists · checked external prerequisitemultiple_decidable · checked external prerequisitejordan_tuple_all_divisible_extendle_refl · checked external prerequisitele_succ · checked external prerequisite
Original expanded first-order statement 
forall d b c k. (forall jt_index_alldecyes jt_value_alldecyes. (exists jt_gap_alldecyesindex. jt_gap_alldecyesindex+S (jt_index_alldecyes)=(k)) -> (((exists fs_h_jt_alldecyesat. fs_h_jt_alldecyesat + S (jt_value_alldecyes) = S ((S (jt_index_alldecyes)) * c)) /\ exists fs_q_jt_alldecyesat. b = fs_q_jt_alldecyesat * S ((S (jt_index_alldecyes)) * c) + (jt_value_alldecyes))) -> (exists jt_factor_alldecyesdivides. (jt_value_alldecyes)=(d)*jt_factor_alldecyesdivides)) \/ ~(forall jt_index_alldecno jt_value_alldecno. (exists jt_gap_alldecnoindex. jt_gap_alldecnoindex+S (jt_index_alldecno)=(k)) -> (((exists fs_h_jt_alldecnoat. fs_h_jt_alldecnoat + S (jt_value_alldecno) = S ((S (jt_index_alldecno)) * c)) /\ exists fs_q_jt_alldecnoat. b = fs_q_jt_alldecnoat * S ((S (jt_index_alldecno)) * c) + (jt_value_alldecno))) -> (exists jt_factor_alldecnodivides. (jt_value_alldecno)=(d)*jt_factor_alldecnodivides))

Complete tactic proof in conservative notation

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

55 script commands · 17 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.

Named ingredients (2)
jordan tuple all divisible emptyjordan tuple all divisible extend
01Fix variables and assumptionsL1–3

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

  1. L1
    intro d
  2. L2
    intro b
  3. L3
    intro c
02Induction on kL4–4

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

  1. L4
    induction k
03Separate the logical casesL5–5

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

  1. L5
    left
04Use earlier factsL6–9

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

  1. L6
    specialize jordan_tuple_all_divisible_empty (d)
  2. L7
    specialize jordan_tuple_all_divisible_empty (b)
  3. L8
    specialize jordan_tuple_all_divisible_empty (c)
  4. L9
    apply jordan_tuple_all_divisible_empty
05Establish haL10–14

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

  1. L10
    have ha : ∃ a. BetaAt(b,c,k,a)Definitions: BetaAt(b,c,k,a)Original native command in the exact edition
  2. L11
    specialize beta_at_exists (b)
  3. L12
    specialize beta_at_exists (c)
  4. L13
    specialize beta_at_exists (k)
  5. L14
    apply beta_at_exists
06Separate the logical casesL15–15

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

  1. L15
    cases ha
07Establish hdL16–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply multiple decidable.

  1. L16
    have hd : Dvd(d,x) ∨ ¬Dvd(d,x)Definitions: Dvd(d,x)Original native command in the exact edition
  2. L17
    specialize multiple_decidable (d)
  3. L18
    specialize multiple_decidable (x)
  4. L19
    apply multiple_decidable
08Separate the logical casesL20–22

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

  1. L20
    cases IH
  2. L21
    cases hd
  3. L22
    left
09Use earlier factsL23–31

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

  1. L23
    specialize jordan_tuple_all_divisible_extend (d)
  2. L24
    specialize jordan_tuple_all_divisible_extend (b)
  3. L25
    specialize jordan_tuple_all_divisible_extend (c)
  4. L26
    specialize jordan_tuple_all_divisible_extend (k)
  5. L27
    specialize jordan_tuple_all_divisible_extend (x)
  6. L28
    apply jordan_tuple_all_divisible_extend
  7. L29
    exact IH_left
  8. L30
    exact ha_witness
  9. L31
    exact hd_left
10Separate the logical casesL32–32

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

  1. L32
    right
11Fix variables and assumptionsL33–33

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

  1. L33
    intro h
12Use earlier factsL34–40

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

  1. L34
    apply hd_right
  2. L35
    specialize h (k)
  3. L36
    specialize h (x)
  4. L37
    apply h
  5. L38
    specialize le_refl (S k)
  6. L39
    apply le_refl
  7. L40
    exact ha_witness
13Separate the logical casesL41–41

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

  1. L41
    right
14Fix variables and assumptionsL42–42

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

  1. L42
    intro h
15Use earlier factsL43–43

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

  1. L43
    apply IH_right
16Fix variables and assumptionsL44–47

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

  1. L44
    intro i
  2. L45
    intro a
  3. L46
    intro hi
  4. L47
    intro hat
17Use earlier factsL48–55

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

  1. L48
    specialize h (i)
  2. L49
    specialize h (a)
  3. L50
    apply h
  4. L51
    specialize le_succ (S i)
  5. L52
    specialize le_succ (k)
  6. L53
    apply le_succ
  7. L54
    exact hi
  8. L55
    exact hat

Library-wide reading audit

Original defined command ledger · 55 lines
  1. 0001intro d
  2. 0002intro b
  3. 0003intro c
  4. 0004induction k
  5. 0005left
  6. 0006specialize jordan_tuple_all_divisible_empty (d)
  7. 0007specialize jordan_tuple_all_divisible_empty (b)
  8. 0008specialize jordan_tuple_all_divisible_empty (c)
  9. 0009apply jordan_tuple_all_divisible_empty
  10. 0010have ha : ∃ a. BetaAt(b,c,k,a)
  11. 0011specialize beta_at_exists (b)
  12. 0012specialize beta_at_exists (c)
  13. 0013specialize beta_at_exists (k)
  14. 0014apply beta_at_exists
  15. 0015cases ha
  16. 0016have hd : Dvd(d,x) ∨ ¬Dvd(d,x)
  17. 0017specialize multiple_decidable (d)
  18. 0018specialize multiple_decidable (x)
  19. 0019apply multiple_decidable
  20. 0020cases IH
  21. 0021cases hd
  22. 0022left
  23. 0023specialize jordan_tuple_all_divisible_extend (d)
  24. 0024specialize jordan_tuple_all_divisible_extend (b)
  25. 0025specialize jordan_tuple_all_divisible_extend (c)
  26. 0026specialize jordan_tuple_all_divisible_extend (k)
  27. 0027specialize jordan_tuple_all_divisible_extend (x)
  28. 0028apply jordan_tuple_all_divisible_extend
  29. 0029exact IH_left
  30. 0030exact ha_witness
  31. 0031exact hd_left
  32. 0032right
  33. 0033intro h
  34. 0034apply hd_right
  35. 0035specialize h (k)
  36. 0036specialize h (x)
  37. 0037apply h
  38. 0038specialize le_refl (S k)
  39. 0039apply le_refl
  40. 0040exact ha_witness
  41. 0041right
  42. 0042intro h
  43. 0043apply IH_right
  44. 0044intro i
  45. 0045intro a
  46. 0046intro hi
  47. 0047intro hat
  48. 0048specialize h (i)
  49. 0049specialize h (a)
  50. 0050apply h
  51. 0051specialize le_succ (S i)
  52. 0052specialize le_succ (k)
  53. 0053apply le_succ
  54. 0054exact hi
  55. 0055exact hat