PF0008

pythagorean_square_gap_from_order

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Every witnessed natural parameter inequality n≤m produces the exact subtraction-free square-difference witness m²=n²+d.

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 m n. (exists gap. gap + n = m) -> exists d. m * m = n * n + d

Constructive proof overview

Generated structural guide

Every witnessed natural parameter inequality n≤m produces the exact subtraction-free square-difference witness m²=n²+d.

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

mul_le_mul Alpha theorem; checked-use authorized add_comm Stable theorem; checked-use authorized

Direct dependents

PF0009 pythagorean_euclidean_from_order PF000U pythagorean_primitive_euclidean_from_order

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

13 script commands · 6 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.

01Fix variables and assumptionsL1–3

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

  1. L1
    intro m
  2. L2
    intro n
  3. L3
    intro hbound
02Establish hsquareL4–7

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

  1. L4
    have hsquare : exists gap. gap + n * n = m * m
  2. L5
    apply mul_le_mul
  3. L6
    exact hbound
  4. L7
    exact hbound
03Separate the logical casesL8–8

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

  1. L8
    cases hsquare
04Construct an explicit witnessL9–9

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

  1. L9
    exists x
05Calculate and transport equalitiesL10–11

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

  1. L10
    trans x + n * n
  2. L11
    symm
06Use earlier factsL12–13

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

  1. L12
    exact hsquare_witness
  2. L13
    apply add_comm

Library-wide reading audit

Original exact command ledger · 13 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro hbound
  4. 0004have hsquare : exists gap. gap + n * n = m * m
  5. 0005apply mul_le_mul
  6. 0006exact hbound
  7. 0007exact hbound
  8. 0008cases hsquare
  9. 0009exists x
  10. 0010trans x + n * n
  11. 0011symm
  12. 0012exact hsquare_witness
  13. 0013apply add_comm