FS004F · theorem body

four_square_bounded_complement_prefix_exists

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

Every bounded finite beta prefix admits a constructive beta-coded pointwise residue complement p-1-r.

historical independently replay-verified empty-context experiment; the experiment itself persisted no certificate and granted no release authority; current checked use follows separately sealed proof bundles; no Stable promotion.

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.

Statement with defined notation

∀ p. ∀ b. ∀ c. ∀ l. (∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,p)) → ∃ x. ∃ y. ∀ z. ∀ n. ∀ m. Lt(z,l) → BetaAt(b,c,z,n) → BetaAt(x,y,z,m) → m + S n = p

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt

In local proof propositions

PD0002 Lt PD0013 BetaAt
Exact expanded first-order statement
forall p b c l. (forall fom_index_fsri_complement_source. (exists fom_gap_fsri_complement_source_index_bound. fom_gap_fsri_complement_source_index_bound + S (fom_index_fsri_complement_source) = l) -> exists fom_value_fsri_complement_source. ((((exists fom_beta_height_fsri_complement_source_entry. fom_beta_height_fsri_complement_source_entry + S (fom_value_fsri_complement_source) = S ((S (fom_index_fsri_complement_source)) * c)) /\ exists fom_beta_quotient_fsri_complement_source_entry. b = fom_beta_quotient_fsri_complement_source_entry * S ((S (fom_index_fsri_complement_source)) * c) + (fom_value_fsri_complement_source))) /\ (exists fom_gap_fsri_complement_source_value_bound. fom_gap_fsri_complement_source_value_bound + S (fom_value_fsri_complement_source) = p))) -> exists z d. (forall fsri_complement_index_exists fsri_complement_source_exists fsri_complement_target_exists. (exists fsri_gap_exists_index. fsri_gap_exists_index + S (fsri_complement_index_exists) = (l)) -> (((exists fsri_height_exists_source. fsri_height_exists_source + S (fsri_complement_source_exists) = S ((S (fsri_complement_index_exists)) * (c))) /\ exists fsri_quotient_exists_source. (b) = fsri_quotient_exists_source * S ((S (fsri_complement_index_exists)) * (c)) + (fsri_complement_source_exists))) -> (((exists fsri_height_exists_target. fsri_height_exists_target + S (fsri_complement_target_exists) = S ((S (fsri_complement_index_exists)) * (d))) /\ exists fsri_quotient_exists_target. (z) = fsri_quotient_exists_target * S ((S (fsri_complement_index_exists)) * (d)) + (fsri_complement_target_exists))) -> fsri_complement_target_exists + S fsri_complement_source_exists = (p))

Proof neighborhood

Direct theorem prerequisites

add_eq_zero_right · Stable closed succ_ne_zero · Stable closed le_succ · Stable closed le_refl · Stable closed beta_prefix_extend · Stable closed finite_lt_succ_eq_or_lt · Stable closed beta_at_unique · Stable closed beta_at_exists · Stable closed

Direct theorem dependents

FS000K four_square_odd_prime_half_coordinate_seed FS004K four_square_odd_prime_modular_seed

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

123 script commands · 27 reading checkpoints · 11 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.

01Fix variables and assumptionsL1–3

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
02Induction on lL4–5

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

  1. L4
    induction l
  2. L5
    intro hbounded
03Construct an explicit witnessL6–7

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

  1. L6
    exists 0
  2. L7
    exists 0
04Fix variables and assumptionsL8–13

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

  1. L8
    intro i
  2. L9
    intro v
  3. L10
    intro w
  4. L11
    intro hi
  5. L12
    intro hsource
  6. L13
    intro htarget
05Separate the logical casesL14–15

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

  1. L14
    exfalso
  2. L15
    cases hi
06Establish himpossibleL16–24

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

  1. L16
    have himpossible : S i = 0
  2. L17
    specialize add_eq_zero_right x
  3. L18
    specialize add_eq_zero_right (S i)
  4. L19
    apply add_eq_zero_right
  5. L20
    exact hi_witness
  6. L21
    specialize succ_ne_zero i
  7. L22
    apply succ_ne_zero
  8. L23
    exact himpossible
  9. L24
    intro hbounded
