FS004H

four_square_complement_prefix_bounded

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

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

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.

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

Constructive proof overview

Generated structural guide

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

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

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Historical empty-context replay experiment only; that experiment persisted no certificate and granted no release authority. Current checked use follows separately sealed, independently verified proof bundles; there is no Stable promotion.

Proof neighborhood

Direct dependencies

beta_at_exists Stable theorem; checked-use authorized FS004G four_square_complement_gap_symmetry

Direct dependents

FS000K four_square_odd_prime_half_coordinate_seed FS004K four_square_odd_prime_modular_seed

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

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.

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 : 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)))
  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 : 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)))
  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 exact 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 : 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 : 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