FS004B · theorem body

four_square_square_residue_prefix_exists

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

For every nonzero modulus and arbitrary finite length, canonical square residues are constructively encoded as one beta prefix.

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. ∀ l. ¬p = 0 → ∃ x. ∃ y. ∀ z. Lt(z,l) → ∃ n. ∃ m. z · z = p · n + m ∧ (Lt(m,p) ∧ BetaAt(x,y,z,m))

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 PD0007 DivRem PD0013 BetaAt PD0018 Range PD0040 DivisionPrefix
Exact expanded first-order statement
forall p l. ~(p = 0) -> exists b c. (forall fsri_index_exists. (exists fsri_gap_exists_index. fsri_gap_exists_index + S (fsri_index_exists) = (l)) -> exists fsri_quotient_exists fsri_residue_exists. (fsri_index_exists * fsri_index_exists = (p) * fsri_quotient_exists + fsri_residue_exists /\ ((exists fsri_gap_exists_residue. fsri_gap_exists_residue + S (fsri_residue_exists) = (p)) /\ (((exists fsri_height_exists_entry. fsri_height_exists_entry + S (fsri_residue_exists) = S ((S (fsri_index_exists)) * (c))) /\ exists fsri_quotient_exists_entry. (b) = fsri_quotient_exists_entry * S ((S (fsri_index_exists)) * (c)) + (fsri_residue_exists))))))

Proof neighborhood

Direct theorem prerequisites

beta_range_exists · Stable closed beta_pointwise_mul_prefix_exists · Alpha closed beta_division_prefix_exists · Alpha closed zero_add · 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

70 script commands · 20 reading checkpoints · 7 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 l
  3. L3
    intro hnonzero
02Establish hrangeL4–7

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

  1. L4
    have hrange : ∃ b. ∃ c. Range(b,c,0,l)Definitions: Range(b,c,0,l)Original native command in the exact edition
  2. L5
    specialize beta_range_exists 0
  3. L6
    specialize beta_range_exists l
  4. L7
    exact beta_range_exists
03Separate the logical casesL8–9

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

  1. L8
    cases hrange
  2. L9
    cases hrange_witness
04Establish hsquaresL10–16

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

  1. L10
    have hsquares : ∃ b. ∃ c. ∀ y. ∀ z. ∀ n. ∀ m. Lt(y,l) → BetaAt(x,x1,y,z) → BetaAt(x,x1,y,n) → BetaAt(b,c,y,m) → m = z · nDefinitions: Lt(y,l)BetaAt(x,x1,y,z)BetaAt(x,x1,y,n)BetaAt(b,c,y,m)Original native command in the exact edition
  2. L11
    specialize beta_pointwise_mul_prefix_exists x
  3. L12
    specialize beta_pointwise_mul_prefix_exists x1
  4. L13
    specialize beta_pointwise_mul_prefix_exists x
  5. L14
    specialize beta_pointwise_mul_prefix_exists x1
  6. L15
    specialize beta_pointwise_mul_prefix_exists l
  7. L16
    exact beta_pointwise_mul_prefix_exists
05Separate the logical casesL17–18

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

  1. L17
    cases hsquares
  2. L18
    cases hsquares_witness
06Establish hdivisionsL19–25

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

  1. L19
    have hdivisions : ∃ qb. ∃ qc. ∃ rb. ∃ rc. DivisionPrefix(p,x2,x3,qb,qc,rb,rc,l)Definitions: DivisionPrefix(p,x2,x3,qb,qc,rb,rc,l)Original native command in the exact edition
  2. L20
    specialize beta_division_prefix_exists p
  3. L21
    specialize beta_division_prefix_exists x2
  4. L22
    specialize beta_division_prefix_exists x3
  5. L23
    specialize beta_division_prefix_exists l
  6. L24
    apply beta_division_prefix_exists
  7. L25
    exact hnonzero
07Separate the logical casesL26–29

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

  1. L26
    cases hdivisions
  2. L27
    cases hdivisions_witness
  3. L28
    cases hdivisions_witness_witness
  4. L29
    cases hdivisions_witness_witness_witness
08Construct an explicit witnessL30–31

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

  1. L30
    exists x6
  2. L31
    exists x7
09Fix variables and assumptionsL32–33

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

  1. L32
    intro i
  2. L33
    intro hi
