CD0034

finite_modular_orbit_member_or_boundary

Finite orbit induction either proves membership at the reached residue or constructs an actual first-exit edge.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Sets are complete characteristic-bit codes with actual finite cardinality witnesses. The proof constructs translations and the sumset; no finite-choice oracle, supplied cardinality conclusion, or unproved polynomial-method premise is used.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ p. ∀ d. ∀ a. ∀ n. ∀ r. ¬p = 0 → AllBits(b,c,p) → ModularSetMember(b,c,p,a) → Lt(r,p) → ModEq(p,a + n · d,r) → BetaAt(b,c,r,1) ∨ (∃ x. ∃ y. ModularTranslationBoundary(b,c,p,d,x,y))

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

Definition DAG

ModularSetMember(b,c,p,x) · 1ModularTranslationBoundary(b,c,p,d,a,r) · 2Lt(a,b) · 2ModEq(m,a,b) · 3BetaAt(b,c,i,x) · 4AllBits(b,c,l) · 1

Actual proof prerequisites

mul_zero_left · checked external prerequisitemod_eq_bounded_unique · checked external prerequisitefinite_modular_residue_existsfinite_bit_membership_decidablemod_eq_add · checked external prerequisitemod_eq_refl · checked external prerequisitemod_eq_symm · checked external prerequisitemod_eq_trans · checked external prerequisitemul_succ_left · checked external prerequisiteadd_assoc · checked external prerequisite
Original expanded first-order statement 
forall b c p d a n r. ~(p=0) -> (forall ff_i_fms_bits. (exists ff_lt_fms_bits_bound. ff_lt_fms_bits_bound + S ff_i_fms_bits = (p)) -> exists ff_bit_fms_bits. ((((exists ff_h_fms_bits_decoded. ff_h_fms_bits_decoded + S (ff_bit_fms_bits) = S ((S (ff_i_fms_bits)) * (c))) /\ exists ff_q_fms_bits_decoded. (b) = ff_q_fms_bits_decoded * S ((S (ff_i_fms_bits)) * (c)) + (ff_bit_fms_bits))) /\ (ff_bit_fms_bits = 0 \/ ff_bit_fms_bits = 1))) -> (((exists fms_gap_member. fms_gap_member + S (a) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (a)) * c)) /\ exists fs_q_fms_member. b = fs_q_fms_member * S ((S (a)) * c) + (1))))) -> (exists fms_gap_lt. fms_gap_lt + S (r) = (p)) -> (exists fms_u_mod fms_v_mod. (a+n*d) + (p) * fms_u_mod = (r) + (p) * fms_v_mod) -> (((exists fs_h_cd_orbit_inside. fs_h_cd_orbit_inside + S (1) = S ((S (r)) * c)) /\ exists fs_q_cd_orbit_inside. b = fs_q_cd_orbit_inside * S ((S (r)) * c) + (1))) \/ (exists cd_source_boundary cd_target_boundary. ((((exists fms_gap_cd_boundary_source. fms_gap_cd_boundary_source + S (cd_source_boundary) = (p)) /\ (((exists fs_h_fms_cd_boundary_source. fs_h_fms_cd_boundary_source + S (1) = S ((S (cd_source_boundary)) * c)) /\ exists fs_q_fms_cd_boundary_source. b = fs_q_fms_cd_boundary_source * S ((S (cd_source_boundary)) * c) + (1))))) /\ ((exists fms_gap_cd_boundary_target. fms_gap_cd_boundary_target + S (cd_target_boundary) = (p)) /\ ((exists fms_u_cd_boundary_shift fms_v_cd_boundary_shift. (cd_source_boundary+d) + (p) * fms_u_cd_boundary_shift = (cd_target_boundary) + (p) * fms_v_cd_boundary_shift) /\ ~(((exists fs_h_cd_boundary_outside. fs_h_cd_boundary_outside + S (1) = S ((S (cd_target_boundary)) * c)) /\ exists fs_q_cd_boundary_outside. b = fs_q_cd_boundary_outside * S ((S (cd_target_boundary)) * c) + (1)))))))

Complete tactic proof in conservative notation

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

108 script commands · 32 reading checkpoints · 8 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 (2)
finite modular residue existsfinite bit membership decidable
01Fix variables and assumptionsL1–5

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro p
  4. L4
    intro d
  5. L5
    intro a
02Induction on nL6–12

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L6
    induction n
  2. L7
    intro r
  3. L8
    intro hp
  4. L9
    intro hbits
  5. L10
    intro hstart
  6. L11
    intro hr
  7. L12
    intro hmod
03Separate the logical casesL13–13

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

  1. L13
    cases hstart
04Establish hzeroL14–16

Establish this local claim before using it. It is not an additional assumption.

  1. L14
    have hzero : a+0*d=a
  2. L15
    simp [mul_zero_left]
  3. L16
    rewrite hzero at hmod
