FS000S · theorem body

four_square_branch_even_represented_strict_step

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

Every represented nonzero even prime multiplier unconditionally descends to its nonzero strictly smaller represented half.

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

∀ p. ∀ k. ∀ h. ¬k = 0 → k = 2 · h → (∃ x. ∃ y. ∃ z. ∃ n. p · k = x · x + y · y + z · z + n · n) → ∃ x. ¬x = 0 ∧ (Lt(x,k) ∧ (∃ y. ∃ z. ∃ n. ∃ m. p · x = y · y + z · z + n · n + m · m))

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 p k h. ~(k = 0) -> k = 2 * h -> (exists fsl_a_fsbr_multiple fsl_b_fsbr_multiple fsl_c_fsbr_multiple fsl_d_fsbr_multiple. (p * k) = fsl_a_fsbr_multiple * fsl_a_fsbr_multiple + fsl_b_fsbr_multiple * fsl_b_fsbr_multiple + fsl_c_fsbr_multiple * fsl_c_fsbr_multiple + fsl_d_fsbr_multiple * fsl_d_fsbr_multiple) -> (exists r. (~(r = 0) /\ ((exists gap. gap + S r = k) /\ (exists fsl_a_fsbr_smaller fsl_b_fsbr_smaller fsl_c_fsbr_smaller fsl_d_fsbr_smaller. (p * r) = fsl_a_fsbr_smaller * fsl_a_fsbr_smaller + fsl_b_fsbr_smaller * fsl_b_fsbr_smaller + fsl_c_fsbr_smaller * fsl_c_fsbr_smaller + fsl_d_fsbr_smaller * fsl_d_fsbr_smaller))))

Proof neighborhood

Direct theorem prerequisites

FS000Q four_square_branch_nonzero_even_half FS000R four_square_branch_positive_half_strict mul_double_right · Stable closed mul_comm · Stable closed FS0041 four_square_parity_represented_double_halving

Direct theorem dependents

FS000U four_square_bounded_strict_descent_from_odd_signed_quaternion

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

31 script commands · 14 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.

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 (3)
four square branch nonzero even halffour square branch positive half strictfour square parity represented double halving
01Fix variables and assumptionsL1–6

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

  1. L1
    intro p
  2. L2
    intro k
  3. L3
    intro h
  4. L4
    intro hnonzero
  5. L5
    intro hdouble
  6. L6
    intro hrepresented
02Establish hhalfL7–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square branch nonzero even half.

  1. L7
    have hhalf : ~(h = 0)
  2. L8
    intro hzero
  3. L9
    specialize four_square_branch_nonzero_even_half k
  4. L10
    specialize four_square_branch_nonzero_even_half h
  5. L11
    apply four_square_branch_nonzero_even_half
  6. L12
    exact hnonzero
  7. L13
    exact hdouble
  8. L14
    exact hzero
03Construct an explicit witnessL15–15

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

  1. L15
    exists h
04Separate the logical casesL16–16

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

  1. L16
    split
05Use earlier factsL17–17

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

  1. L17
    exact hhalf
06Separate the logical casesL18–18

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

  1. L18
    split
07Calculate and transport equalitiesL19–19

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

  1. L19
    rewrite hdouble
08Use earlier factsL20–21

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

  1. L20
    apply four_square_branch_positive_half_strict
  2. L21
    exact hhalf
09Calculate and transport equalitiesL22–22

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

  1. L22
    rewrite hdouble at hrepresented
10Use earlier factsL23–24

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

  1. L23
    specialize mul_double_right p
  2. L24
    specialize mul_double_right h
11Calculate and transport equalitiesL25–25

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

  1. L25
    rewrite mul_double_right at hrepresented
12Use earlier factsL26–27

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

  1. L26
    specialize mul_comm 2
  2. L27
    specialize mul_comm (p * h)
13Calculate and transport equalitiesL28–28

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

  1. L28
    rewrite mul_comm at hrepresented
14Use earlier factsL29–31

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

  1. L29
    specialize four_square_parity_represented_double_halving (p * h)
  2. L30
    apply four_square_parity_represented_double_halving
  3. L31
    exact hrepresented

Library-wide reading audit

Original defined command ledger · 31 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro h
  4. 0004intro hnonzero
  5. 0005intro hdouble
  6. 0006intro hrepresented
  7. 0007have hhalf : ~(h = 0)
  8. 0008intro hzero
  9. 0009specialize four_square_branch_nonzero_even_half k
  10. 0010specialize four_square_branch_nonzero_even_half h
  11. 0011apply four_square_branch_nonzero_even_half
  12. 0012exact hnonzero
  13. 0013exact hdouble
  14. 0014exact hzero
  15. 0015exists h
  16. 0016split
  17. 0017exact hhalf
  18. 0018split
  19. 0019rewrite hdouble
  20. 0020apply four_square_branch_positive_half_strict
  21. 0021exact hhalf
  22. 0022rewrite hdouble at hrepresented
  23. 0023specialize mul_double_right p
  24. 0024specialize mul_double_right h
  25. 0025rewrite mul_double_right at hrepresented
  26. 0026specialize mul_comm 2
  27. 0027specialize mul_comm (p * h)
  28. 0028rewrite mul_comm at hrepresented
  29. 0029specialize four_square_parity_represented_double_halving (p * h)
  30. 0030apply four_square_parity_represented_double_halving
  31. 0031exact hrepresented