EL0002

euclidean_log_strict_half_cancel

Strict comparison of two exact doubles constructively cancels the factor two.

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

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

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

Definition DAG

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

Actual proof prerequisites

le_total · checked external prerequisitele_eq_or_lt · checked external prerequisiteeuclidean_log_double_monotonelt_not_le · checked external prerequisitelt_irrefl_expanded · checked external prerequisite
Original expanded first-order statement 
forall t p. (exists gap. gap + S (t + t) = p + p) -> exists gap. gap + S t = p

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

28 script commands · 9 reading checkpoints · 1 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 double monotone
01Fix variables and assumptionsL1–3

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

  1. L1
    intro t
  2. L2
    intro p
  3. L3
    intro hstrict
02Use earlier factsL4–5

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

  1. L4
    specialize le_total p
  2. L5
    specialize le_total t
03Separate the logical casesL6–7

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L6
    cases le_total
  2. L7
    exfalso
04Use earlier factsL8–17

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

  1. L8
    specialize lt_not_le (t + t)
  2. L9
    specialize lt_not_le (p + p)
  3. L10
    apply lt_not_le
  4. L11
    exact hstrict
  5. L12
    specialize euclidean_log_double_monotone p
  6. L13
    specialize euclidean_log_double_monotone t
  7. L14
    apply euclidean_log_double_monotone
  8. L15
    exact le_total_left
  9. L16
    specialize le_eq_or_lt t
  10. L17
    specialize le_eq_or_lt p
05Establish hcasesL18–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L18
    have hcases : t = p \/ exists gap. gap + S t = p
  2. L19
    apply le_eq_or_lt
  3. L20
    exact le_total_right
06Separate the logical casesL21–22

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L21
    cases hcases
  2. L22
    exfalso
07Use earlier factsL23–24

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

  1. L23
    specialize lt_irrefl_expanded (p + p)
  2. L24
    apply lt_irrefl_expanded
08Calculate and transport equalitiesL25–26

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L25
    rewrite hcases_left at hstrict
  2. L26
    rewrite hcases_left at hstrict
09Use earlier factsL27–28

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

  1. L27
    exact hstrict
  2. L28
    exact hcases_right

Library-wide reading audit

Original defined command ledger · 28 lines
  1. 0001intro t
  2. 0002intro p
  3. 0003intro hstrict
  4. 0004specialize le_total p
  5. 0005specialize le_total t
  6. 0006cases le_total
  7. 0007exfalso
  8. 0008specialize lt_not_le (t + t)
  9. 0009specialize lt_not_le (p + p)
  10. 0010apply lt_not_le
  11. 0011exact hstrict
  12. 0012specialize euclidean_log_double_monotone p
  13. 0013specialize euclidean_log_double_monotone t
  14. 0014apply euclidean_log_double_monotone
  15. 0015exact le_total_left
  16. 0016specialize le_eq_or_lt t
  17. 0017specialize le_eq_or_lt p
  18. 0018have hcases : t = p \/ exists gap. gap + S t = p
  19. 0019apply le_eq_or_lt
  20. 0020exact le_total_right
  21. 0021cases hcases
  22. 0022exfalso
  23. 0023specialize lt_irrefl_expanded (p + p)
  24. 0024apply lt_irrefl_expanded
  25. 0025rewrite hcases_left at hstrict
  26. 0026rewrite hcases_left at hstrict
  27. 0027exact hstrict
  28. 0028exact hcases_right