FS000R · theorem body

four_square_branch_positive_half_strict

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

Every positive natural half is constructively strictly smaller than its doubled value.

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. ¬h = 0 → Lt(h,2 · 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

PD0002 Lt

In local proof propositions

PD0002 Lt
Exact expanded first-order statement
forall h. ~(h = 0) -> exists gap. gap + S h = 2 * h

Proof neighborhood

Direct theorem prerequisites

mul_lt_mul_succ_left_nonzero · Stable closed mul_one · Stable closed mul_comm · Stable closed

Direct theorem dependents

FS000S four_square_branch_even_represented_strict_step

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

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

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

  1. L1
    intro h
  2. L2
    intro hnonzero
02Establish hboundL3–9

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul lt mul succ left nonzero.

  1. L3
    have hbound : Lt(h · 1,h · 2)Definitions: Lt(h · 1,h · 2)Original native command in the exact edition
  2. L4
    specialize mul_lt_mul_succ_left_nonzero h
  3. L5
    specialize mul_lt_mul_succ_left_nonzero 1
  4. L6
    apply mul_lt_mul_succ_left_nonzero
  5. L7
    exact hnonzero
  6. L8
    specialize mul_one h
  7. L9
    rewrite mul_one at hbound
03Establish htwoL10–16

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

  1. L10
    have htwo : S 1 = 2
  2. L11
    norm_num
  3. L12
    rewrite htwo at hbound
  4. L13
    specialize mul_comm h
  5. L14
    specialize mul_comm 2
  6. L15
    rewrite mul_comm at hbound
  7. L16
    exact hbound

Library-wide reading audit

Original defined command ledger · 16 lines
  1. 0001intro h
  2. 0002intro hnonzero
  3. 0003have hbound : Lt(h · 1,h · 2)
    Exact native replay linehave hbound : exists gap. gap + S (h * 1) = h * S 1
  4. 0004specialize mul_lt_mul_succ_left_nonzero h
  5. 0005specialize mul_lt_mul_succ_left_nonzero 1
  6. 0006apply mul_lt_mul_succ_left_nonzero
  7. 0007exact hnonzero
  8. 0008specialize mul_one h
  9. 0009rewrite mul_one at hbound
  10. 0010have htwo : S 1 = 2
  11. 0011norm_num
  12. 0012rewrite htwo at hbound
  13. 0013specialize mul_comm h
  14. 0014specialize mul_comm 2
  15. 0015rewrite mul_comm at hbound
  16. 0016exact hbound