EL0002

euclidean_log_strict_half_cancel

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 5 declared prerequisites and contains 28 exact native proof lines.

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

Proof neighborhood

Direct dependencies

le_total Stable theorem; checked-use authorized le_eq_or_lt Stable theorem; checked-use authorized EL0001 euclidean_log_double_monotone lt_not_le Stable theorem; checked-use authorized lt_irrefl_expanded Stable theorem; checked-use authorized

Direct dependents

EL0003 euclidean_log_halving_power_drop

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

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.

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

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