PA0070 · theorem

gauss_pointwise_signed_half_representative

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

A nonzero canonical product remainder has a positive half-range magnitude, with its sign recorded by a lower/reflected congruence disjunction.

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.

Statement with defined notation

∀ p. ∀ h. ∀ a. ∀ x. ∀ q. ∀ r. p = 2 · h + 1 → a · x = q · p + r → Lt(r,p) → ¬r = 0 → ∃ y. Lt(0,y) ∧ (Le(y,h) ∧ (ModEq(p,a · x,y) ∨ ModEq(p,a · x,2 · h · y)))

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0002 Lt PD0008 ModEq

5 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0008 ModEq

7 occurrences

Exact expanded native-PA statement
forall p h a x q r. p = 2 * h + 1 -> a * x = q * p + r -> (exists gsh_lt_gap_product_remainder. gsh_lt_gap_product_remainder + S r = p) -> ~(r = 0) -> (exists m. (exists gsh_lt_gap_product_positive. gsh_lt_gap_product_positive + S 0 = m) /\ ((exists gsh_le_gap_product_bounded. gsh_le_gap_product_bounded + m = h) /\ ((exists gsh_mod_left_product_lower gsh_mod_right_product_lower. (a * x) + p * gsh_mod_left_product_lower = (m) + p * gsh_mod_right_product_lower) \/ (exists gsh_mod_left_product_upper gsh_mod_right_product_upper. (a * x) + p * gsh_mod_left_product_upper = ((2 * h) * m) + p * gsh_mod_right_product_upper))))

Proof neighborhood

Direct theorem prerequisites

PA0009 add_assoc PA000F add_comm PA000G mul_succ_left PA0002 mul_one PA003B le_or_lt PA002L one_le_of_ne_zero PA003C remainder_decomposition_to_mod_eq PA006Y odd_upper_remainder_reflection PA0024 mod_eq_trans

Direct theorem dependents

PA0071 gauss_pointwise_signed_half_choice

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

76 script commands · 33 reading checkpoints · 5 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 (9)
add assocadd commmul succ leftmul onele or ltone le of ne zeroremainder decomposition to mod eqodd upper remainder reflectionmod eq trans
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro a
  4. L4
    intro x
  5. L5
    intro q
  6. L6
    intro r
  7. L7
    intro hp
  8. L8
    intro hdecomp
  9. L9
    intro hrp
  10. L10
    intro hr0
02Establish hcanonicalL11–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply remainder decomposition to mod eq.

  1. L11
    have hcanonical : ModEq(p,a · x,r)Definitions: ModEq(p,a · x,r)Original native command in the exact edition
  2. L12
    specialize remainder_decomposition_to_mod_eq p
  3. L13
    specialize remainder_decomposition_to_mod_eq (a * x)
  4. L14
    specialize remainder_decomposition_to_mod_eq q
  5. L15
    specialize remainder_decomposition_to_mod_eq r
  6. L16
    apply remainder_decomposition_to_mod_eq
  7. L17
    exact hdecomp
03Establish hsplitL18–21

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

  1. L18
    have hsplit : Le(r,h) ∨ Lt(h,r)Definitions: Le(r,h)Lt(h,r)Original native command in the exact edition
  2. L19
    specialize le_or_lt r
  3. L20
    specialize le_or_lt h
  4. L21
    exact le_or_lt
04Separate the logical casesL22–22

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

  1. L22
    cases hsplit
05Construct an explicit witnessL23–23

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

  1. L23
    exists r
06Separate the logical casesL24–24

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

  1. L24
    split
07Use earlier factsL25–27

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

  1. L25
    specialize one_le_of_ne_zero r
  2. L26
    apply one_le_of_ne_zero
  3. L27
    exact hr0
08Separate the logical casesL28–28

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

  1. L28
    split
09Use earlier factsL29–29

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

  1. L29
    exact hsplit_left
10Separate the logical casesL30–30

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

  1. L30
    left
11Use earlier factsL31–31

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

  1. L31
    exact hcanonical
12Establish hreflectionL32–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd upper remainder reflection.

  1. L32
    have hreflection : ∃ m. Lt(0,m) ∧ (Le(m,h) ∧ r + m = p)Definitions: Lt(0,m)Le(m,h)Original native command in the exact edition
  2. L33
    specialize odd_upper_remainder_reflection p
  3. L34
    specialize odd_upper_remainder_reflection h
  4. L35
    specialize odd_upper_remainder_reflection r
  5. L36
    apply odd_upper_remainder_reflection
  6. L37
    exact hp
  7. L38
    exact hrp
  8. L39
    exact hsplit_right
13Separate the logical casesL40–42

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

  1. L40
    cases hreflection
  2. L41
    cases hreflection_witness
  3. L42
    cases hreflection_witness_right
14Establish hreflected_remainderL43–43

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

  1. L43
    have hreflected_remainder : ModEq(p,r,2 · h · x1)Definitions: ModEq(p,r,2 · h · x1)Original native command in the exact edition
15Construct an explicit witnessL44–45

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

  1. L44
    exists x1
  2. L45
    exists 1
16Calculate and transport equalitiesL46–49

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

  1. L46
    trans (r + x1) + (2 * h) * x1
  2. L47
    rewrite hp
  3. L48
    trans r + (x1 + (2 * h) * x1)
  4. L49
    simp
17Use earlier factsL50–51

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

  1. L50
    specialize mul_succ_left (2 * h)
  2. L51
    specialize mul_succ_left x1
18Calculate and transport equalitiesL52–54

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

  1. L52
    rewrite mul_succ_left
  2. L53
    congr
  3. L54
    refl
19Use earlier factsL55–55

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

  1. L55
    apply add_comm