10Establish hindex_zeroL34–37

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

  1. L34
    have hindex_zero : BetaAt(x,x1,i,0 + i)Definitions: BetaAt(x,x1,i,0 + i)Original native command in the exact edition
  2. L35
    specialize hrange_witness_witness i
  3. L36
    apply hrange_witness_witness
  4. L37
    exact hi
11Establish hzeroL38–41

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

  1. L38
    have hzero : 0 + i = i
  2. L39
    apply zero_add
  3. L40
    rewrite hzero at hindex_zero
  4. L41
    rewrite hzero at hindex_zero
12Establish hdivisionL42–45

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

  1. L42
    have hdivision : ∃ v. ∃ q. ∃ r. BetaAt(x2,x3,i,v) ∧ (BetaAt(x4,x5,i,q) ∧ (BetaAt(x6,x7,i,r) ∧ DivRem(v,p,q,r)))Definitions: BetaAt(x2,x3,i,v)BetaAt(x4,x5,i,q)BetaAt(x6,x7,i,r)DivRem(v,p,q,r)Original native command in the exact edition
  2. L43
    specialize hdivisions_witness_witness_witness_witness i
  3. L44
    apply hdivisions_witness_witness_witness_witness
  4. L45
    exact hi
13Separate the logical casesL46–52

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

  1. L46
    cases hdivision
  2. L47
    cases hdivision_witness
  3. L48
    cases hdivision_witness_witness
  4. L49
    cases hdivision_witness_witness_witness
  5. L50
    cases hdivision_witness_witness_witness_right
  6. L51
    cases hdivision_witness_witness_witness_right_right
  7. L52
    cases hdivision_witness_witness_witness_right_right_right
14Establish hvalueL53–62

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

  1. L53
    have hvalue : x8 = i * i
  2. L54
    specialize hsquares_witness_witness i
  3. L55
    specialize hsquares_witness_witness i
  4. L56
    specialize hsquares_witness_witness i
  5. L57
    specialize hsquares_witness_witness x8
  6. L58
    apply hsquares_witness_witness
  7. L59
    exact hi
  8. L60
    exact hindex_zero
  9. L61
    exact hindex_zero
  10. L62
    exact hdivision_witness_witness_witness_left
15Construct an explicit witnessL63–64

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

  1. L63
    exists x9
  2. L64
    exists x10
16Separate the logical casesL65–65

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

  1. L65
    split
17Calculate and transport equalitiesL66–66

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

  1. L66
    rewrite <- hvalue
18Use earlier factsL67–67

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

  1. L67
    exact hdivision_witness_witness_witness_right_right_right_left
19Separate the logical casesL68–68

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

  1. L68
    split
20Use earlier factsL69–70

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

  1. L69
    exact hdivision_witness_witness_witness_right_right_right_right
  2. L70
    exact hdivision_witness_witness_witness_right_right_left

Library-wide reading audit

