FS004H · theorem body

four_square_complement_prefix_bounded

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

The pointwise predecessor complement of any bounded residue prefix is itself bounded by the modulus.

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. ∀ z. ∀ d. ∀ l. (∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,p)) → (∀ x. ∀ y. ∀ n. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,d,x,n) → n + S y = p) → ∀ x. Lt(x,l) → ∃ y. BetaAt(z,d,x,y) ∧ Lt(y,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 z d l. (forall fom_index_fsri_complement_bounded_source. (exists fom_gap_fsri_complement_bounded_source_index_bound. fom_gap_fsri_complement_bounded_source_index_bound + S (fom_index_fsri_complement_bounded_source) = l) -> exists fom_value_fsri_complement_bounded_source. ((((exists fom_beta_height_fsri_complement_bounded_source_entry. fom_beta_height_fsri_complement_bounded_source_entry + S (fom_value_fsri_complement_bounded_source) = S ((S (fom_index_fsri_complement_bounded_source)) * c)) /\ exists fom_beta_quotient_fsri_complement_bounded_source_entry. b = fom_beta_quotient_fsri_complement_bounded_source_entry * S ((S (fom_index_fsri_complement_bounded_source)) * c) + (fom_value_fsri_complement_bounded_source))) /\ (exists fom_gap_fsri_complement_bounded_source_value_bound. fom_gap_fsri_complement_bounded_source_value_bound + S (fom_value_fsri_complement_bounded_source) = p))) -> (forall fsri_complement_index_bounded_alignment fsri_complement_source_bounded_alignment fsri_complement_target_bounded_alignment. (exists fsri_gap_bounded_alignment_index. fsri_gap_bounded_alignment_index + S (fsri_complement_index_bounded_alignment) = (l)) -> (((exists fsri_height_bounded_alignment_source. fsri_height_bounded_alignment_source + S (fsri_complement_source_bounded_alignment) = S ((S (fsri_complement_index_bounded_alignment)) * (c))) /\ exists fsri_quotient_bounded_alignment_source. (b) = fsri_quotient_bounded_alignment_source * S ((S (fsri_complement_index_bounded_alignment)) * (c)) + (fsri_complement_source_bounded_alignment))) -> (((exists fsri_height_bounded_alignment_target. fsri_height_bounded_alignment_target + S (fsri_complement_target_bounded_alignment) = S ((S (fsri_complement_index_bounded_alignment)) * (d))) /\ exists fsri_quotient_bounded_alignment_target. (z) = fsri_quotient_bounded_alignment_target * S ((S (fsri_complement_index_bounded_alignment)) * (d)) + (fsri_complement_target_bounded_alignment))) -> fsri_complement_target_bounded_alignment + S fsri_complement_source_bounded_alignment = (p)) -> (forall fom_index_fsri_complement_bounded_result. (exists fom_gap_fsri_complement_bounded_result_index_bound. fom_gap_fsri_complement_bounded_result_index_bound + S (fom_index_fsri_complement_bounded_result) = l) -> exists fom_value_fsri_complement_bounded_result. ((((exists fom_beta_height_fsri_complement_bounded_result_entry. fom_beta_height_fsri_complement_bounded_result_entry + S (fom_value_fsri_complement_bounded_result) = S ((S (fom_index_fsri_complement_bounded_result)) * d)) /\ exists fom_beta_quotient_fsri_complement_bounded_result_entry. z = fom_beta_quotient_fsri_complement_bounded_result_entry * S ((S (fom_index_fsri_complement_bounded_result)) * d) + (fom_value_fsri_complement_bounded_result))) /\ (exists fom_gap_fsri_complement_bounded_result_value_bound. fom_gap_fsri_complement_bounded_result_value_bound + S (fom_value_fsri_complement_bounded_result) = p)))

Proof neighborhood

Direct theorem prerequisites

beta_at_exists · Stable closed FS004G four_square_complement_gap_symmetry

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

37 script commands · 11 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.

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)
four square complement gap symmetry
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro z
  5. L5
    intro d
  6. L6
    intro l
  7. L7
    intro hbounded
  8. L8
    intro hcomplement
  9. L9
    intro i
  10. L10
    intro hi
