EL0011

lte_prime_divides_correction

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

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

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

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

gauss_coprime_cancel Stable theorem; checked-use authorized prime_not_divides_coprime Stable theorem; checked-use authorized EL000F lte_prime_nondivisor_two multiple_add Stable theorem; checked-use authorized mul_assoc Stable theorem; checked-use authorized

Direct dependents

EL0012 lte_odd_prime_quotient_unit

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

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.

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