FS004A · theorem body

four_square_prime_half_square_residues_injective

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

Squaring is constructively injective modulo every odd prime on its complete inclusive half range.

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. ∀ h. ∀ x. ∀ y. p = 2 · h + 1 → Prime(p) → Le(x,h) → Le(y,h) → ModEq(p,x · x,y · y) → x = y

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

PD0001 Le PD0004 Prime PD0008 ModEq

In local proof propositions

PD0001 Le
Exact expanded first-order statement
forall p h x y. p = 2 * h + 1 -> ((~(p = 1) /\ forall frm_prime_left_fsri_prime frm_prime_right_fsri_prime. p = frm_prime_left_fsri_prime * frm_prime_right_fsri_prime -> frm_prime_left_fsri_prime = 1 \/ frm_prime_right_fsri_prime = 1)) -> (exists fsri_gap_half_x. fsri_gap_half_x + (x) = (h)) -> (exists fsri_gap_half_y. fsri_gap_half_y + (y) = (h)) -> (exists fsri_left_half_equal fsri_right_half_equal. (x * x) + (p) * fsri_left_half_equal = (y * y) + (p) * fsri_right_half_equal) -> x = y

Proof neighborhood

Direct theorem prerequisites

le_total · Stable closed add_comm · Stable closed mod_eq_symm · Stable closed FS0049 four_square_ordered_half_square_injective

Direct theorem dependents

FS004E four_square_half_square_residue_prefix_injective

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

51 script commands · 11 reading checkpoints · 1 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 ordered half square injective
01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro hodd
  6. L6
    intro hprime
  7. L7
    intro hx
  8. L8
    intro hy
  9. L9
    intro hmod
02Establish horderL10–13

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

  1. L10
    have horder : Le(x,y) ∨ Le(y,x)Definitions: Le(x,y)Le(y,x)Original native command in the exact edition
  2. L11
    specialize le_total x
  3. L12
    specialize le_total y
  4. L13
    exact le_total
03Separate the logical casesL14–15

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

  1. L14
    cases horder
  2. L15
    cases horder_left
04Use earlier factsL16–25

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

  1. L16
    specialize four_square_ordered_half_square_injective p
  2. L17
    specialize four_square_ordered_half_square_injective h
  3. L18
    specialize four_square_ordered_half_square_injective x
  4. L19
    specialize four_square_ordered_half_square_injective y
  5. L20
    specialize four_square_ordered_half_square_injective x1
  6. L21
    apply four_square_ordered_half_square_injective
  7. L22
    exact hodd
  8. L23
    exact hprime
  9. L24
    exact hx
  10. L25
    exact hy
05Calculate and transport equalitiesL26–27

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

  1. L26
    trans x1 + x
  2. L27
    symm
06Use earlier factsL28–30

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

  1. L28
    exact horder_left_witness
  2. L29
    apply add_comm
  3. L30
    exact hmod
07Separate the logical casesL31–31

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

  1. L31
    cases horder_right
08Calculate and transport equalitiesL32–32

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

  1. L32
    symm
09Use earlier factsL33–42

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

  1. L33
    specialize four_square_ordered_half_square_injective p
  2. L34
    specialize four_square_ordered_half_square_injective h
  3. L35
    specialize four_square_ordered_half_square_injective y
  4. L36
    specialize four_square_ordered_half_square_injective x
  5. L37
    specialize four_square_ordered_half_square_injective x1
  6. L38
    apply four_square_ordered_half_square_injective
  7. L39
    exact hodd
  8. L40
    exact hprime
  9. L41
    exact hy
  10. L42
    exact hx
10Calculate and transport equalitiesL43–44

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

  1. L43
    trans x1 + y
  2. L44
    symm
11Use earlier factsL45–51

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

  1. L45
    exact horder_right_witness
  2. L46
    apply add_comm
  3. L47
    specialize mod_eq_symm p
  4. L48
    specialize mod_eq_symm (x * x)
  5. L49
    specialize mod_eq_symm (y * y)
  6. L50
    apply mod_eq_symm
  7. L51
    exact hmod

Library-wide reading audit

Original defined command ledger · 51 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro x
  4. 0004intro y
  5. 0005intro hodd
  6. 0006intro hprime
  7. 0007intro hx
  8. 0008intro hy
  9. 0009intro hmod
  10. 0010have horder : Le(x,y) ∨ Le(y,x)
    Exact native replay linehave horder : (exists fsri_gap_half_order_xy. fsri_gap_half_order_xy + (x) = (y)) \/ (exists fsri_gap_half_order_yx. fsri_gap_half_order_yx + (y) = (x))
  11. 0011specialize le_total x
  12. 0012specialize le_total y
  13. 0013exact le_total
  14. 0014cases horder
  15. 0015cases horder_left
  16. 0016specialize four_square_ordered_half_square_injective p
  17. 0017specialize four_square_ordered_half_square_injective h
  18. 0018specialize four_square_ordered_half_square_injective x
  19. 0019specialize four_square_ordered_half_square_injective y
  20. 0020specialize four_square_ordered_half_square_injective x1
  21. 0021apply four_square_ordered_half_square_injective
  22. 0022exact hodd
  23. 0023exact hprime
  24. 0024exact hx
  25. 0025exact hy
  26. 0026trans x1 + x
  27. 0027symm
  28. 0028exact horder_left_witness
  29. 0029apply add_comm
  30. 0030exact hmod
  31. 0031cases horder_right
  32. 0032symm
  33. 0033specialize four_square_ordered_half_square_injective p
  34. 0034specialize four_square_ordered_half_square_injective h
  35. 0035specialize four_square_ordered_half_square_injective y
  36. 0036specialize four_square_ordered_half_square_injective x
  37. 0037specialize four_square_ordered_half_square_injective x1
  38. 0038apply four_square_ordered_half_square_injective
  39. 0039exact hodd
  40. 0040exact hprime
  41. 0041exact hy
  42. 0042exact hx
  43. 0043trans x1 + y
  44. 0044symm
  45. 0045exact horder_right_witness
  46. 0046apply add_comm
  47. 0047specialize mod_eq_symm p
  48. 0048specialize mod_eq_symm (x * x)
  49. 0049specialize mod_eq_symm (y * y)
  50. 0050apply mod_eq_symm
  51. 0051exact hmod