02Establish hsourceL11–14

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

  1. L11
    have hsource : ∃ v. BetaAt(b,c,i,v) ∧ Lt(v,p)Definitions: BetaAt(b,c,i,v)Lt(v,p)Original native command in the exact edition
  2. L12
    specialize hbounded i
  3. L13
    apply hbounded
  4. L14
    exact hi
03Separate the logical casesL15–16

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

  1. L15
    cases hsource
  2. L16
    cases hsource_witness
04Establish htargetL17–21

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

  1. L17
    have htarget : ∃ w. BetaAt(z,d,i,w)Definitions: BetaAt(z,d,i,w)Original native command in the exact edition
  2. L18
    specialize beta_at_exists z
  3. L19
    specialize beta_at_exists d
  4. L20
    specialize beta_at_exists i
  5. L21
    exact beta_at_exists
05Separate the logical casesL22–22

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

  1. L22
    cases htarget
06Construct an explicit witnessL23–23

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

  1. L23
    exists x1
07Separate the logical casesL24–24

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

  1. L24
    split
08Use earlier factsL25–25

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

  1. L25
    exact htarget_witness
09Construct an explicit witnessL26–26

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

  1. L26
    exists x
10Use earlier factsL27–36

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

  1. L27
    specialize four_square_complement_gap_symmetry p
  2. L28
    specialize four_square_complement_gap_symmetry x
  3. L29
    specialize four_square_complement_gap_symmetry x1
  4. L30
    apply four_square_complement_gap_symmetry
  5. L31
    specialize hcomplement i
  6. L32
    specialize hcomplement x
  7. L33
    specialize hcomplement x1
  8. L34
    apply hcomplement
  9. L35
    exact hi
  10. L36
    exact hsource_witness_left
11Use earlier factsL37–37

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

  1. L37
    exact htarget_witness

Library-wide reading audit

Original defined command ledger · 37 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro z
  5. 0005intro d
  6. 0006intro l
  7. 0007intro hbounded
  8. 0008intro hcomplement
  9. 0009intro i
  10. 0010intro hi
  11. 0011have hsource : ∃ v. BetaAt(b,c,i,v) ∧ Lt(v,p)
    Exact native replay linehave hsource : exists v. ((((exists fsri_height_complement_bound_source_entry. fsri_height_complement_bound_source_entry + S (v) = S ((S (i)) * (c))) /\ exists fsri_quotient_complement_bound_source_entry. (b) = fsri_quotient_complement_bound_source_entry * S ((S (i)) * (c)) + (v))) /\ (exists fsri_gap_complement_bound_source_value. fsri_gap_complement_bound_source_value + S (v) = (p)))
  12. 0012specialize hbounded i
  13. 0013apply hbounded
  14. 0014exact hi
  15. 0015cases hsource
  16. 0016cases hsource_witness
  17. 0017have htarget : ∃ w. BetaAt(z,d,i,w)
    Exact native replay linehave htarget : exists w. (((exists fsri_height_complement_bound_target_entry. fsri_height_complement_bound_target_entry + S (w) = S ((S (i)) * (d))) /\ exists fsri_quotient_complement_bound_target_entry. (z) = fsri_quotient_complement_bound_target_entry * S ((S (i)) * (d)) + (w)))
  18. 0018specialize beta_at_exists z
  19. 0019specialize beta_at_exists d
  20. 0020specialize beta_at_exists i
  21. 0021exact beta_at_exists
  22. 0022cases htarget
  23. 0023exists x1
  24. 0024split
  25. 0025exact htarget_witness
  26. 0026exists x
  27. 0027specialize four_square_complement_gap_symmetry p
  28. 0028specialize four_square_complement_gap_symmetry x
  29. 0029specialize four_square_complement_gap_symmetry x1
  30. 0030apply four_square_complement_gap_symmetry
  31. 0031specialize hcomplement i
  32. 0032specialize hcomplement x
  33. 0033specialize hcomplement x1
  34. 0034apply hcomplement
  35. 0035exact hi
  36. 0036exact hsource_witness_left
  37. 0037exact htarget_witness