PA005Q

square_residue_witness

Stable checked-use theorem · independently closed

Existential wrapper for the generic square-residue lift.

Exact expanded PA statement

forall a z q r c s. z = a * q + r -> r * r = a * c + s -> exists w. z * z = a * w + s

Structural proof guide

Generated structural guide

Existential wrapper for the generic square-residue lift.

Use the direct prerequisites square_residue_lift as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA005P square_residue_lift

Proof neighborhood

Direct dependencies

PA005P square_residue_lift

Direct dependents

PA005R quadratic_residue_bounded_equiv

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001intro a
  2. 0002intro z
  3. 0003intro q
  4. 0004intro r
  5. 0005intro c
  6. 0006intro s
  7. 0007intro hz
  8. 0008intro hrc
  9. 0009exists (q * z + r * q) + c
  10. 0010apply square_residue_lift
  11. 0011exact hz
  12. 0012exact hrc