07Establish hprevious_boundL25–33

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

  1. L25
    have hprevious_bound : ∀ fom_index_fsri_previous_bound. Lt(fom_index_fsri_previous_bound,l) → ∃ x. BetaAt(b,c,fom_index_fsri_previous_bound,x) ∧ Lt(x,p)Definitions: Lt(fom_index_fsri_previous_bound,l)BetaAt(b,c,fom_index_fsri_previous_bound,x)Lt(x,p)Original native command in the exact edition
  2. L26
    intro i
  3. L27
    intro hi
  4. L28
    specialize hbounded i
  5. L29
    apply hbounded
  6. L30
    specialize le_succ (S i)
  7. L31
    specialize le_succ l
  8. L32
    apply le_succ
  9. L33
    exact hi
08Establish hpreviousL34–36

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

  1. L34
    have hprevious : ∃ z. ∃ d. ∀ x. ∀ y. ∀ n. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,d,x,n) → n + S y = pDefinitions: Lt(x,l)BetaAt(b,c,x,y)BetaAt(z,d,x,n)Original native command in the exact edition
  2. L35
    apply IH
  3. L36
    exact hprevious_bound
09Separate the logical casesL37–38

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

  1. L37
    cases hprevious
  2. L38
    cases hprevious_witness
10Establish hlastL39–43

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

  1. L39
    have hlast : ∃ v. BetaAt(b,c,l,v) ∧ Lt(v,p)Definitions: BetaAt(b,c,l,v)Lt(v,p)Original native command in the exact edition
  2. L40
    specialize hbounded l
  3. L41
    apply hbounded
  4. L42
    specialize le_refl (S l)
  5. L43
    exact le_refl
11Separate the logical casesL44–46

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

  1. L44
    cases hlast
  2. L45
    cases hlast_witness
  3. L46
    cases hlast_witness_right
12Establish hextendL47–52

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

  1. L47
    have hextend : ∃ z. ∃ d. BetaAt(z,d,l,x3) ∧ (∀ y. ∀ n. Lt(y,l) → BetaAt(x,x1,y,n) → BetaAt(z,d,y,n))Definitions: BetaAt(z,d,l,x3)Lt(y,l)BetaAt(x,x1,y,n)BetaAt(z,d,y,n)Original native command in the exact edition
  2. L48
    specialize beta_prefix_extend l
  3. L49
    specialize beta_prefix_extend x
  4. L50
    specialize beta_prefix_extend x1
  5. L51
    specialize beta_prefix_extend x3
  6. L52
    exact beta_prefix_extend
13Separate the logical casesL53–55

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

  1. L53
    cases hextend
  2. L54
    cases hextend_witness
  3. L55
    cases hextend_witness_witness
14Construct an explicit witnessL56–57

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

  1. L56
    exists x4
  2. L57
    exists x5
15Fix variables and assumptionsL58–63

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

  1. L58
    intro i
  2. L59
    intro v
  3. L60
    intro w
  4. L61
    intro hi
  5. L62
    intro hsource
  6. L63
    intro htarget
16Establish hsplitL64–68

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. L64
    have hsplit : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L65
    specialize finite_lt_succ_eq_or_lt l
  3. L66
    specialize finite_lt_succ_eq_or_lt i
  4. L67
    apply finite_lt_succ_eq_or_lt
  5. L68
    exact hi
17Separate the logical casesL69–69

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

  1. L69
    cases hsplit
18Calculate and transport equalitiesL70–73

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

  1. L70
    rewrite hsplit_left at hsource
  2. L71
    rewrite hsplit_left at hsource
  3. L72
    rewrite hsplit_left at htarget
  4. L73
    rewrite hsplit_left at htarget
19Establish hsource_valueL74–82

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

  1. L74
    have hsource_value : v = x2
  2. L75
    specialize beta_at_unique b
  3. L76
    specialize beta_at_unique c
  4. L77
    specialize beta_at_unique l
  5. L78
    specialize beta_at_unique v
  6. L79
    specialize beta_at_unique x2
  7. L80
    apply beta_at_unique
  8. L81
    exact hsource
  9. L82
    exact hlast_witness_left
