PF0020 · theorem body

pythagorean_ordered_gap_positive

Alpha v34 checked-use · independently kernel and Lean verified; 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.

Statement with defined notation

∀ a. ∀ m. ∀ n. ¬n = 0 → Lt(n,m) → m · m = n · n + a → ¬m = 0 ∧ ¬a = 0

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

PD0002 Lt

In local proof propositions

none
Exact expanded first-order statement
forall a m n. ~(n = 0) -> (exists gap. gap + S n = m) -> m * m = n * n + a -> (~(m = 0) /\ ~(a = 0))

Proof neighborhood

Direct theorem prerequisites

lt_to_le · Stable closed le_zero · Stable closed PF001B square_eq_injective lt_irrefl_expanded · Stable closed

Direct theorem dependents

PF0021 pythagorean_euclidean_parameters_positive_constructor

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

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.

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)
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 defined 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