FS004A

four_square_prime_half_square_residues_injective

Alpha v34 independently verified · alpha_closed; checked-use authorized; 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.

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 51 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

Proof neighborhood

Direct dependencies

le_total Stable theorem; checked-use authorized add_comm Stable theorem; checked-use authorized mod_eq_symm Stable theorem; checked-use authorized FS0049 four_square_ordered_half_square_injective

Direct dependents

FS004E four_square_half_square_residue_prefix_injective

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

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.

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