JT0015

jordan_primitive_tuple_decidable

Alpha v35 independently verified · alpha_closed; checked-use authorized; not Stable

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

Exact expanded first-order arithmetic 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)

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 45 exact native proof lines.

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

Proof neighborhood

Direct dependencies

JT0014 jordan_tuple_primitive_bounded_decidable divisor_le_nonzero Alpha theorem; checked-use authorized

Direct dependents

JT0027 jordan_tuple_scan_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

Named ingredients (1)
jordan tuple primitive bounded decidable

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–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: JordanTupleAllDivisibleLtDvd
  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
    have hb : exists g. g+d=n
  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 exact command ledger · 45 lines
  1. 0001intro n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro k
  5. 0005intro hn
  6. 0006have hd : (forall jt_divisor_primitiveyes. (exists jt_gap_primitiveyesbound. jt_gap_primitiveyesbound+S (jt_divisor_primitiveyes)=(S n)) -> ((exists jt_factor_primitiveyestestmodulus. (n)=(jt_divisor_primitiveyes)*jt_factor_primitiveyestestmodulus) -> (forall jt_index_primitiveyestestcoordinates jt_value_primitiveyestestcoordinates. (exists jt_gap_primitiveyestestcoordinatesindex. jt_gap_primitiveyestestcoordinatesindex+S (jt_index_primitiveyestestcoordinates)=(k)) -> (((exists fs_h_jt_primitiveyestestcoordinatesat. fs_h_jt_primitiveyestestcoordinatesat + S (jt_value_primitiveyestestcoordinates) = S ((S (jt_index_primitiveyestestcoordinates)) * c)) /\ exists fs_q_jt_primitiveyestestcoordinatesat. b = fs_q_jt_primitiveyestestcoordinatesat * S ((S (jt_index_primitiveyestestcoordinates)) * c) + (jt_value_primitiveyestestcoordinates))) -> (exists jt_factor_primitiveyestestcoordinatesdivides. (jt_value_primitiveyestestcoordinates)=(jt_divisor_primitiveyes)*jt_factor_primitiveyestestcoordinatesdivides)) -> (jt_divisor_primitiveyes)=1)) \/ ~(forall jt_divisor_primitiveno. (exists jt_gap_primitivenobound. jt_gap_primitivenobound+S (jt_divisor_primitiveno)=(S n)) -> ((exists jt_factor_primitivenotestmodulus. (n)=(jt_divisor_primitiveno)*jt_factor_primitivenotestmodulus) -> (forall jt_index_primitivenotestcoordinates jt_value_primitivenotestcoordinates. (exists jt_gap_primitivenotestcoordinatesindex. jt_gap_primitivenotestcoordinatesindex+S (jt_index_primitivenotestcoordinates)=(k)) -> (((exists fs_h_jt_primitivenotestcoordinatesat. fs_h_jt_primitivenotestcoordinatesat + S (jt_value_primitivenotestcoordinates) = S ((S (jt_index_primitivenotestcoordinates)) * c)) /\ exists fs_q_jt_primitivenotestcoordinatesat. b = fs_q_jt_primitivenotestcoordinatesat * S ((S (jt_index_primitivenotestcoordinates)) * c) + (jt_value_primitivenotestcoordinates))) -> (exists jt_factor_primitivenotestcoordinatesdivides. (jt_value_primitivenotestcoordinates)=(jt_divisor_primitiveno)*jt_factor_primitivenotestcoordinatesdivides)) -> (jt_divisor_primitiveno)=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 : exists g. g+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