FS004I · theorem body

four_square_complement_prefix_preserves_injectivity

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

Taking p-1 residue complements preserves constructive injectivity of an arbitrary beta-coded finite prefix.

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. InjectivePrefix(b,c,l) → (∀ x. ∀ y. ∀ n. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,d,x,n) → n + S y = p) → InjectivePrefix(z,d,l)

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 PD0025 InjectivePrefix

In local proof propositions

PD0013 BetaAt
Exact expanded first-order statement
forall p b c z d l. (forall fp_i_fsri_complement_injective_source fp_j_fsri_complement_injective_source fp_value_fsri_complement_injective_source. (exists fp_gap_fsri_complement_injective_source_i. fp_gap_fsri_complement_injective_source_i + S fp_i_fsri_complement_injective_source = l) -> (exists fp_gap_fsri_complement_injective_source_j. fp_gap_fsri_complement_injective_source_j + S fp_j_fsri_complement_injective_source = l) -> (((exists ff_h_fsri_complement_injective_source_left. ff_h_fsri_complement_injective_source_left + S (fp_value_fsri_complement_injective_source) = S ((S (fp_i_fsri_complement_injective_source)) * c)) /\ exists ff_q_fsri_complement_injective_source_left. b = ff_q_fsri_complement_injective_source_left * S ((S (fp_i_fsri_complement_injective_source)) * c) + (fp_value_fsri_complement_injective_source))) -> (((exists ff_h_fsri_complement_injective_source_right. ff_h_fsri_complement_injective_source_right + S (fp_value_fsri_complement_injective_source) = S ((S (fp_j_fsri_complement_injective_source)) * c)) /\ exists ff_q_fsri_complement_injective_source_right. b = ff_q_fsri_complement_injective_source_right * S ((S (fp_j_fsri_complement_injective_source)) * c) + (fp_value_fsri_complement_injective_source))) -> fp_i_fsri_complement_injective_source = fp_j_fsri_complement_injective_source) -> (forall fsri_complement_index_injective_alignment fsri_complement_source_injective_alignment fsri_complement_target_injective_alignment. (exists fsri_gap_injective_alignment_index. fsri_gap_injective_alignment_index + S (fsri_complement_index_injective_alignment) = (l)) -> (((exists fsri_height_injective_alignment_source. fsri_height_injective_alignment_source + S (fsri_complement_source_injective_alignment) = S ((S (fsri_complement_index_injective_alignment)) * (c))) /\ exists fsri_quotient_injective_alignment_source. (b) = fsri_quotient_injective_alignment_source * S ((S (fsri_complement_index_injective_alignment)) * (c)) + (fsri_complement_source_injective_alignment))) -> (((exists fsri_height_injective_alignment_target. fsri_height_injective_alignment_target + S (fsri_complement_target_injective_alignment) = S ((S (fsri_complement_index_injective_alignment)) * (d))) /\ exists fsri_quotient_injective_alignment_target. (z) = fsri_quotient_injective_alignment_target * S ((S (fsri_complement_index_injective_alignment)) * (d)) + (fsri_complement_target_injective_alignment))) -> fsri_complement_target_injective_alignment + S fsri_complement_source_injective_alignment = (p)) -> (forall fp_i_fsri_complement_injective_result fp_j_fsri_complement_injective_result fp_value_fsri_complement_injective_result. (exists fp_gap_fsri_complement_injective_result_i. fp_gap_fsri_complement_injective_result_i + S fp_i_fsri_complement_injective_result = l) -> (exists fp_gap_fsri_complement_injective_result_j. fp_gap_fsri_complement_injective_result_j + S fp_j_fsri_complement_injective_result = l) -> (((exists ff_h_fsri_complement_injective_result_left. ff_h_fsri_complement_injective_result_left + S (fp_value_fsri_complement_injective_result) = S ((S (fp_i_fsri_complement_injective_result)) * d)) /\ exists ff_q_fsri_complement_injective_result_left. z = ff_q_fsri_complement_injective_result_left * S ((S (fp_i_fsri_complement_injective_result)) * d) + (fp_value_fsri_complement_injective_result))) -> (((exists ff_h_fsri_complement_injective_result_right. ff_h_fsri_complement_injective_result_right + S (fp_value_fsri_complement_injective_result) = S ((S (fp_j_fsri_complement_injective_result)) * d)) /\ exists ff_q_fsri_complement_injective_result_right. z = ff_q_fsri_complement_injective_result_right * S ((S (fp_j_fsri_complement_injective_result)) * d) + (fp_value_fsri_complement_injective_result))) -> fp_i_fsri_complement_injective_result = fp_j_fsri_complement_injective_result)

Proof neighborhood

Direct theorem prerequisites

beta_at_exists · Stable closed add_left_cancel · Stable closed succ_injective · 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

67 script commands · 11 reading checkpoints · 6 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–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 hinjective
  8. L8
    intro hcomplement
  9. L9
    intro i
  10. L10
    intro j
02Fix variables and assumptionsL11–15

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

  1. L11
    intro w
  2. L12
    intro hi
  3. L13
    intro hj
  4. L14
    intro hleft
  5. L15
    intro hright
03Establish hfirstL16–20

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

  1. L16
    have hfirst : ∃ v. BetaAt(b,c,i,v)Definitions: BetaAt(b,c,i,v)Original native command in the exact edition
  2. L17
    specialize beta_at_exists b
  3. L18
    specialize beta_at_exists c
  4. L19
    specialize beta_at_exists i
  5. L20
    exact beta_at_exists
