PF001U

pythagorean_positive_even_leg_parameters_nonzero

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

A positive even leg forces both explicitly constructed Euclidean parameters to be positive.

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 b m n. ~(b = 0) -> b = 2 * (m * n) -> (~(m = 0) /\ ~(n = 0))

Constructive proof overview

Generated structural guide

A positive even leg forces both explicitly constructed Euclidean parameters to be positive.

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

factor_nonzero_right Alpha theorem; checked-use authorized mul_zero_left Stable theorem; checked-use authorized

Direct dependents

PF001W pythagorean_half_factors_extract_parameters PF002K fermat_four_primitive_odd_even_descent

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

23 script commands · 10 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–5

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

  1. L1
    intro b
  2. L2
    intro m
  3. L3
    intro n
  4. L4
    intro hb
  5. L5
    intro heq
02Establish hproductL6–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor nonzero right.

  1. L6
    have hproduct : ~(m * n = 0)
  2. L7
    intro hzero
  3. L8
    specialize factor_nonzero_right b
  4. L9
    specialize factor_nonzero_right 2
  5. L10
    specialize factor_nonzero_right (m * n)
  6. L11
    apply factor_nonzero_right
  7. L12
    exact hb
  8. L13
    exact heq
  9. L14
    exact hzero
03Separate the logical casesL15–15

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

  1. L15
    split
04Fix variables and assumptionsL16–16

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

  1. L16
    intro hm
05Use earlier factsL17–17

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

  1. L17
    apply hproduct
06Calculate and transport equalitiesL18–18

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

  1. L18
    rewrite hm
07Use earlier factsL19–19

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

  1. L19
    apply mul_zero_left
08Fix variables and assumptionsL20–20

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

  1. L20
    intro hn
09Use earlier factsL21–21

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

  1. L21
    apply hproduct
10Calculate and transport equalitiesL22–23

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

  1. L22
    rewrite hn
  2. L23
    simp

Library-wide reading audit

Original exact command ledger · 23 lines
  1. 0001intro b
  2. 0002intro m
  3. 0003intro n
  4. 0004intro hb
  5. 0005intro heq
  6. 0006have hproduct : ~(m * n = 0)
  7. 0007intro hzero
  8. 0008specialize factor_nonzero_right b
  9. 0009specialize factor_nonzero_right 2
  10. 0010specialize factor_nonzero_right (m * n)
  11. 0011apply factor_nonzero_right
  12. 0012exact hb
  13. 0013exact heq
  14. 0014exact hzero
  15. 0015split
  16. 0016intro hm
  17. 0017apply hproduct
  18. 0018rewrite hm
  19. 0019apply mul_zero_left
  20. 0020intro hn
  21. 0021apply hproduct
  22. 0022rewrite hn
  23. 0023simp