20Establish htarget_valueL83–92

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

  1. L83
    have htarget_value : w = x3
  2. L84
    specialize beta_at_unique x4
  3. L85
    specialize beta_at_unique x5
  4. L86
    specialize beta_at_unique l
  5. L87
    specialize beta_at_unique w
  6. L88
    specialize beta_at_unique x3
  7. L89
    apply beta_at_unique
  8. L90
    exact htarget
  9. L91
    exact hextend_witness_witness_left
  10. L92
    rewrite hsource_value
21Calculate and transport equalitiesL93–93

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

  1. L93
    rewrite htarget_value
22Use earlier factsL94–94

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

  1. L94
    exact hlast_witness_right_witness
23Establish holdL95–99

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

  1. L95
    have hold : ∃ t. BetaAt(x,x1,i,t)Definitions: BetaAt(x,x1,i,t)Original native command in the exact edition
  2. L96
    specialize beta_at_exists x
  3. L97
    specialize beta_at_exists x1
  4. L98
    specialize beta_at_exists i
  5. L99
    exact beta_at_exists
24Separate the logical casesL100–100

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

  1. L100
    cases hold
25Establish htransportL101–106

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

  1. L101
    have htransport : BetaAt(x4,x5,i,x6)Definitions: BetaAt(x4,x5,i,x6)Original native command in the exact edition
  2. L102
    specialize hextend_witness_witness_right i
  3. L103
    specialize hextend_witness_witness_right x6
  4. L104
    apply hextend_witness_witness_right
  5. L105
    exact hsplit_right
  6. L106
    exact hold_witness
26Establish htarget_valueL107–116

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

  1. L107
    have htarget_value : w = x6
  2. L108
    specialize beta_at_unique x4
  3. L109
    specialize beta_at_unique x5
  4. L110
    specialize beta_at_unique i
  5. L111
    specialize beta_at_unique w
  6. L112
    specialize beta_at_unique x6
  7. L113
    apply beta_at_unique
  8. L114
    exact htarget
  9. L115
    exact htransport
  10. L116
    rewrite htarget_value
27Use earlier factsL117–123

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

  1. L117
    specialize hprevious_witness_witness i
  2. L118
    specialize hprevious_witness_witness v
  3. L119
    specialize hprevious_witness_witness x6
  4. L120
    apply hprevious_witness_witness
  5. L121
    exact hsplit_right
  6. L122
    exact hsource
  7. L123
    exact hold_witness

Library-wide reading audit