04Separate the logical casesL21–21

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

  1. L21
    cases hfirst
05Establish hsecondL22–26

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

  1. L22
    have hsecond : ∃ v. BetaAt(b,c,j,v)Definitions: BetaAt(b,c,j,v)Original native command in the exact edition
  2. L23
    specialize beta_at_exists b
  3. L24
    specialize beta_at_exists c
  4. L25
    specialize beta_at_exists j
  5. L26
    exact beta_at_exists
06Separate the logical casesL27–27

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

  1. L27
    cases hsecond
07Establish hleft_gapL28–35

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

  1. L28
    have hleft_gap : w + S x = p
  2. L29
    specialize hcomplement i
  3. L30
    specialize hcomplement x
  4. L31
    specialize hcomplement w
  5. L32
    apply hcomplement
  6. L33
    exact hi
  7. L34
    exact hfirst_witness
  8. L35
    exact hleft
08Establish hright_gapL36–43

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

  1. L36
    have hright_gap : w + S x1 = p
  2. L37
    specialize hcomplement j
  3. L38
    specialize hcomplement x1
  4. L39
    specialize hcomplement w
  5. L40
    apply hcomplement
  6. L41
    exact hj
  7. L42
    exact hsecond_witness
  8. L43
    exact hright
09Establish hequal_successorsL44–52

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

  1. L44
    have hequal_successors : S x = S x1
  2. L45
    specialize add_left_cancel w
  3. L46
    specialize add_left_cancel (S x)
  4. L47
    specialize add_left_cancel (S x1)
  5. L48
    apply add_left_cancel
  6. L49
    trans p
  7. L50
    exact hleft_gap
  8. L51
    symm
  9. L52
    exact hright_gap
10Establish hequalL53–62

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

  1. L53
    have hequal : x = x1
  2. L54
    specialize succ_injective x
  3. L55
    specialize succ_injective x1
  4. L56
    apply succ_injective
  5. L57
    exact hequal_successors
  6. L58
    rewrite <- hequal at hsecond_witness
  7. L59
    rewrite <- hequal at hsecond_witness
  8. L60
    specialize hinjective i
  9. L61
    specialize hinjective j
  10. L62
    specialize hinjective x
11Use earlier factsL63–67

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

  1. L63
    apply hinjective
  2. L64
    exact hi
  3. L65
    exact hj
  4. L66
    exact hfirst_witness
  5. L67
    exact hsecond_witness

Library-wide reading audit

Original defined command ledger · 67 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro z
  5. 0005intro d
  6. 0006intro l
  7. 0007intro hinjective
  8. 0008intro hcomplement
  9. 0009intro i
  10. 0010intro j
  11. 0011intro w
  12. 0012intro hi
  13. 0013intro hj
  14. 0014intro hleft
  15. 0015intro hright
  16. 0016have hfirst : ∃ v. BetaAt(b,c,i,v)
    Exact native replay linehave hfirst : exists v. (((exists fsri_height_complement_injective_first. fsri_height_complement_injective_first + S (v) = S ((S (i)) * (c))) /\ exists fsri_quotient_complement_injective_first. (b) = fsri_quotient_complement_injective_first * S ((S (i)) * (c)) + (v)))
  17. 0017specialize beta_at_exists b
  18. 0018specialize beta_at_exists c
  19. 0019specialize beta_at_exists i
  20. 0020exact beta_at_exists
  21. 0021cases hfirst
  22. 0022have hsecond : ∃ v. BetaAt(b,c,j,v)
    Exact native replay linehave hsecond : exists v. (((exists fsri_height_complement_injective_second. fsri_height_complement_injective_second + S (v) = S ((S (j)) * (c))) /\ exists fsri_quotient_complement_injective_second. (b) = fsri_quotient_complement_injective_second * S ((S (j)) * (c)) + (v)))
  23. 0023specialize beta_at_exists b
  24. 0024specialize beta_at_exists c
  25. 0025specialize beta_at_exists j
  26. 0026exact beta_at_exists
  27. 0027cases hsecond
  28. 0028have hleft_gap : w + S x = p
  29. 0029specialize hcomplement i
  30. 0030specialize hcomplement x
  31. 0031specialize hcomplement w
  32. 0032apply hcomplement
  33. 0033exact hi
  34. 0034exact hfirst_witness
  35. 0035exact hleft
  36. 0036have hright_gap : w + S x1 = p
  37. 0037specialize hcomplement j
  38. 0038specialize hcomplement x1
  39. 0039specialize hcomplement w
  40. 0040apply hcomplement
  41. 0041exact hj
  42. 0042exact hsecond_witness
  43. 0043exact hright
  44. 0044have hequal_successors : S x = S x1
  45. 0045specialize add_left_cancel w
  46. 0046specialize add_left_cancel (S x)
  47. 0047specialize add_left_cancel (S x1)
  48. 0048apply add_left_cancel
  49. 0049trans p
  50. 0050exact hleft_gap
  51. 0051symm
  52. 0052exact hright_gap
  53. 0053have hequal : x = x1
  54. 0054specialize succ_injective x
  55. 0055specialize succ_injective x1
  56. 0056apply succ_injective
  57. 0057exact hequal_successors
  58. 0058rewrite <- hequal at hsecond_witness
  59. 0059rewrite <- hequal at hsecond_witness
  60. 0060specialize hinjective i
  61. 0061specialize hinjective j
  62. 0062specialize hinjective x
  63. 0063apply hinjective
  64. 0064exact hi
  65. 0065exact hj
  66. 0066exact hfirst_witness
  67. 0067exact hsecond_witness