EL0011

lte_prime_divides_correction

The doubled second-order remainder is divisible by an odd prime, so its actual correction is divisible too.

Alpha v34 checked-use · first admitted v29 · 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.

All displayed hypotheses are required. Powers and positive differences are actual existential outputs. The proof constructs second-order correction identities and iterates the prime step; no binomial expansion or LTE oracle is assumed. The 2-adic variants remain separate open targets.

Exact theorem in conservative defined notation

∀ p. ∀ d. ∀ r. ∀ T. ∀ C. ∀ H. ¬p = 1 ∧ (∀ x. ∀ y. p = x · y → x = 1 ∨ y = 1) → ¬p = 2 → Dvd(p,d) → 2 · C = p · r · T + d · H → Dvd(p,C)

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

Definition DAG

Dvd(d,n) · 2

Actual proof prerequisites

gauss_coprime_cancel · checked external prerequisiteprime_not_divides_coprime · checked external prerequisitelte_prime_nondivisor_twomultiple_add · checked external prerequisitemul_assoc · checked external prerequisite
Original expanded first-order statement 
forall p d r T C H. (~((p) = 1) /\ forall pvs_left_correction_prime pvs_right_correction_prime. (p) = pvs_left_correction_prime * pvs_right_correction_prime -> pvs_left_correction_prime = 1 \/ pvs_right_correction_prime = 1) -> ~(p = 2) -> (exists olte_factor_correction_difference. (d) = (p) * olte_factor_correction_difference) -> 2 * C = (p * r) * T + d * H -> (exists olte_factor_correction_result. (C) = (p) * olte_factor_correction_result)

Complete tactic proof in conservative notation

All 35 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

35 script commands · 12 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)
lte prime nondivisor two
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro d
  3. L3
    intro r
  4. L4
    intro T
  5. L5
    intro C
  6. L6
    intro H
  7. L7
    intro hp
  8. L8
    intro hne
  9. L9
    intro hd
  10. L10
    intro hC
02Use earlier factsL11–18

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

  1. L11
    specialize gauss_coprime_cancel (p)
  2. L12
    specialize gauss_coprime_cancel (2)
  3. L13
    specialize gauss_coprime_cancel (C)
  4. L14
    apply gauss_coprime_cancel
  5. L15
    specialize prime_not_divides_coprime (p)
  6. L16
    specialize prime_not_divides_coprime (2)
  7. L17
    apply prime_not_divides_coprime
  8. L18
    exact hp
03Fix variables and assumptionsL19–19

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

  1. L19
    intro hdiv
04Use earlier factsL20–24

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

  1. L20
    specialize lte_prime_nondivisor_two (p)
  2. L21
    apply lte_prime_nondivisor_two
  3. L22
    exact hp
  4. L23
    exact hne
  5. L24
    exact hdiv
05Calculate and transport equalitiesL25–25

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

  1. L25
    rewrite hC
06Use earlier factsL26–29

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

  1. L26
    specialize multiple_add (p)
  2. L27
    specialize multiple_add ((p * r) * T)
  3. L28
    specialize multiple_add (d * H)
  4. L29
    apply multiple_add
07Construct an explicit witnessL30–30

Supply the displayed value, then prove that it has the required property.

  1. L30
    exists r * T
08Use earlier factsL31–31

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

  1. L31
    apply mul_assoc
09Separate the logical casesL32–32

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

  1. L32
    cases hd
10Construct an explicit witnessL33–33

Supply the displayed value, then prove that it has the required property.

  1. L33
    exists x * H
11Calculate and transport equalitiesL34–34

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

  1. L34
    rewrite hd_witness
12Use earlier factsL35–35

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

  1. L35
    apply mul_assoc

Library-wide reading audit

Original defined command ledger · 35 lines
  1. 0001intro p
  2. 0002intro d
  3. 0003intro r
  4. 0004intro T
  5. 0005intro C
  6. 0006intro H
  7. 0007intro hp
  8. 0008intro hne
  9. 0009intro hd
  10. 0010intro hC
  11. 0011specialize gauss_coprime_cancel (p)
  12. 0012specialize gauss_coprime_cancel (2)
  13. 0013specialize gauss_coprime_cancel (C)
  14. 0014apply gauss_coprime_cancel
  15. 0015specialize prime_not_divides_coprime (p)
  16. 0016specialize prime_not_divides_coprime (2)
  17. 0017apply prime_not_divides_coprime
  18. 0018exact hp
  19. 0019intro hdiv
  20. 0020specialize lte_prime_nondivisor_two (p)
  21. 0021apply lte_prime_nondivisor_two
  22. 0022exact hp
  23. 0023exact hne
  24. 0024exact hdiv
  25. 0025rewrite hC
  26. 0026specialize multiple_add (p)
  27. 0027specialize multiple_add ((p * r) * T)
  28. 0028specialize multiple_add (d * H)
  29. 0029apply multiple_add
  30. 0030exists r * T
  31. 0031apply mul_assoc
  32. 0032cases hd
  33. 0033exists x * H
  34. 0034rewrite hd_witness
  35. 0035apply mul_assoc