JT0013

jordan_tuple_divisor_test_decidable

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

Decide each actual common-divisor-one implication constructively.

Exact expanded first-order arithmetic statement

forall n b c k d. ((exists jt_factor_leaftestyesmodulus. (n)=(d)*jt_factor_leaftestyesmodulus) -> (forall jt_index_leaftestyescoordinates jt_value_leaftestyescoordinates. (exists jt_gap_leaftestyescoordinatesindex. jt_gap_leaftestyescoordinatesindex+S (jt_index_leaftestyescoordinates)=(k)) -> (((exists fs_h_jt_leaftestyescoordinatesat. fs_h_jt_leaftestyescoordinatesat + S (jt_value_leaftestyescoordinates) = S ((S (jt_index_leaftestyescoordinates)) * c)) /\ exists fs_q_jt_leaftestyescoordinatesat. b = fs_q_jt_leaftestyescoordinatesat * S ((S (jt_index_leaftestyescoordinates)) * c) + (jt_value_leaftestyescoordinates))) -> (exists jt_factor_leaftestyescoordinatesdivides. (jt_value_leaftestyescoordinates)=(d)*jt_factor_leaftestyescoordinatesdivides)) -> (d)=1) \/ ~((exists jt_factor_leaftestnomodulus. (n)=(d)*jt_factor_leaftestnomodulus) -> (forall jt_index_leaftestnocoordinates jt_value_leaftestnocoordinates. (exists jt_gap_leaftestnocoordinatesindex. jt_gap_leaftestnocoordinatesindex+S (jt_index_leaftestnocoordinates)=(k)) -> (((exists fs_h_jt_leaftestnocoordinatesat. fs_h_jt_leaftestnocoordinatesat + S (jt_value_leaftestnocoordinates) = S ((S (jt_index_leaftestnocoordinates)) * c)) /\ exists fs_q_jt_leaftestnocoordinatesat. b = fs_q_jt_leaftestnocoordinatesat * S ((S (jt_index_leaftestnocoordinates)) * c) + (jt_value_leaftestnocoordinates))) -> (exists jt_factor_leaftestnocoordinatesdivides. (jt_value_leaftestnocoordinates)=(d)*jt_factor_leaftestnocoordinatesdivides)) -> (d)=1)

Constructive proof overview

Generated structural guide

Decide each actual common-divisor-one implication constructively.

The unchanged tactic script uses 3 declared prerequisites and contains 44 exact native proof lines.

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

Proof neighborhood

Direct dependencies

eq_decidable Alpha theorem; checked-use authorized multiple_decidable Alpha theorem; checked-use authorized JT0012 jordan_tuple_all_divisible_decidable

Direct dependents

JT0014 jordan_tuple_primitive_bounded_decidable

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

44 script commands · 19 reading checkpoints · 3 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 all divisible 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 d
02Establish heqL6–9

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

  1. L6
    have heq : d=1 \/ ~(d=1)
  2. L7
    specialize eq_decidable (d)
  3. L8
    specialize eq_decidable (1)
  4. L9
    apply eq_decidable
03Separate the logical casesL10–11

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

  1. L10
    cases heq
  2. L11
    left
04Fix variables and assumptionsL12–13

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

  1. L12
    intro hd
  2. L13
    intro hall
05Use earlier factsL14–14

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

  1. L14
    exact heq_left
06Establish hdL15–18

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

  1. L15
    have hd : (exists jt_factor_leafyes. (n)=(d)*jt_factor_leafyes) \/ ~(exists jt_factor_leafno. (n)=(d)*jt_factor_leafno)
  2. L16
    specialize multiple_decidable (d)
  3. L17
    specialize multiple_decidable (n)
  4. L18
    apply multiple_decidable
07Separate the logical casesL19–19

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

  1. L19
    cases hd
08Establish hallL20–25

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

  1. L20
    have hall : JordanTupleAllDivisible(d,b,c,k) ∨ ¬JordanTupleAllDivisible(d,b,c,k)Definitions: JordanTupleAllDivisible
  2. L21
    specialize jordan_tuple_all_divisible_decidable (d)
  3. L22
    specialize jordan_tuple_all_divisible_decidable (b)
  4. L23
    specialize jordan_tuple_all_divisible_decidable (c)
  5. L24
    specialize jordan_tuple_all_divisible_decidable (k)
  6. L25
    apply jordan_tuple_all_divisible_decidable