05Establish heL17–24

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

  1. L17
    have he : a=r
  2. L18
    specialize mod_eq_bounded_unique p
  3. L19
    specialize mod_eq_bounded_unique a
  4. L20
    specialize mod_eq_bounded_unique r
  5. L21
    apply mod_eq_bounded_unique
  6. L22
    exact hstart_left
  7. L23
    exact hr
  8. L24
    exact hmod
06Separate the logical casesL25–25

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

  1. L25
    left
07Calculate and transport equalitiesL26–27

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

  1. L26
    rewrite he at hstart_right
  2. L27
    rewrite he at hstart_right
08Use earlier factsL28–28

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

  1. L28
    exact hstart_right
09Fix variables and assumptionsL29–34

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

  1. L29
    intro r
  2. L30
    intro hp
  3. L31
    intro hbits
  4. L32
    intro hstart
  5. L33
    intro hr
  6. L34
    intro hmod
10Establish hprevL35–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite modular residue exists.

  1. L35
    have hprev : ∃ v. Lt(v,p) ∧ ModEq(p,a + n · d,v)Definitions: Lt(v,p)ModEq(p,a + n · d,v)Original native command in the exact edition
  2. L36
    specialize finite_modular_residue_exists p
  3. L37
    specialize finite_modular_residue_exists a+n*d
  4. L38
    apply finite_modular_residue_exists
  5. L39
    exact hp
11Separate the logical casesL40–41

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

  1. L40
    cases hprev
  2. L41
    cases hprev_witness
12Establish hcaseL42–49

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

  1. L42
    have hcase : BetaAt(b,c,x,1) ∨ (∃ y. ∃ z. ModularTranslationBoundary(b,c,p,d,y,z))Definitions: BetaAt(b,c,x,1)ModularTranslationBoundary(b,c,p,d,y,z)Original native command in the exact edition
  2. L43
    specialize IH x
  3. L44
    apply IH
  4. L45
    exact hp
  5. L46
    exact hbits
  6. L47
    exact hstart
  7. L48
    exact hprev_witness_left
  8. L49
    exact hprev_witness_right
13Separate the logical casesL50–50

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

  1. L50
    cases hcase
14Establish hdecL51–58

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

  1. L51
    have hdec : BetaAt(b,c,r,1) ∨ ¬BetaAt(b,c,r,1)Definitions: BetaAt(b,c,r,1)Original native command in the exact edition
  2. L52
    specialize finite_bit_membership_decidable b
  3. L53
    specialize finite_bit_membership_decidable c
  4. L54
    specialize finite_bit_membership_decidable p
  5. L55
    specialize finite_bit_membership_decidable r
  6. L56
    apply finite_bit_membership_decidable
  7. L57
    exact hbits
  8. L58
    exact hr
15Separate the logical casesL59–60

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

  1. L59
    cases hdec
  2. L60
    left
16Use earlier factsL61–61

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

  1. L61
    exact hdec_left
17Separate the logical casesL62–62

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

  1. L62
    right
18Construct an explicit witnessL63–64

Supply the displayed value, then prove that it has the required property.

  1. L63
    exists x
  2. L64
    exists r
19Separate the logical casesL65–66

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

  1. L65
    split
  2. L66
    split
20Use earlier factsL67–68

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

  1. L67
    exact hprev_witness_left
  2. L68
    exact hcase_left
21Separate the logical casesL69–69

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

  1. L69
    split
22Use earlier factsL70–70

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

  1. L70
    exact hr
23Separate the logical casesL71–71

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

  1. L71
    split
24Establish haddL72–81

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

  1. L72
    have hadd : ModEq(p,a + n · d + d,x + d)Definitions: ModEq(p,a + n · d + d,x + d)Original native command in the exact edition
  2. L73
    specialize mod_eq_add p
  3. L74
    specialize mod_eq_add a+n*d
  4. L75
    specialize mod_eq_add x
  5. L76
    specialize mod_eq_add d
  6. L77
    specialize mod_eq_add d
  7. L78
    apply mod_eq_add
  8. L79
    exact hprev_witness_right
  9. L80
    specialize mod_eq_refl p
  10. L81
    specialize mod_eq_refl d
25Use earlier factsL82–91

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

  1. L82
    apply mod_eq_refl
  2. L83
    specialize mod_eq_trans p
  3. L84
    specialize mod_eq_trans x+d
  4. L85
    specialize mod_eq_trans (a+n*d)+d
  5. L86
    specialize mod_eq_trans r
  6. L87
    apply mod_eq_trans
  7. L88
    specialize mod_eq_symm p
  8. L89
    specialize mod_eq_symm (a+n*d)+d
  9. L90
    specialize mod_eq_symm x+d
  10. L91
    apply mod_eq_symm
26Use earlier factsL92–92

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

  1. L92
    exact hadd
27Establish heL93–93

Establish this local claim before using it. It is not an additional assumption.

  1. L93
    have he : a+(S n)*d=(a+n*d)+d
