FS000R

four_square_branch_positive_half_strict

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

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

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. ~(h = 0) -> exists gap. gap + S h = 2 * h

Constructive proof overview

Generated structural guide

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

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

mul_lt_mul_succ_left_nonzero Stable theorem; checked-use authorized mul_one Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized

Direct dependents

FS000S four_square_branch_even_represented_strict_step

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

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.

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 : exists gap. gap + S (h * 1) = h * S 1
  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 exact command ledger · 16 lines
  1. 0001intro h
  2. 0002intro hnonzero
  3. 0003have 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