20Calculate and transport equalitiesL56–56

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

  1. L56
    symm
21Use earlier factsL57–57

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

  1. L57
    apply add_assoc
22Calculate and transport equalitiesL58–58

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

  1. L58
    rewrite hreflection_witness_right_right
23Use earlier factsL59–59

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

  1. L59
    specialize mul_one p
24Calculate and transport equalitiesL60–60

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

  1. L60
    rewrite mul_one
25Use earlier factsL61–61

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

  1. L61
    apply add_comm
26Establish hreflected_productL62–69

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

  1. L62
    have hreflected_product : ModEq(p,a · x,2 · h · x1)Definitions: ModEq(p,a · x,2 · h · x1)Original native command in the exact edition
  2. L63
    specialize mod_eq_trans p
  3. L64
    specialize mod_eq_trans (a * x)
  4. L65
    specialize mod_eq_trans r
  5. L66
    specialize mod_eq_trans ((2 * h) * x1)
  6. L67
    apply mod_eq_trans
  7. L68
    exact hcanonical
  8. L69
    exact hreflected_remainder
27Construct an explicit witnessL70–70

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

  1. L70
    exists x1
28Separate the logical casesL71–71

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

  1. L71
    split
29Use earlier factsL72–72

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

  1. L72
    exact hreflection_witness_left
30Separate the logical casesL73–73

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

  1. L73
    split
31Use earlier factsL74–74

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

  1. L74
    exact hreflection_witness_right_left
32Separate the logical casesL75–75

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

  1. L75
    right
33Use earlier factsL76–76

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

  1. L76
    exact hreflected_product

Library-wide reading audit

Original defined command ledger · 76 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro x
  5. 0005intro q
  6. 0006intro r
  7. 0007intro hp
  8. 0008intro hdecomp
  9. 0009intro hrp
  10. 0010intro hr0
  11. 0011have hcanonical : ModEq(p,a · x,r)
    Exact native replay linehave hcanonical : exists gsh_mod_left_canonical_remainder gsh_mod_right_canonical_remainder. (a * x) + p * gsh_mod_left_canonical_remainder = (r) + p * gsh_mod_right_canonical_remainder
  12. 0012specialize remainder_decomposition_to_mod_eq p
  13. 0013specialize remainder_decomposition_to_mod_eq (a * x)
  14. 0014specialize remainder_decomposition_to_mod_eq q
  15. 0015specialize remainder_decomposition_to_mod_eq r
  16. 0016apply remainder_decomposition_to_mod_eq
  17. 0017exact hdecomp
  18. 0018have hsplit : Le(r,h) ∨ Lt(h,r)
    Exact native replay linehave hsplit : (exists d. d + r = h) \/ (exists d. d + S h = r)
  19. 0019specialize le_or_lt r
  20. 0020specialize le_or_lt h
  21. 0021exact le_or_lt
  22. 0022cases hsplit
  23. 0023exists r
  24. 0024split
  25. 0025specialize one_le_of_ne_zero r
  26. 0026apply one_le_of_ne_zero
  27. 0027exact hr0
  28. 0028split
  29. 0029exact hsplit_left
  30. 0030left
  31. 0031exact hcanonical
  32. 0032have hreflection : ∃ m. Lt(0,m) ∧ (Le(m,h) ∧ r + m = p)
    Exact native replay linehave hreflection : 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)
  33. 0033specialize odd_upper_remainder_reflection p
  34. 0034specialize odd_upper_remainder_reflection h
  35. 0035specialize odd_upper_remainder_reflection r
  36. 0036apply odd_upper_remainder_reflection
  37. 0037exact hp
  38. 0038exact hrp
  39. 0039exact hsplit_right
  40. 0040cases hreflection
  41. 0041cases hreflection_witness
  42. 0042cases hreflection_witness_right
  43. 0043have hreflected_remainder : ModEq(p,r,2 · h · x1)
    Exact native replay linehave hreflected_remainder : exists gsh_mod_left_reflected_remainder gsh_mod_right_reflected_remainder. (r) + p * gsh_mod_left_reflected_remainder = ((2 * h) * x1) + p * gsh_mod_right_reflected_remainder
  44. 0044exists x1
  45. 0045exists 1
  46. 0046trans (r + x1) + (2 * h) * x1
  47. 0047rewrite hp
  48. 0048trans r + (x1 + (2 * h) * x1)
  49. 0049simp
  50. 0050specialize mul_succ_left (2 * h)
  51. 0051specialize mul_succ_left x1
  52. 0052rewrite mul_succ_left
  53. 0053congr
  54. 0054refl
  55. 0055apply add_comm
  56. 0056symm
  57. 0057apply add_assoc
  58. 0058rewrite hreflection_witness_right_right
  59. 0059specialize mul_one p
  60. 0060rewrite mul_one
  61. 0061apply add_comm
  62. 0062have hreflected_product : ModEq(p,a · x,2 · h · x1)
    Exact native replay linehave hreflected_product : exists gsh_mod_left_reflected_product gsh_mod_right_reflected_product. (a * x) + p * gsh_mod_left_reflected_product = ((2 * h) * x1) + p * gsh_mod_right_reflected_product
  63. 0063specialize mod_eq_trans p
  64. 0064specialize mod_eq_trans (a * x)
  65. 0065specialize mod_eq_trans r
  66. 0066specialize mod_eq_trans ((2 * h) * x1)
  67. 0067apply mod_eq_trans
  68. 0068exact hcanonical
  69. 0069exact hreflected_remainder
  70. 0070exists x1
  71. 0071split
  72. 0072exact hreflection_witness_left
  73. 0073split
  74. 0074exact hreflection_witness_right_left
  75. 0075right
  76. 0076exact hreflected_product