EL0003

euclidean_log_halving_power_drop

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

A genuine two-step strict halving below twice a power lies below that power.

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 b t p. (exists gap. gap + S (t + t) = b) -> (exists gap. gap + S b = p + p) -> exists gap. gap + S t = p

Constructive proof overview

Generated structural guide

A genuine two-step strict halving below twice a power lies below that power.

The unchanged tactic script uses 2 declared prerequisites and contains 14 exact native proof lines.

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

Proof neighborhood

Direct dependencies

lt_trans Stable theorem; checked-use authorized EL0002 euclidean_log_strict_half_cancel

Direct dependents

EL000C euclidean_log_trace_below_power

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

14 script commands · 2 reading checkpoints · 0 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 (1)
euclidean log strict half cancel
01Fix variables and assumptionsL1–5

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

  1. L1
    intro b
  2. L2
    intro t
  3. L3
    intro p
  4. L4
    intro hhalf
  5. L5
    intro hupper
02Use earlier factsL6–14

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

  1. L6
    specialize euclidean_log_strict_half_cancel t
  2. L7
    specialize euclidean_log_strict_half_cancel p
  3. L8
    apply euclidean_log_strict_half_cancel
  4. L9
    specialize lt_trans (t + t)
  5. L10
    specialize lt_trans b
  6. L11
    specialize lt_trans (p + p)
  7. L12
    apply lt_trans
  8. L13
    exact hhalf
  9. L14
    exact hupper

Library-wide reading audit

Original exact command ledger · 14 lines
  1. 0001intro b
  2. 0002intro t
  3. 0003intro p
  4. 0004intro hhalf
  5. 0005intro hupper
  6. 0006specialize euclidean_log_strict_half_cancel t
  7. 0007specialize euclidean_log_strict_half_cancel p
  8. 0008apply euclidean_log_strict_half_cancel
  9. 0009specialize lt_trans (t + t)
  10. 0010specialize lt_trans b
  11. 0011specialize lt_trans (p + p)
  12. 0012apply lt_trans
  13. 0013exact hhalf
  14. 0014exact hupper

Separate complete second-wave branches: Full T13 proof · Alpha v27.