PF0020

pythagorean_ordered_gap_positive

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

Strictly ordered parameters with a positive smaller parameter have a positive larger parameter and a positive exact square gap.

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 a m n. ~(n = 0) -> (exists gap. gap + S n = m) -> m * m = n * n + a -> (~(m = 0) /\ ~(a = 0))

Constructive proof overview

Generated structural guide

Strictly ordered parameters with a positive smaller parameter have a positive larger parameter and a positive exact square gap.

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

lt_to_le Stable theorem; checked-use authorized le_zero Stable theorem; checked-use authorized PF001B square_eq_injective lt_irrefl_expanded Stable theorem; checked-use authorized

Direct dependents

PF0021 pythagorean_euclidean_parameters_positive_constructor

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

24 script commands · 9 reading checkpoints · 2 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)
square eq injective
01Fix variables and assumptionsL1–6

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

  1. L1
    intro a
  2. L2
    intro m
  3. L3
    intro n
  4. L4
    intro hn
  5. L5
    intro horder
  6. L6
    intro hgap
02Separate the logical casesL7–7

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

  1. L7
    split
03Fix variables and assumptionsL8–8

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

  1. L8
    intro hm
04Use earlier factsL9–10

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

  1. L9
    apply hn
  2. L10
    apply le_zero
05Calculate and transport equalitiesL11–11

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

  1. L11
    rewrite <- hm
06Use earlier factsL12–13

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

  1. L12
    apply lt_to_le
  2. L13
    exact horder
07Fix variables and assumptionsL14–14

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

  1. L14
    intro ha
08Establish hsquareL15–18

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

  1. L15
    have hsquare : m * m = n * n
  2. L16
    trans n * n + a
  3. L17
    exact hgap
  4. L18
    simp [ha]
09Establish hequalL19–24

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

  1. L19
    have hequal : m = n
  2. L20
    apply square_eq_injective
  3. L21
    exact hsquare
  4. L22
    rewrite hequal at horder
  5. L23
    apply lt_irrefl_expanded
  6. L24
    exact horder

Library-wide reading audit

Original exact command ledger · 24 lines
  1. 0001intro a
  2. 0002intro m
  3. 0003intro n
  4. 0004intro hn
  5. 0005intro horder
  6. 0006intro hgap
  7. 0007split
  8. 0008intro hm
  9. 0009apply hn
  10. 0010apply le_zero
  11. 0011rewrite <- hm
  12. 0012apply lt_to_le
  13. 0013exact horder
  14. 0014intro ha
  15. 0015have hsquare : m * m = n * n
  16. 0016trans n * n + a
  17. 0017exact hgap
  18. 0018simp [ha]
  19. 0019have hequal : m = n
  20. 0020apply square_eq_injective
  21. 0021exact hsquare
  22. 0022rewrite hequal at horder
  23. 0023apply lt_irrefl_expanded
  24. 0024exact horder