Original defined command ledger · 70 lines
  1. 0001intro p
  2. 0002intro l
  3. 0003intro hnonzero
  4. 0004have hrange : ∃ b. ∃ c. Range(b,c,0,l)
    Exact native replay linehave hrange : exists b c. forall i. (exists fsri_gap_range_index. fsri_gap_range_index + S (i) = (l)) -> (((exists fsri_height_range_entry. fsri_height_range_entry + S (0 + i) = S ((S (i)) * (c))) /\ exists fsri_quotient_range_entry. (b) = fsri_quotient_range_entry * S ((S (i)) * (c)) + (0 + i)))
  5. 0005specialize beta_range_exists 0
  6. 0006specialize beta_range_exists l
  7. 0007exact beta_range_exists
  8. 0008cases hrange
  9. 0009cases hrange_witness
  10. 0010have hsquares : ∃ b. ∃ c. ∀ y. ∀ z. ∀ n. ∀ m. Lt(y,l) → BetaAt(x,x1,y,z) → BetaAt(x,x1,y,n) → BetaAt(b,c,y,m) → m = z · n
    Exact native replay linehave hsquares : exists b c. (forall fpmp_index_fsri_square_values fpmp_left_fsri_square_values fpmp_right_fsri_square_values fpmp_target_fsri_square_values. (exists fpmp_gap_fsri_square_values. fpmp_gap_fsri_square_values + S fpmp_index_fsri_square_values = l) -> (((exists ff_h_fpmp_fsri_square_values_left. ff_h_fpmp_fsri_square_values_left + S (fpmp_left_fsri_square_values) = S ((S (fpmp_index_fsri_square_values)) * x1)) /\ exists ff_q_fpmp_fsri_square_values_left. x = ff_q_fpmp_fsri_square_values_left * S ((S (fpmp_index_fsri_square_values)) * x1) + (fpmp_left_fsri_square_values))) -> (((exists ff_h_fpmp_fsri_square_values_right. ff_h_fpmp_fsri_square_values_right + S (fpmp_right_fsri_square_values) = S ((S (fpmp_index_fsri_square_values)) * x1)) /\ exists ff_q_fpmp_fsri_square_values_right. x = ff_q_fpmp_fsri_square_values_right * S ((S (fpmp_index_fsri_square_values)) * x1) + (fpmp_right_fsri_square_values))) -> (((exists ff_h_fpmp_fsri_square_values_target. ff_h_fpmp_fsri_square_values_target + S (fpmp_target_fsri_square_values) = S ((S (fpmp_index_fsri_square_values)) * c)) /\ exists ff_q_fpmp_fsri_square_values_target. b = ff_q_fpmp_fsri_square_values_target * S ((S (fpmp_index_fsri_square_values)) * c) + (fpmp_target_fsri_square_values))) -> fpmp_target_fsri_square_values = fpmp_left_fsri_square_values * fpmp_right_fsri_square_values)
  11. 0011specialize beta_pointwise_mul_prefix_exists x
  12. 0012specialize beta_pointwise_mul_prefix_exists x1
  13. 0013specialize beta_pointwise_mul_prefix_exists x
  14. 0014specialize beta_pointwise_mul_prefix_exists x1
  15. 0015specialize beta_pointwise_mul_prefix_exists l
  16. 0016exact beta_pointwise_mul_prefix_exists
  17. 0017cases hsquares
  18. 0018cases hsquares_witness
  19. 0019have hdivisions : ∃ qb. ∃ qc. ∃ rb. ∃ rc. DivisionPrefix(p,x2,x3,qb,qc,rb,rc,l)
    Exact native replay linehave hdivisions : exists qb qc rb rc. (forall fdp_index_fsri_square_divisions. (exists gsp_lt_gap_fsri_square_divisions_index_bound. gsp_lt_gap_fsri_square_divisions_index_bound + S fdp_index_fsri_square_divisions = l) -> exists fdp_value_fsri_square_divisions fdp_quotient_fsri_square_divisions fdp_remainder_fsri_square_divisions. (((exists ff_h_fdp_fsri_square_divisions_source. ff_h_fdp_fsri_square_divisions_source + S (fdp_value_fsri_square_divisions) = S ((S (fdp_index_fsri_square_divisions)) * x3)) /\ exists ff_q_fdp_fsri_square_divisions_source. x2 = ff_q_fdp_fsri_square_divisions_source * S ((S (fdp_index_fsri_square_divisions)) * x3) + (fdp_value_fsri_square_divisions))) /\ ((((exists ff_h_fdp_fsri_square_divisions_quotient_entry. ff_h_fdp_fsri_square_divisions_quotient_entry + S (fdp_quotient_fsri_square_divisions) = S ((S (fdp_index_fsri_square_divisions)) * qc)) /\ exists ff_q_fdp_fsri_square_divisions_quotient_entry. qb = ff_q_fdp_fsri_square_divisions_quotient_entry * S ((S (fdp_index_fsri_square_divisions)) * qc) + (fdp_quotient_fsri_square_divisions))) /\ ((((exists ff_h_fdp_fsri_square_divisions_remainder_entry. ff_h_fdp_fsri_square_divisions_remainder_entry + S (fdp_remainder_fsri_square_divisions) = S ((S (fdp_index_fsri_square_divisions)) * rc)) /\ exists ff_q_fdp_fsri_square_divisions_remainder_entry. rb = ff_q_fdp_fsri_square_divisions_remainder_entry * S ((S (fdp_index_fsri_square_divisions)) * rc) + (fdp_remainder_fsri_square_divisions))) /\ (fdp_value_fsri_square_divisions = p * fdp_quotient_fsri_square_divisions + fdp_remainder_fsri_square_divisions /\ (exists gsp_lt_gap_fsri_square_divisions_remainder_bound. gsp_lt_gap_fsri_square_divisions_remainder_bound + S fdp_remainder_fsri_square_divisions = p)))))
  20. 0020specialize beta_division_prefix_exists p
  21. 0021specialize beta_division_prefix_exists x2
  22. 0022specialize beta_division_prefix_exists x3
  23. 0023specialize beta_division_prefix_exists l
  24. 0024apply beta_division_prefix_exists
  25. 0025exact hnonzero
  26. 0026cases hdivisions
  27. 0027cases hdivisions_witness
  28. 0028cases hdivisions_witness_witness
  29. 0029cases hdivisions_witness_witness_witness
  30. 0030exists x6
  31. 0031exists x7
  32. 0032intro i
  33. 0033intro hi
  34. 0034have hindex_zero : BetaAt(x,x1,i,0 + i)
    Exact native replay linehave hindex_zero : ((exists fsri_height_square_index_zero. fsri_height_square_index_zero + S (0 + i) = S ((S (i)) * (x1))) /\ exists fsri_quotient_square_index_zero. (x) = fsri_quotient_square_index_zero * S ((S (i)) * (x1)) + (0 + i))
  35. 0035specialize hrange_witness_witness i
  36. 0036apply hrange_witness_witness
  37. 0037exact hi
  38. 0038have hzero : 0 + i = i
  39. 0039apply zero_add
  40. 0040rewrite hzero at hindex_zero
  41. 0041rewrite hzero at hindex_zero
  42. 0042have hdivision : ∃ v. ∃ q. ∃ r. BetaAt(x2,x3,i,v) ∧ (BetaAt(x4,x5,i,q) ∧ (BetaAt(x6,x7,i,r) ∧ DivRem(v,p,q,r)))
    Exact native replay linehave hdivision : exists v q r. ((((exists fsri_height_square_source_value. fsri_height_square_source_value + S (v) = S ((S (i)) * (x3))) /\ exists fsri_quotient_square_source_value. (x2) = fsri_quotient_square_source_value * S ((S (i)) * (x3)) + (v))) /\ ((((exists fsri_height_square_quotient_value. fsri_height_square_quotient_value + S (q) = S ((S (i)) * (x5))) /\ exists fsri_quotient_square_quotient_value. (x4) = fsri_quotient_square_quotient_value * S ((S (i)) * (x5)) + (q))) /\ ((((exists fsri_height_square_remainder_value. fsri_height_square_remainder_value + S (r) = S ((S (i)) * (x7))) /\ exists fsri_quotient_square_remainder_value. (x6) = fsri_quotient_square_remainder_value * S ((S (i)) * (x7)) + (r))) /\ (v = p * q + r /\ (exists fsri_gap_square_remainder_bound. fsri_gap_square_remainder_bound + S (r) = (p))))))
  43. 0043specialize hdivisions_witness_witness_witness_witness i
  44. 0044apply hdivisions_witness_witness_witness_witness
  45. 0045exact hi
  46. 0046cases hdivision
  47. 0047cases hdivision_witness
  48. 0048cases hdivision_witness_witness
  49. 0049cases hdivision_witness_witness_witness
  50. 0050cases hdivision_witness_witness_witness_right
  51. 0051cases hdivision_witness_witness_witness_right_right
  52. 0052cases hdivision_witness_witness_witness_right_right_right
  53. 0053have hvalue : x8 = i * i
  54. 0054specialize hsquares_witness_witness i
  55. 0055specialize hsquares_witness_witness i
  56. 0056specialize hsquares_witness_witness i
  57. 0057specialize hsquares_witness_witness x8
  58. 0058apply hsquares_witness_witness
  59. 0059exact hi
  60. 0060exact hindex_zero
  61. 0061exact hindex_zero
  62. 0062exact hdivision_witness_witness_witness_left
  63. 0063exists x9
  64. 0064exists x10
  65. 0065split
  66. 0066rewrite <- hvalue
  67. 0067exact hdivision_witness_witness_witness_right_right_right_left
  68. 0068split
  69. 0069exact hdivision_witness_witness_witness_right_right_right_right
  70. 0070exact hdivision_witness_witness_witness_right_right_left