JT0013

jordan_tuple_divisor_test_decidable

Decide each actual common-divisor-one implication constructively.

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. ∀ d. (Dvd(d,n) → JordanTupleAllDivisible(d,b,c,k) → d = 1) ∨ ¬(Dvd(d,n) → JordanTupleAllDivisible(d,b,c,k) → d = 1)

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

Definition DAG

JordanTupleAllDivisible(d,b,c,k) · 4Dvd(d,n) · 4

Actual proof prerequisites

eq_decidable · checked external prerequisitemultiple_decidable · checked external prerequisitejordan_tuple_all_divisible_decidable
Original expanded first-order 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)

Complete tactic proof in conservative notation

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

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.

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 all divisible 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 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 : Dvd(d,n) ∨ ¬Dvd(d,n)Definitions: Dvd(d,n)Original native command in the exact edition
  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(d,b,c,k)Original native command in the exact edition
  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 defined 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 : Dvd(d,n) ∨ ¬Dvd(d,n)
  16. 0016specialize multiple_decidable (d)
  17. 0017specialize multiple_decidable (n)
  18. 0018apply multiple_decidable
  19. 0019cases hd
  20. 0020have hall : JordanTupleAllDivisible(d,b,c,k) ∨ ¬JordanTupleAllDivisible(d,b,c,k)
  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