PA006Y

odd_upper_remainder_reflection

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

A residue strictly above h and below 2*h+1 has a positive reflected magnitude at most h.

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 r. p = 2 * h + 1 -> (exists gsh_lt_gap_reflection_remainder. gsh_lt_gap_reflection_remainder + S r = p) -> (exists gsh_lt_gap_reflection_upper. gsh_lt_gap_reflection_upper + S h = r) -> (exists m. (exists gsh_lt_gap_reflection_positive. gsh_lt_gap_reflection_positive + S 0 = m) /\ ((exists gsh_le_gap_reflection_bounded. gsh_le_gap_reflection_bounded + m = h) /\ r + m = p))

Structural proof guide

Generated structural guide

A residue strictly above h and below 2*h+1 has a positive reflected magnitude at most h.

Use the direct prerequisites add_assoc, add_comm, mul_succ_left, mul_zero_left, zero_add, add_right_cancel as previously established PA formulas.

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

Referenced ingredients

PA0009 add_assoc PA000F add_comm PA000G mul_succ_left PA000D mul_zero_left PA0001 zero_add PA0012 add_right_cancel

Proof neighborhood

Direct dependencies

PA0009 add_assoc PA000F add_comm PA000G mul_succ_left PA000D mul_zero_left PA0001 zero_add PA0012 add_right_cancel

Direct dependents

PA0070 gauss_pointwise_signed_half_representative

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

50 script commands · 18 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 (3)
add assocadd commadd right cancel
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 r
  4. L4
    intro hp
  5. L5
    intro hrp
  6. L6
    intro hhr
02Separate the logical casesL7–8

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

  1. L7
    cases hhr
  2. L8
    cases hrp
03Establish hrmL9–18

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

  1. L9
    have hrm : r + S x1 = p
  2. L10
    trans S (r + x1)
  3. L11
    apply PA4
  4. L12
    trans S (x1 + r)
  5. L13
    congr
  6. L14
    apply add_comm
  7. L15
    trans x1 + S r
  8. L16
    symm
  9. L17
    apply PA4
  10. L18
    exact hrp_witness
04Establish hsumL19–28

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

  1. L19
    have hsum : (x + S x1) + S h = h + S h
  2. L20
    trans (x + S h) + S x1
  3. L21
    trans x + (S x1 + S h)
  4. L22
    apply add_assoc
  5. L23
    trans x + (S h + S x1)
  6. L24
    congr
  7. L25
    refl
  8. L26
    apply add_comm
  9. L27
    symm
  10. L28
    apply add_assoc
05Calculate and transport equalitiesL29–30

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

  1. L29
    trans r + S x1
  2. L30
    congr
06Use earlier factsL31–31

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

  1. L31
    exact hhr_witness
07Calculate and transport equalitiesL32–33

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

  1. L32
    refl
  2. L33
    trans p
08Use earlier factsL34–34

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

  1. L34
    exact hrm
09Calculate and transport equalitiesL35–36

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

  1. L35
    rewrite hp
  2. L36
    simp [mul_succ_left, mul_zero_left, zero_add, add_assoc]
10Establish hmleL37–37

Establish this local claim before using it. It is not an additional assumption.

  1. L37
    have hmle : exists d. d + S x1 = h
11Construct an explicit witnessL38–38

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

  1. L38
    exists x
12Use earlier factsL39–43

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

  1. L39
    specialize add_right_cancel (x + S x1)
  2. L40
    specialize add_right_cancel h
  3. L41
    specialize add_right_cancel (S h)
  4. L42
    apply add_right_cancel
  5. L43
    exact hsum
13Construct an explicit witnessL44–44

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

  1. L44
    exists (S x1)
14Separate the logical casesL45–45

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

  1. L45
    split
15Construct an explicit witnessL46–46

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

  1. L46
    exists x1
16Calculate and transport equalitiesL47–47

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

  1. L47
    simp
17Separate the logical casesL48–48

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

  1. L48
    split
18Use earlier factsL49–50

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

  1. L49
    exact hmle
  2. L50
    exact hrm

Library-wide reading audit

Original exact command ledger · 50 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro r
  4. 0004intro hp
  5. 0005intro hrp
  6. 0006intro hhr
  7. 0007cases hhr
  8. 0008cases hrp
  9. 0009have hrm : r + S x1 = p
  10. 0010trans S (r + x1)
  11. 0011apply PA4
  12. 0012trans S (x1 + r)
  13. 0013congr
  14. 0014apply add_comm
  15. 0015trans x1 + S r
  16. 0016symm
  17. 0017apply PA4
  18. 0018exact hrp_witness
  19. 0019have hsum : (x + S x1) + S h = h + S h
  20. 0020trans (x + S h) + S x1
  21. 0021trans x + (S x1 + S h)
  22. 0022apply add_assoc
  23. 0023trans x + (S h + S x1)
  24. 0024congr
  25. 0025refl
  26. 0026apply add_comm
  27. 0027symm
  28. 0028apply add_assoc
  29. 0029trans r + S x1
  30. 0030congr
  31. 0031exact hhr_witness
  32. 0032refl
  33. 0033trans p
  34. 0034exact hrm
  35. 0035rewrite hp
  36. 0036simp [mul_succ_left, mul_zero_left, zero_add, add_assoc]
  37. 0037have hmle : exists d. d + S x1 = h
  38. 0038exists x
  39. 0039specialize add_right_cancel (x + S x1)
  40. 0040specialize add_right_cancel h
  41. 0041specialize add_right_cancel (S h)
  42. 0042apply add_right_cancel
  43. 0043exact hsum
  44. 0044exists (S x1)
  45. 0045split
  46. 0046exists x1
  47. 0047simp
  48. 0048split
  49. 0049exact hmle
  50. 0050exact hrm