JT0011

jordan_tuple_all_divisible_extend

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

Adjoining an actually decoded divisible entry preserves common divisibility.

Exact expanded first-order arithmetic statement

forall d b c k a. (forall jt_index_allprefix jt_value_allprefix. (exists jt_gap_allprefixindex. jt_gap_allprefixindex+S (jt_index_allprefix)=(k)) -> (((exists fs_h_jt_allprefixat. fs_h_jt_allprefixat + S (jt_value_allprefix) = S ((S (jt_index_allprefix)) * c)) /\ exists fs_q_jt_allprefixat. b = fs_q_jt_allprefixat * S ((S (jt_index_allprefix)) * c) + (jt_value_allprefix))) -> (exists jt_factor_allprefixdivides. (jt_value_allprefix)=(d)*jt_factor_allprefixdivides)) -> (((exists fs_h_jt_allentry. fs_h_jt_allentry + S (a) = S ((S (k)) * c)) /\ exists fs_q_jt_allentry. b = fs_q_jt_allentry * S ((S (k)) * c) + (a))) -> (exists jt_factor_allvalue. (a)=(d)*jt_factor_allvalue) -> (forall jt_index_allsuccessor jt_value_allsuccessor. (exists jt_gap_allsuccessorindex. jt_gap_allsuccessorindex+S (jt_index_allsuccessor)=(S k)) -> (((exists fs_h_jt_allsuccessorat. fs_h_jt_allsuccessorat + S (jt_value_allsuccessor) = S ((S (jt_index_allsuccessor)) * c)) /\ exists fs_q_jt_allsuccessorat. b = fs_q_jt_allsuccessorat * S ((S (jt_index_allsuccessor)) * c) + (jt_value_allsuccessor))) -> (exists jt_factor_allsuccessordivides. (jt_value_allsuccessor)=(d)*jt_factor_allsuccessordivides))

Constructive proof overview

Generated structural guide

Adjoining an actually decoded divisible entry preserves common divisibility.

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

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

Proof neighborhood

Direct dependencies

finite_lt_succ_eq_or_lt Alpha theorem; checked-use authorized beta_at_unique Alpha theorem; checked-use authorized

Direct dependents

JT0012 jordan_tuple_all_divisible_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

36 script commands · 8 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro d
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro k
  5. L5
    intro a
  6. L6
    intro hprefix
  7. L7
    intro ha
  8. L8
    intro hda
  9. L9
    intro i
  10. L10
    intro z
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hi
  2. L12
    intro hz
03Establish hcasesL13–17

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

  1. L13
    have hcases : i=k \/ (exists jt_gap_allcases. jt_gap_allcases+S (i)=(k))
  2. L14
    specialize finite_lt_succ_eq_or_lt (k)
  3. L15
    specialize finite_lt_succ_eq_or_lt (i)
  4. L16
    apply finite_lt_succ_eq_or_lt
  5. L17
    exact hi
04Separate the logical casesL18–18

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

  1. L18
    cases hcases
05Establish heqL19–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L19
    have heq : z=a
  2. L20
    specialize beta_at_unique (b)
  3. L21
    specialize beta_at_unique (c)
  4. L22
    specialize beta_at_unique (k)
  5. L23
    specialize beta_at_unique (z)
  6. L24
    specialize beta_at_unique (a)
  7. L25
    apply beta_at_unique
  8. L26
    rewrite hcases_left at hz
  9. L27
    rewrite hcases_left at hz
  10. L28
    exact hz
06Use earlier factsL29–29

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

  1. L29
    exact ha
07Calculate and transport equalitiesL30–30

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

  1. L30
    rewrite <- heq at hda
08Use earlier factsL31–36

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

  1. L31
    exact hda
  2. L32
    specialize hprefix (i)
  3. L33
    specialize hprefix (z)
  4. L34
    apply hprefix
  5. L35
    exact hcases_right
  6. L36
    exact hz

Library-wide reading audit

Original exact command ledger · 36 lines
  1. 0001intro d
  2. 0002intro b
  3. 0003intro c
  4. 0004intro k
  5. 0005intro a
  6. 0006intro hprefix
  7. 0007intro ha
  8. 0008intro hda
  9. 0009intro i
  10. 0010intro z
  11. 0011intro hi
  12. 0012intro hz
  13. 0013have hcases : i=k \/ (exists jt_gap_allcases. jt_gap_allcases+S (i)=(k))
  14. 0014specialize finite_lt_succ_eq_or_lt (k)
  15. 0015specialize finite_lt_succ_eq_or_lt (i)
  16. 0016apply finite_lt_succ_eq_or_lt
  17. 0017exact hi
  18. 0018cases hcases
  19. 0019have heq : z=a
  20. 0020specialize beta_at_unique (b)
  21. 0021specialize beta_at_unique (c)
  22. 0022specialize beta_at_unique (k)
  23. 0023specialize beta_at_unique (z)
  24. 0024specialize beta_at_unique (a)
  25. 0025apply beta_at_unique
  26. 0026rewrite hcases_left at hz
  27. 0027rewrite hcases_left at hz
  28. 0028exact hz
  29. 0029exact ha
  30. 0030rewrite <- heq at hda
  31. 0031exact hda
  32. 0032specialize hprefix (i)
  33. 0033specialize hprefix (z)
  34. 0034apply hprefix
  35. 0035exact hcases_right
  36. 0036exact hz