PA00C3

odd_half_positive_complement_exists

Alpha v34 checked-use theorem · independently closed; not Stable

A positive magnitude at most the odd half has a complement below the modulus.

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 PA statement

forall p h m. p = 2 * h + 1 -> (exists gsp_lt_gap_gsd_m_positive. gsp_lt_gap_gsd_m_positive + S 0 = m) -> (exists gsp_le_gap_gsd_m_le_h. gsp_le_gap_gsd_m_le_h + m = h) -> (exists t. (exists gsp_lt_gap_gsd_t_below_p. gsp_lt_gap_gsd_t_below_p + S t = p) /\ t + m = p)

Structural proof guide

Generated structural guide

A positive magnitude at most the odd half has a complement below the modulus.

Use the direct prerequisites lt_irrefl_expanded, nonzero_is_succ, add_assoc, add_comm, mul_comm, zero_add, add_succ_left as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (3), equality transport (3), certified simplification (2).

Referenced ingredients

PA0010 lt_irrefl_expanded PA001V nonzero_is_succ PA0009 add_assoc PA000F add_comm PA000H mul_comm PA0001 zero_add PA000E add_succ_left

Proof neighborhood

Direct dependencies

PA0010 lt_irrefl_expanded PA001V nonzero_is_succ PA0009 add_assoc PA000F add_comm PA000H mul_comm PA0001 zero_add PA000E add_succ_left

Direct dependents

PA00C6 odd_signed_division_branch_exact

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

59 script commands · 22 reading checkpoints · 3 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 (5)
lt irrefl expandednonzero is succadd assocadd commmul comm
01Fix variables and assumptionsL1–6

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro m
  4. L4
    intro hp
  5. L5
    intro hmpositive
  6. L6
    intro hmle
02Separate the logical casesL7–7

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

  1. L7
    cases hmle
03Establish hsumL8–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add assoc.

  1. L8
    have hsum : (h + x + 1) + m = p
  2. L9
    trans h + (x + m) + 1
  3. L10
    simp [add_assoc, add_comm]
  4. L11
    congr
  5. L12
    trans (m + x) + h
  6. L13
    symm
  7. L14
    apply add_assoc
  8. L15
    trans (x + m) + h
  9. L16
    congr
  10. L17
    apply add_comm
04Calculate and transport equalitiesL18–18

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

  1. L18
    refl
05Use earlier factsL19–19

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

  1. L19
    apply add_assoc
06Calculate and transport equalitiesL20–26

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

  1. L20
    rewrite hmle_witness
  2. L21
    rewrite hp
  3. L22
    trans h + h + 1
  4. L23
    refl
  5. L24
    congr
  6. L25
    trans h * 2
  7. L26
    simp [zero_add]
07Use earlier factsL27–29

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

  1. L27
    specialize mul_comm h
  2. L28
    specialize mul_comm 2
  3. L29
    apply mul_comm
08Calculate and transport equalitiesL30–30

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

  1. L30
    refl
09Establish hm0L31–36

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

  1. L31
    have hm0 : ~(m = 0)
  2. L32
    intro hmzero
  3. L33
    specialize lt_irrefl_expanded 0
  4. L34
    apply lt_irrefl_expanded
  5. L35
    rewrite hmzero at hmpositive
  6. L36
    exact hmpositive
10Establish hmsuccL37–40

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply nonzero is succ.

  1. L37
    have hmsucc : exists z. m = S z
  2. L38
    specialize nonzero_is_succ m
  3. L39
    apply nonzero_is_succ
  4. L40
    exact hm0
11Separate the logical casesL41–41

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

  1. L41
    cases hmsucc
12Construct an explicit witnessL42–42

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

  1. L42
    exists h + x + 1
13Separate the logical casesL43–43

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

  1. L43
    split
14Construct an explicit witnessL44–44

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

  1. L44
    exists x1
15Calculate and transport equalitiesL45–45

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

  1. L45
    trans S (x1 + (h + x + 1))
16Use earlier factsL46–46

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

  1. L46
    apply PA4
17Calculate and transport equalitiesL47–48

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

  1. L47
    trans S ((h + x + 1) + x1)
  2. L48
    congr
18Use earlier factsL49–49

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

  1. L49
    apply add_comm
19Calculate and transport equalitiesL50–51

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

  1. L50
    trans (h + x + 1) + S x1
  2. L51
    symm
20Use earlier factsL52–52

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

  1. L52
    apply PA4
21Calculate and transport equalitiesL53–56

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

  1. L53
    trans (h + x + 1) + m
  2. L54
    congr
  3. L55
    refl
  4. L56
    symm
22Use earlier factsL57–59

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

  1. L57
    exact hmsucc_witness
  2. L58
    exact hsum
  3. L59
    exact hsum

Library-wide reading audit

Original exact command ledger · 59 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro m
  4. 0004intro hp
  5. 0005intro hmpositive
  6. 0006intro hmle
  7. 0007cases hmle
  8. 0008have hsum : (h + x + 1) + m = p
  9. 0009trans h + (x + m) + 1
  10. 0010simp [add_assoc, add_comm]
  11. 0011congr
  12. 0012trans (m + x) + h
  13. 0013symm
  14. 0014apply add_assoc
  15. 0015trans (x + m) + h
  16. 0016congr
  17. 0017apply add_comm
  18. 0018refl
  19. 0019apply add_assoc
  20. 0020rewrite hmle_witness
  21. 0021rewrite hp
  22. 0022trans h + h + 1
  23. 0023refl
  24. 0024congr
  25. 0025trans h * 2
  26. 0026simp [zero_add]
  27. 0027specialize mul_comm h
  28. 0028specialize mul_comm 2
  29. 0029apply mul_comm
  30. 0030refl
  31. 0031have hm0 : ~(m = 0)
  32. 0032intro hmzero
  33. 0033specialize lt_irrefl_expanded 0
  34. 0034apply lt_irrefl_expanded
  35. 0035rewrite hmzero at hmpositive
  36. 0036exact hmpositive
  37. 0037have hmsucc : exists z. m = S z
  38. 0038specialize nonzero_is_succ m
  39. 0039apply nonzero_is_succ
  40. 0040exact hm0
  41. 0041cases hmsucc
  42. 0042exists h + x + 1
  43. 0043split
  44. 0044exists x1
  45. 0045trans S (x1 + (h + x + 1))
  46. 0046apply PA4
  47. 0047trans S ((h + x + 1) + x1)
  48. 0048congr
  49. 0049apply add_comm
  50. 0050trans (h + x + 1) + S x1
  51. 0051symm
  52. 0052apply PA4
  53. 0053trans (h + x + 1) + m
  54. 0054congr
  55. 0055refl
  56. 0056symm
  57. 0057exact hmsucc_witness
  58. 0058exact hsum
  59. 0059exact hsum