JT0015

jordan_primitive_tuple_decidable

At positive modulus every possible common divisor lies below S n, giving genuine tuple-predicate decidability.

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

∀ n. ∀ b. ∀ c. ∀ k. ¬n = 0 → JordanPrimitiveTuple(n,b,c,k) ∨ ¬JordanPrimitiveTuple(n,b,c,k)

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

Definition DAG

JordanTupleAllDivisible(d,b,c,k) · 2JordanPrimitiveTuple(n,b,c,k) · 2Le(a,b) · 1Lt(a,b) · 2Dvd(d,n) · 2

Actual proof prerequisites

jordan_tuple_primitive_bounded_decidabledivisor_le_nonzero · checked external prerequisite
Original expanded first-order statement 
forall n b c k. ~(n=0) -> (forall jt_divisor_decprimitiveyes. (exists jt_factor_decprimitiveyesmodulus. (n)=(jt_divisor_decprimitiveyes)*jt_factor_decprimitiveyesmodulus) -> (forall jt_index_decprimitiveyescoordinates jt_value_decprimitiveyescoordinates. (exists jt_gap_decprimitiveyescoordinatesindex. jt_gap_decprimitiveyescoordinatesindex+S (jt_index_decprimitiveyescoordinates)=(k)) -> (((exists fs_h_jt_decprimitiveyescoordinatesat. fs_h_jt_decprimitiveyescoordinatesat + S (jt_value_decprimitiveyescoordinates) = S ((S (jt_index_decprimitiveyescoordinates)) * c)) /\ exists fs_q_jt_decprimitiveyescoordinatesat. b = fs_q_jt_decprimitiveyescoordinatesat * S ((S (jt_index_decprimitiveyescoordinates)) * c) + (jt_value_decprimitiveyescoordinates))) -> (exists jt_factor_decprimitiveyescoordinatesdivides. (jt_value_decprimitiveyescoordinates)=(jt_divisor_decprimitiveyes)*jt_factor_decprimitiveyescoordinatesdivides)) -> jt_divisor_decprimitiveyes=1) \/ ~(forall jt_divisor_decprimitiveno. (exists jt_factor_decprimitivenomodulus. (n)=(jt_divisor_decprimitiveno)*jt_factor_decprimitivenomodulus) -> (forall jt_index_decprimitivenocoordinates jt_value_decprimitivenocoordinates. (exists jt_gap_decprimitivenocoordinatesindex. jt_gap_decprimitivenocoordinatesindex+S (jt_index_decprimitivenocoordinates)=(k)) -> (((exists fs_h_jt_decprimitivenocoordinatesat. fs_h_jt_decprimitivenocoordinatesat + S (jt_value_decprimitivenocoordinates) = S ((S (jt_index_decprimitivenocoordinates)) * c)) /\ exists fs_q_jt_decprimitivenocoordinatesat. b = fs_q_jt_decprimitivenocoordinatesat * S ((S (jt_index_decprimitivenocoordinates)) * c) + (jt_value_decprimitivenocoordinates))) -> (exists jt_factor_decprimitivenocoordinatesdivides. (jt_value_decprimitivenocoordinates)=(jt_divisor_decprimitiveno)*jt_factor_decprimitivenocoordinatesdivides)) -> jt_divisor_decprimitiveno=1)

Complete tactic proof in conservative notation

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

45 script commands · 15 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 (1)
jordan tuple primitive bounded decidable
01Fix variables and assumptionsL1–5

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

  1. L1
    intro n
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro k
  5. L5
    intro hn
02Establish hdL6–12

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

  1. L6
    have hd : (∀ x. Lt(x,S n) → Dvd(x,n) → JordanTupleAllDivisible(x,b,c,k) → x = 1) ∨ ¬(∀ x. Lt(x,S n) → Dvd(x,n) → JordanTupleAllDivisible(x,b,c,k) → x = 1)Definitions: Lt(x,S n)Dvd(x,n)JordanTupleAllDivisible(x,b,c,k)Original native command in the exact edition
  2. L7
    specialize jordan_tuple_primitive_bounded_decidable (n)
  3. L8
    specialize jordan_tuple_primitive_bounded_decidable (b)
  4. L9
    specialize jordan_tuple_primitive_bounded_decidable (c)
  5. L10
    specialize jordan_tuple_primitive_bounded_decidable (k)
  6. L11
    specialize jordan_tuple_primitive_bounded_decidable (S n)
  7. L12
    apply jordan_tuple_primitive_bounded_decidable
