JT0012

jordan_tuple_all_divisible_decidable

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 6 declared prerequisites and contains 55 exact native proof lines.

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

Proof neighborhood

Direct dependencies

JT0010 jordan_tuple_all_divisible_empty beta_at_exists Alpha theorem; checked-use authorized multiple_decidable Alpha theorem; checked-use authorized JT0011 jordan_tuple_all_divisible_extend le_refl Alpha theorem; checked-use authorized le_succ Alpha theorem; checked-use authorized

Direct dependents

JT0013 jordan_tuple_divisor_test_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

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.

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 : exists a. ((exists fs_h_jt_alllast. fs_h_jt_alllast + S (a) = S ((S (k)) * c)) /\ exists fs_q_jt_alllast. b = fs_q_jt_alllast * S ((S (k)) * c) + (a))
  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 : (exists jt_factor_allyes. (x)=(d)*jt_factor_allyes) \/ ~(exists jt_factor_allno. (x)=(d)*jt_factor_allno)
  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 exact 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 : exists a. ((exists fs_h_jt_alllast. fs_h_jt_alllast + S (a) = S ((S (k)) * c)) /\ exists fs_q_jt_alllast. b = fs_q_jt_alllast * S ((S (k)) * c) + (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 : (exists jt_factor_allyes. (x)=(d)*jt_factor_allyes) \/ ~(exists jt_factor_allno. (x)=(d)*jt_factor_allno)
  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