09Separate the logical casesL26–27

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

  1. L26
    cases hall
  2. L27
    right
10Fix variables and assumptionsL28–28

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

  1. L28
    intro h
11Use earlier factsL29–32

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

  1. L29
    apply heq_right
  2. L30
    apply h
  3. L31
    exact hd_left
  4. L32
    exact hall_left
12Separate the logical casesL33–33

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

  1. L33
    left
13Fix variables and assumptionsL34–35

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

  1. L34
    intro hdiv
  2. L35
    intro hcoords
14Separate the logical casesL36–36

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

  1. L36
    exfalso
15Use earlier factsL37–38

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

  1. L37
    apply hall_right
  2. L38
    exact hcoords
16Separate the logical casesL39–39

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

  1. L39
    left
17Fix variables and assumptionsL40–41

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

  1. L40
    intro hdiv
  2. L41
    intro hcoords
18Separate the logical casesL42–42

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

  1. L42
    exfalso
19Use earlier factsL43–44

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

  1. L43
    apply hd_right
  2. L44
    exact hdiv

Library-wide reading audit

Original exact command ledger · 44 lines
  1. 0001intro n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro k
  5. 0005intro d
  6. 0006have heq : d=1 \/ ~(d=1)
  7. 0007specialize eq_decidable (d)
  8. 0008specialize eq_decidable (1)
  9. 0009apply eq_decidable
  10. 0010cases heq
  11. 0011left
  12. 0012intro hd
  13. 0013intro hall
  14. 0014exact heq_left
  15. 0015have hd : (exists jt_factor_leafyes. (n)=(d)*jt_factor_leafyes) \/ ~(exists jt_factor_leafno. (n)=(d)*jt_factor_leafno)
  16. 0016specialize multiple_decidable (d)
  17. 0017specialize multiple_decidable (n)
  18. 0018apply multiple_decidable
  19. 0019cases hd
  20. 0020have hall : (forall jt_index_leafallyes jt_value_leafallyes. (exists jt_gap_leafallyesindex. jt_gap_leafallyesindex+S (jt_index_leafallyes)=(k)) -> (((exists fs_h_jt_leafallyesat. fs_h_jt_leafallyesat + S (jt_value_leafallyes) = S ((S (jt_index_leafallyes)) * c)) /\ exists fs_q_jt_leafallyesat. b = fs_q_jt_leafallyesat * S ((S (jt_index_leafallyes)) * c) + (jt_value_leafallyes))) -> (exists jt_factor_leafallyesdivides. (jt_value_leafallyes)=(d)*jt_factor_leafallyesdivides)) \/ ~(forall jt_index_leafallno jt_value_leafallno. (exists jt_gap_leafallnoindex. jt_gap_leafallnoindex+S (jt_index_leafallno)=(k)) -> (((exists fs_h_jt_leafallnoat. fs_h_jt_leafallnoat + S (jt_value_leafallno) = S ((S (jt_index_leafallno)) * c)) /\ exists fs_q_jt_leafallnoat. b = fs_q_jt_leafallnoat * S ((S (jt_index_leafallno)) * c) + (jt_value_leafallno))) -> (exists jt_factor_leafallnodivides. (jt_value_leafallno)=(d)*jt_factor_leafallnodivides))
  21. 0021specialize jordan_tuple_all_divisible_decidable (d)
  22. 0022specialize jordan_tuple_all_divisible_decidable (b)
  23. 0023specialize jordan_tuple_all_divisible_decidable (c)
  24. 0024specialize jordan_tuple_all_divisible_decidable (k)
  25. 0025apply jordan_tuple_all_divisible_decidable
  26. 0026cases hall
  27. 0027right
  28. 0028intro h
  29. 0029apply heq_right
  30. 0030apply h
  31. 0031exact hd_left
  32. 0032exact hall_left
  33. 0033left
  34. 0034intro hdiv
  35. 0035intro hcoords
  36. 0036exfalso
  37. 0037apply hall_right
  38. 0038exact hcoords
  39. 0039left
  40. 0040intro hdiv
  41. 0041intro hcoords
  42. 0042exfalso
  43. 0043apply hd_right
  44. 0044exact hdiv