EL0003

euclidean_log_halving_power_drop

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

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

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.

The exact G101 milestone is fully proved, including the stronger checked bound k≤2·BitLen(b), a real beta-coded execution, and its actual terminal gcd. The independent T13 determinant/rank/integer-span substrate is now closed in the separate Alpha-v27 integer-linear-algebra branch. Full T13 proof · Alpha v27

Exact theorem in conservative defined notation

∀ b. ∀ t. ∀ p. EuclideanHalving(b,t) → Lt(b,p + p) → Lt(t,p)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

EuclideanHalving(b,r) · 1Lt(a,b) · 2

Actual proof prerequisites

lt_trans · checked external prerequisiteeuclidean_log_strict_half_cancel
Original expanded first-order 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

Complete unchanged native tactic proof

All 14 lines are the exact independently kernel-checked original script.

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.

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

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 defined 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