28Establish hsL94–103

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul succ left.

  1. L94
    have hs : (S n)*d=n*d+d
  2. L95
    specialize mul_succ_left n
  3. L96
    specialize mul_succ_left d
  4. L97
    apply mul_succ_left
  5. L98
    rewrite hs
  6. L99
    symm
  7. L100
    specialize add_assoc a
  8. L101
    specialize add_assoc n*d
  9. L102
    specialize add_assoc d
  10. L103
    apply add_assoc
29Calculate and transport equalitiesL104–104

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

  1. L104
    rewrite <- he
30Use earlier factsL105–106

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

  1. L105
    exact hmod
  2. L106
    exact hdec_right
31Separate the logical casesL107–107

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

  1. L107
    right
32Use earlier factsL108–108

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

  1. L108
    exact hcase_right

Library-wide reading audit

Original defined command ledger · 108 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro p
  4. 0004intro d
  5. 0005intro a
  6. 0006induction n
  7. 0007intro r
  8. 0008intro hp
  9. 0009intro hbits
  10. 0010intro hstart
  11. 0011intro hr
  12. 0012intro hmod
  13. 0013cases hstart
  14. 0014have hzero : a+0*d=a
  15. 0015simp [mul_zero_left]
  16. 0016rewrite hzero at hmod
  17. 0017have he : a=r
  18. 0018specialize mod_eq_bounded_unique p
  19. 0019specialize mod_eq_bounded_unique a
  20. 0020specialize mod_eq_bounded_unique r
  21. 0021apply mod_eq_bounded_unique
  22. 0022exact hstart_left
  23. 0023exact hr
  24. 0024exact hmod
  25. 0025left
  26. 0026rewrite he at hstart_right
  27. 0027rewrite he at hstart_right
  28. 0028exact hstart_right
  29. 0029intro r
  30. 0030intro hp
  31. 0031intro hbits
  32. 0032intro hstart
  33. 0033intro hr
  34. 0034intro hmod
  35. 0035have hprev : ∃ v. Lt(v,p) ∧ ModEq(p,a + n · d,v)
  36. 0036specialize finite_modular_residue_exists p
  37. 0037specialize finite_modular_residue_exists a+n*d
  38. 0038apply finite_modular_residue_exists
  39. 0039exact hp
  40. 0040cases hprev
  41. 0041cases hprev_witness
  42. 0042have hcase : BetaAt(b,c,x,1) ∨ (∃ y. ∃ z. ModularTranslationBoundary(b,c,p,d,y,z))
  43. 0043specialize IH x
  44. 0044apply IH
  45. 0045exact hp
  46. 0046exact hbits
  47. 0047exact hstart
  48. 0048exact hprev_witness_left
  49. 0049exact hprev_witness_right
  50. 0050cases hcase
  51. 0051have hdec : BetaAt(b,c,r,1) ∨ ¬BetaAt(b,c,r,1)
  52. 0052specialize finite_bit_membership_decidable b
  53. 0053specialize finite_bit_membership_decidable c
  54. 0054specialize finite_bit_membership_decidable p
  55. 0055specialize finite_bit_membership_decidable r
  56. 0056apply finite_bit_membership_decidable
  57. 0057exact hbits
  58. 0058exact hr
  59. 0059cases hdec
  60. 0060left
  61. 0061exact hdec_left
  62. 0062right
  63. 0063exists x
  64. 0064exists r
  65. 0065split
  66. 0066split
  67. 0067exact hprev_witness_left
  68. 0068exact hcase_left
  69. 0069split
  70. 0070exact hr
  71. 0071split
  72. 0072have hadd : ModEq(p,a + n · d + d,x + d)
  73. 0073specialize mod_eq_add p
  74. 0074specialize mod_eq_add a+n*d
  75. 0075specialize mod_eq_add x
  76. 0076specialize mod_eq_add d
  77. 0077specialize mod_eq_add d
  78. 0078apply mod_eq_add
  79. 0079exact hprev_witness_right
  80. 0080specialize mod_eq_refl p
  81. 0081specialize mod_eq_refl d
  82. 0082apply mod_eq_refl
  83. 0083specialize mod_eq_trans p
  84. 0084specialize mod_eq_trans x+d
  85. 0085specialize mod_eq_trans (a+n*d)+d
  86. 0086specialize mod_eq_trans r
  87. 0087apply mod_eq_trans
  88. 0088specialize mod_eq_symm p
  89. 0089specialize mod_eq_symm (a+n*d)+d
  90. 0090specialize mod_eq_symm x+d
  91. 0091apply mod_eq_symm
  92. 0092exact hadd
  93. 0093have he : a+(S n)*d=(a+n*d)+d
  94. 0094have hs : (S n)*d=n*d+d
  95. 0095specialize mul_succ_left n
  96. 0096specialize mul_succ_left d
  97. 0097apply mul_succ_left
  98. 0098rewrite hs
  99. 0099symm
  100. 0100specialize add_assoc a
  101. 0101specialize add_assoc n*d
  102. 0102specialize add_assoc d
  103. 0103apply add_assoc
  104. 0104rewrite <- he
  105. 0105exact hmod
  106. 0106exact hdec_right
  107. 0107right
  108. 0108exact hcase_right