FS001U · theorem body

four_square_descent_odd_centered_magnitude_half_bound

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

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

historical independently replay-verified empty-context experiment; the experiment itself persisted no certificate and granted no release authority; current checked use follows separately sealed proof bundles; no Stable promotion.

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

∀ h. ∀ m. Le(m + m,2 · h + 1) → Le(m,h)

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

PD0001 Le

In local proof propositions

PD0001 Le PD0002 Lt
Exact expanded first-order statement
forall h m. (exists gap. gap + (m + m) = 2 * h + 1) -> exists gap. gap + m = h

Proof neighborhood

Direct theorem prerequisites

le_eq_or_lt · Stable closed even_odd_exclusive_pointwise · Stable closed two_mul_eq_add_self · Alpha closed le_of_succ_le_succ · Stable closed mul_le_cancel_left_nonzero · Alpha closed succ_ne_zero · Stable closed

Direct theorem dependents

FS001Y four_square_descent_odd_centered_norm_strict

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 ∨ Lt(m + m,2 · h + 1)Definitions: Lt(m + m,2 · h + 1)Original native command in the exact edition
  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 : Le(m + m,2 · h)Definitions: Le(m + m,2 · h)Original native command in the exact edition
  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 : Le(2 · m,2 · h)Definitions: Le(2 · m,2 · h)Original native command in the exact edition
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 defined 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 ∨ Lt(m + m,2 · h + 1)
    Exact native replay linehave 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 : Le(m + m,2 · h)
    Exact native replay linehave 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 : Le(2 · m,2 · h)
    Exact native replay linehave 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