03Separate the logical casesL13–14

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

  1. L13
    cases hd
  2. L14
    left
04Fix variables and assumptionsL15–17

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

  1. L15
    intro d
  2. L16
    intro hdiv
  3. L17
    intro hall
05Use earlier factsL18–19

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

  1. L18
    specialize hd_left (d)
  2. L19
    apply hd_left
06Establish hbL20–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor le nonzero.

  1. L20
  2. L21
    specialize divisor_le_nonzero (d)
  3. L22
    specialize divisor_le_nonzero (n)
  4. L23
    apply divisor_le_nonzero
  5. L24
    exact hn
  6. L25
    exact hdiv
07Separate the logical casesL26–26

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

  1. L26
    cases hb
08Construct an explicit witnessL27–27

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

  1. L27
    exists x
09Calculate and transport equalitiesL28–31

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

  1. L28
    trans S (x+d)
  2. L29
    rewrite PA4
  3. L30
    refl
  4. L31
    congr
10Use earlier factsL32–34

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

  1. L32
    exact hb_witness
  2. L33
    exact hdiv
  3. L34
    exact hall
11Separate the logical casesL35–35

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

  1. L35
    right
12Fix variables and assumptionsL36–36

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

  1. L36
    intro hp
13Use earlier factsL37–37

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

  1. L37
    apply hd_right
14Fix variables and assumptionsL38–41

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

  1. L38
    intro d
  2. L39
    intro hbound
  3. L40
    intro hdiv
  4. L41
    intro hall
15Use earlier factsL42–45

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

  1. L42
    specialize hp (d)
  2. L43
    apply hp
  3. L44
    exact hdiv
  4. L45
    exact hall

Library-wide reading audit

Original defined command ledger · 45 lines
  1. 0001intro n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro k
  5. 0005intro hn
  6. 0006have hd : (∀ x. Lt(x,S n) → Dvd(x,n) → JordanTupleAllDivisible(x,b,c,k) → x = 1) ∨ ¬(∀ x. Lt(x,S n) → Dvd(x,n) → JordanTupleAllDivisible(x,b,c,k) → x = 1)
  7. 0007specialize jordan_tuple_primitive_bounded_decidable (n)
  8. 0008specialize jordan_tuple_primitive_bounded_decidable (b)
  9. 0009specialize jordan_tuple_primitive_bounded_decidable (c)
  10. 0010specialize jordan_tuple_primitive_bounded_decidable (k)
  11. 0011specialize jordan_tuple_primitive_bounded_decidable (S n)
  12. 0012apply jordan_tuple_primitive_bounded_decidable
  13. 0013cases hd
  14. 0014left
  15. 0015intro d
  16. 0016intro hdiv
  17. 0017intro hall
  18. 0018specialize hd_left (d)
  19. 0019apply hd_left
  20. 0020have hb : Le(d,n)
  21. 0021specialize divisor_le_nonzero (d)
  22. 0022specialize divisor_le_nonzero (n)
  23. 0023apply divisor_le_nonzero
  24. 0024exact hn
  25. 0025exact hdiv
  26. 0026cases hb
  27. 0027exists x
  28. 0028trans S (x+d)
  29. 0029rewrite PA4
  30. 0030refl
  31. 0031congr
  32. 0032exact hb_witness
  33. 0033exact hdiv
  34. 0034exact hall
  35. 0035right
  36. 0036intro hp
  37. 0037apply hd_right
  38. 0038intro d
  39. 0039intro hbound
  40. 0040intro hdiv
  41. 0041intro hall
  42. 0042specialize hp (d)
  43. 0043apply hp
  44. 0044exact hdiv
  45. 0045exact hall