Original defined command ledger · 123 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004induction l
  5. 0005intro hbounded
  6. 0006exists 0
  7. 0007exists 0
  8. 0008intro i
  9. 0009intro v
  10. 0010intro w
  11. 0011intro hi
  12. 0012intro hsource
  13. 0013intro htarget
  14. 0014exfalso
  15. 0015cases hi
  16. 0016have himpossible : S i = 0
  17. 0017specialize add_eq_zero_right x
  18. 0018specialize add_eq_zero_right (S i)
  19. 0019apply add_eq_zero_right
  20. 0020exact hi_witness
  21. 0021specialize succ_ne_zero i
  22. 0022apply succ_ne_zero
  23. 0023exact himpossible
  24. 0024intro hbounded
  25. 0025have hprevious_bound : ∀ fom_index_fsri_previous_bound. Lt(fom_index_fsri_previous_bound,l) → ∃ x. BetaAt(b,c,fom_index_fsri_previous_bound,x) ∧ Lt(x,p)
    Exact native replay linehave hprevious_bound : forall fom_index_fsri_previous_bound. (exists fom_gap_fsri_previous_bound_index_bound. fom_gap_fsri_previous_bound_index_bound + S (fom_index_fsri_previous_bound) = l) -> exists fom_value_fsri_previous_bound. ((((exists fom_beta_height_fsri_previous_bound_entry. fom_beta_height_fsri_previous_bound_entry + S (fom_value_fsri_previous_bound) = S ((S (fom_index_fsri_previous_bound)) * c)) /\ exists fom_beta_quotient_fsri_previous_bound_entry. b = fom_beta_quotient_fsri_previous_bound_entry * S ((S (fom_index_fsri_previous_bound)) * c) + (fom_value_fsri_previous_bound))) /\ (exists fom_gap_fsri_previous_bound_value_bound. fom_gap_fsri_previous_bound_value_bound + S (fom_value_fsri_previous_bound) = p))
  26. 0026intro i
  27. 0027intro hi
  28. 0028specialize hbounded i
  29. 0029apply hbounded
  30. 0030specialize le_succ (S i)
  31. 0031specialize le_succ l
  32. 0032apply le_succ
  33. 0033exact hi
  34. 0034have hprevious : ∃ z. ∃ d. ∀ x. ∀ y. ∀ n. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,d,x,n) → n + S y = p
    Exact native replay linehave hprevious : exists z d. (forall fsri_complement_index_previous fsri_complement_source_previous fsri_complement_target_previous. (exists fsri_gap_previous_index. fsri_gap_previous_index + S (fsri_complement_index_previous) = (l)) -> (((exists fsri_height_previous_source. fsri_height_previous_source + S (fsri_complement_source_previous) = S ((S (fsri_complement_index_previous)) * (c))) /\ exists fsri_quotient_previous_source. (b) = fsri_quotient_previous_source * S ((S (fsri_complement_index_previous)) * (c)) + (fsri_complement_source_previous))) -> (((exists fsri_height_previous_target. fsri_height_previous_target + S (fsri_complement_target_previous) = S ((S (fsri_complement_index_previous)) * (d))) /\ exists fsri_quotient_previous_target. (z) = fsri_quotient_previous_target * S ((S (fsri_complement_index_previous)) * (d)) + (fsri_complement_target_previous))) -> fsri_complement_target_previous + S fsri_complement_source_previous = (p))
  35. 0035apply IH
  36. 0036exact hprevious_bound
  37. 0037cases hprevious
  38. 0038cases hprevious_witness
  39. 0039have hlast : ∃ v. BetaAt(b,c,l,v) ∧ Lt(v,p)
    Exact native replay linehave hlast : exists v. ((((exists fsri_height_complement_last_source. fsri_height_complement_last_source + S (v) = S ((S (l)) * (c))) /\ exists fsri_quotient_complement_last_source. (b) = fsri_quotient_complement_last_source * S ((S (l)) * (c)) + (v))) /\ (exists fsri_gap_complement_last_bound. fsri_gap_complement_last_bound + S (v) = (p)))
  40. 0040specialize hbounded l
  41. 0041apply hbounded
  42. 0042specialize le_refl (S l)
  43. 0043exact le_refl
  44. 0044cases hlast
  45. 0045cases hlast_witness
  46. 0046cases hlast_witness_right
  47. 0047have hextend : ∃ z. ∃ d. BetaAt(z,d,l,x3) ∧ (∀ y. ∀ n. Lt(y,l) → BetaAt(x,x1,y,n) → BetaAt(z,d,y,n))
    Exact native replay linehave hextend : exists z d. ((((exists fsri_height_complement_extension_last. fsri_height_complement_extension_last + S (x3) = S ((S (l)) * (d))) /\ exists fsri_quotient_complement_extension_last. (z) = fsri_quotient_complement_extension_last * S ((S (l)) * (d)) + (x3))) /\ forall i v. (exists fsri_gap_complement_extension_old_bound. fsri_gap_complement_extension_old_bound + S (i) = (l)) -> (((exists fsri_height_complement_extension_old. fsri_height_complement_extension_old + S (v) = S ((S (i)) * (x1))) /\ exists fsri_quotient_complement_extension_old. (x) = fsri_quotient_complement_extension_old * S ((S (i)) * (x1)) + (v))) -> (((exists fsri_height_complement_extension_new. fsri_height_complement_extension_new + S (v) = S ((S (i)) * (d))) /\ exists fsri_quotient_complement_extension_new. (z) = fsri_quotient_complement_extension_new * S ((S (i)) * (d)) + (v))))
  48. 0048specialize beta_prefix_extend l
  49. 0049specialize beta_prefix_extend x
  50. 0050specialize beta_prefix_extend x1
  51. 0051specialize beta_prefix_extend x3
  52. 0052exact beta_prefix_extend
  53. 0053cases hextend
  54. 0054cases hextend_witness
  55. 0055cases hextend_witness_witness
  56. 0056exists x4
  57. 0057exists x5
  58. 0058intro i
  59. 0059intro v
  60. 0060intro w
  61. 0061intro hi
  62. 0062intro hsource
  63. 0063intro htarget
  64. 0064have hsplit : i = l ∨ Lt(i,l)
    Exact native replay linehave hsplit : i = l \/ (exists fsri_gap_complement_split. fsri_gap_complement_split + S (i) = (l))
  65. 0065specialize finite_lt_succ_eq_or_lt l
  66. 0066specialize finite_lt_succ_eq_or_lt i
  67. 0067apply finite_lt_succ_eq_or_lt
  68. 0068exact hi
  69. 0069cases hsplit
  70. 0070rewrite hsplit_left at hsource
  71. 0071rewrite hsplit_left at hsource
  72. 0072rewrite hsplit_left at htarget
  73. 0073rewrite hsplit_left at htarget
  74. 0074have hsource_value : v = x2
  75. 0075specialize beta_at_unique b
  76. 0076specialize beta_at_unique c
  77. 0077specialize beta_at_unique l
  78. 0078specialize beta_at_unique v
  79. 0079specialize beta_at_unique x2
  80. 0080apply beta_at_unique
  81. 0081exact hsource
  82. 0082exact hlast_witness_left
  83. 0083have htarget_value : w = x3
  84. 0084specialize beta_at_unique x4
  85. 0085specialize beta_at_unique x5
  86. 0086specialize beta_at_unique l
  87. 0087specialize beta_at_unique w
  88. 0088specialize beta_at_unique x3
  89. 0089apply beta_at_unique
  90. 0090exact htarget
  91. 0091exact hextend_witness_witness_left
  92. 0092rewrite hsource_value
  93. 0093rewrite htarget_value
  94. 0094exact hlast_witness_right_witness
  95. 0095have hold : ∃ t. BetaAt(x,x1,i,t)
    Exact native replay linehave hold : exists t. (((exists fsri_height_complement_old_entry. fsri_height_complement_old_entry + S (t) = S ((S (i)) * (x1))) /\ exists fsri_quotient_complement_old_entry. (x) = fsri_quotient_complement_old_entry * S ((S (i)) * (x1)) + (t)))
  96. 0096specialize beta_at_exists x
  97. 0097specialize beta_at_exists x1
  98. 0098specialize beta_at_exists i
  99. 0099exact beta_at_exists
  100. 0100cases hold
  101. 0101have htransport : BetaAt(x4,x5,i,x6)
    Exact native replay linehave htransport : ((exists fsri_height_complement_old_transport. fsri_height_complement_old_transport + S (x6) = S ((S (i)) * (x5))) /\ exists fsri_quotient_complement_old_transport. (x4) = fsri_quotient_complement_old_transport * S ((S (i)) * (x5)) + (x6))
  102. 0102specialize hextend_witness_witness_right i
  103. 0103specialize hextend_witness_witness_right x6
  104. 0104apply hextend_witness_witness_right
  105. 0105exact hsplit_right
  106. 0106exact hold_witness
  107. 0107have htarget_value : w = x6
  108. 0108specialize beta_at_unique x4
  109. 0109specialize beta_at_unique x5
  110. 0110specialize beta_at_unique i
  111. 0111specialize beta_at_unique w
  112. 0112specialize beta_at_unique x6
  113. 0113apply beta_at_unique
  114. 0114exact htarget
  115. 0115exact htransport
  116. 0116rewrite htarget_value
  117. 0117specialize hprevious_witness_witness i
  118. 0118specialize hprevious_witness_witness v
  119. 0119specialize hprevious_witness_witness x6
  120. 0120apply hprevious_witness_witness
  121. 0121exact hsplit_right
  122. 0122exact hsource
  123. 0123exact hold_witness