FS000S

four_square_branch_even_represented_strict_step

Alpha v34 independently verified · alpha_closed; checked-use authorized; 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.

Exact expanded first-order arithmetic 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))))

Constructive proof overview

Generated structural guide

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

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

FS000Q four_square_branch_nonzero_even_half FS000R four_square_branch_positive_half_strict mul_double_right Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized FS0041 four_square_parity_represented_double_halving

Direct dependents

FS000U four_square_bounded_strict_descent_from_odd_signed_quaternion

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

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.

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 exact 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