FS001U

four_square_descent_odd_centered_magnitude_half_bound

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

For an odd modulus 2h+1, the constructive centered bound m+m≤2h+1 implies the sharp half-range bound m≤h.

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 h m. (exists gap. gap + (m + m) = 2 * h + 1) -> exists gap. gap + m = h

Constructive proof overview

Generated structural guide

For an odd modulus 2h+1, the constructive centered bound m+m≤2h+1 implies the sharp half-range bound m≤h.

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

Historical empty-context replay experiment only; that experiment persisted no certificate and granted no release authority. Current checked use follows separately sealed, independently verified proof bundles; there is no Stable promotion.

Proof neighborhood

Direct dependencies

le_eq_or_lt Stable theorem; checked-use authorized even_odd_exclusive_pointwise Stable theorem; checked-use authorized two_mul_eq_add_self Alpha theorem; checked-use authorized le_of_succ_le_succ Stable theorem; checked-use authorized mul_le_cancel_left_nonzero Alpha theorem; checked-use authorized succ_ne_zero Stable theorem; checked-use authorized

Direct dependents

FS001Y four_square_descent_odd_centered_norm_strict

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

42 script commands · 16 reading checkpoints · 4 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–3

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

  1. L1
    intro h
  2. L2
    intro m
  3. L3
    intro hbound
02Use earlier factsL4–5

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

  1. L4
    specialize le_eq_or_lt (m + m)
  2. L5
    specialize le_eq_or_lt (2 * h + 1)
03Establish hsplitL6–8

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

  1. L6
    have hsplit : m + m = 2 * h + 1 \/ (exists gap. gap + S (m + m) = 2 * h + 1)
  2. L7
    apply le_eq_or_lt
  3. L8
    exact hbound
04Separate the logical casesL9–10

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

  1. L9
    cases hsplit
  2. L10
    exfalso
05Use earlier factsL11–14

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

  1. L11
    specialize even_odd_exclusive_pointwise (m + m)
  2. L12
    specialize even_odd_exclusive_pointwise m
  3. L13
    specialize even_odd_exclusive_pointwise h
  4. L14
    apply even_odd_exclusive_pointwise
06Calculate and transport equalitiesL15–15

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

  1. L15
    symm
07Use earlier factsL16–17

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

  1. L16
    apply two_mul_eq_add_self
  2. L17
    exact hsplit_left
08Establish honeL18–20

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

  1. L18
    have hone : 2 * h + 1 = S (2 * h)
  2. L19
    simp
  3. L20
    rewrite hone at hsplit_right
09Establish hdoubleL21–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.

  1. L21
    have hdouble : exists gap. gap + (m + m) = 2 * h
  2. L22
    specialize le_of_succ_le_succ (m + m)
  3. L23
    specialize le_of_succ_le_succ (2 * h)
  4. L24
    apply le_of_succ_le_succ
  5. L25
    exact hsplit_right
10Establish hscaledL26–26

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

  1. L26
    have hscaled : exists gap. gap + 2 * m = 2 * h
11Separate the logical casesL27–27

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

  1. L27
    cases hdouble
12Construct an explicit witnessL28–28

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

  1. L28
    exists x
13Calculate and transport equalitiesL29–31

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

  1. L29
    trans x + (m + m)
  2. L30
    congr
  3. L31
    refl
14Use earlier factsL32–37

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

  1. L32
    apply two_mul_eq_add_self
  2. L33
    exact hdouble_witness
  3. L34
    specialize mul_le_cancel_left_nonzero 2
  4. L35
    specialize mul_le_cancel_left_nonzero m
  5. L36
    specialize mul_le_cancel_left_nonzero h
  6. L37
    apply mul_le_cancel_left_nonzero
15Fix variables and assumptionsL38–38

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

  1. L38
    intro hzero
16Use earlier factsL39–42

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

  1. L39
    specialize succ_ne_zero 1
  2. L40
    apply succ_ne_zero
  3. L41
    exact hzero
  4. L42
    exact hscaled

Library-wide reading audit

Original exact command ledger · 42 lines
  1. 0001intro h
  2. 0002intro m
  3. 0003intro hbound
  4. 0004specialize le_eq_or_lt (m + m)
  5. 0005specialize le_eq_or_lt (2 * h + 1)
  6. 0006have hsplit : m + m = 2 * h + 1 \/ (exists gap. gap + S (m + m) = 2 * h + 1)
  7. 0007apply le_eq_or_lt
  8. 0008exact hbound
  9. 0009cases hsplit
  10. 0010exfalso
  11. 0011specialize even_odd_exclusive_pointwise (m + m)
  12. 0012specialize even_odd_exclusive_pointwise m
  13. 0013specialize even_odd_exclusive_pointwise h
  14. 0014apply even_odd_exclusive_pointwise
  15. 0015symm
  16. 0016apply two_mul_eq_add_self
  17. 0017exact hsplit_left
  18. 0018have hone : 2 * h + 1 = S (2 * h)
  19. 0019simp
  20. 0020rewrite hone at hsplit_right
  21. 0021have hdouble : exists gap. gap + (m + m) = 2 * h
  22. 0022specialize le_of_succ_le_succ (m + m)
  23. 0023specialize le_of_succ_le_succ (2 * h)
  24. 0024apply le_of_succ_le_succ
  25. 0025exact hsplit_right
  26. 0026have hscaled : exists gap. gap + 2 * m = 2 * h
  27. 0027cases hdouble
  28. 0028exists x
  29. 0029trans x + (m + m)
  30. 0030congr
  31. 0031refl
  32. 0032apply two_mul_eq_add_self
  33. 0033exact hdouble_witness
  34. 0034specialize mul_le_cancel_left_nonzero 2
  35. 0035specialize mul_le_cancel_left_nonzero m
  36. 0036specialize mul_le_cancel_left_nonzero h
  37. 0037apply mul_le_cancel_left_nonzero
  38. 0038intro hzero
  39. 0039specialize succ_ne_zero 1
  40. 0040apply succ_ne_zero
  41. 0041exact hzero
  42. 0042exact hscaled