PA00C6 · theorem

odd_signed_division_branch_exact

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

A Gauss signed congruence determines the exact canonical lower/reflected remainder branch.

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. ∀ n. ∀ q. ∀ r. ∀ m. ∀ s. p = 2 · h + 1 → n = p · q + r → Lt(r,p) → Lt(0,m) → Le(m,h) → s = 0 ∧ ModEq(p,n,m) ∨ s = 1 ∧ ModEq(p,n,2 · h · m) → s = 0 ∧ r = m ∨ s = 1 ∧ r + m = p

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

PD0002 Lt PD0008 ModEq

5 occurrences

Exact expanded native-PA statement
forall p h n q r m s. p = 2 * h + 1 -> n = p * q + r -> (exists gsp_lt_gap_gsd_r_below_p. gsp_lt_gap_gsd_r_below_p + S r = p) -> (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) -> (((s = 0 /\ (exists wpp_mod_left_gsd_n_mod_m wpp_mod_right_gsd_n_mod_m. (n) + p * wpp_mod_left_gsd_n_mod_m = (m) + p * wpp_mod_right_gsd_n_mod_m)) \/ (s = 1 /\ (exists wpp_mod_left_gsd_n_mod_reflected wpp_mod_right_gsd_n_mod_reflected. (n) + p * wpp_mod_left_gsd_n_mod_reflected = ((2 * h) * m) + p * wpp_mod_right_gsd_n_mod_reflected)))) -> (((s = 0 /\ r = m) \/ (s = 1 /\ r + m = p)))

Proof neighborhood

Direct theorem prerequisites

PA00C2 odd_half_strictly_below_modulus PA0033 lt_of_le_of_lt PA00C3 odd_half_positive_complement_exists PA00C4 predecessor_multiple_mod_complement PA00C5 canonical_remainder_from_mod PA0024 mod_eq_trans

Direct theorem dependents

PA00CO odd_signed_division_congruence_mod_two

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

90 script commands · 21 reading checkpoints · 7 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 (6)
odd half strictly below moduluslt of le of ltodd half positive complement existspredecessor multiple mod complementcanonical remainder from modmod 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 n
  4. L4
    intro q
  5. L5
    intro r
  6. L6
    intro m
  7. L7
    intro s
  8. L8
    intro hp
  9. L9
    intro hdivision
  10. L10
    intro hrbelow
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hmpositive
  2. L12
    intro hmle
  3. L13
    intro hsigned
03Establish hhalfbelowL14–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd half strictly below modulus.

  1. L14
    have hhalfbelow : Lt(h,p)Definitions: Lt(h,p)Original native command in the exact edition
  2. L15
    specialize odd_half_strictly_below_modulus p
  3. L16
    specialize odd_half_strictly_below_modulus h
  4. L17
    apply odd_half_strictly_below_modulus
  5. L18
    exact hp
04Establish hmbelowL19–25

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

  1. L19
    have hmbelow : Lt(m,p)Definitions: Lt(m,p)Original native command in the exact edition
  2. L20
    specialize lt_of_le_of_lt m
  3. L21
    specialize lt_of_le_of_lt h
  4. L22
    specialize lt_of_le_of_lt p
  5. L23
    apply lt_of_le_of_lt
  6. L24
    exact hmle
  7. L25
    exact hhalfbelow
05Separate the logical casesL26–29

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

  1. L26
    cases hsigned
  2. L27
    cases hsigned_left
  3. L28
    left
  4. L29
    split
06Use earlier factsL30–39

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

  1. L30
    exact hsigned_left_left
  2. L31
    specialize canonical_remainder_from_mod p
  3. L32
    specialize canonical_remainder_from_mod n
  4. L33
    specialize canonical_remainder_from_mod q
  5. L34
    specialize canonical_remainder_from_mod r
  6. L35
    specialize canonical_remainder_from_mod m
  7. L36
    apply canonical_remainder_from_mod
  8. L37
    exact hdivision
  9. L38
    exact hrbelow
  10. L39
    exact hmbelow
07Use earlier factsL40–40

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

  1. L40
    exact hsigned_left_right
08Separate the logical casesL41–41

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

  1. L41
    cases hsigned_right
09Establish hcomplementL42–49

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd half positive complement exists.

  1. L42
    have hcomplement : ∃ t. Lt(t,p) ∧ t + m = pDefinitions: Lt(t,p)Original native command in the exact edition
  2. L43
    specialize odd_half_positive_complement_exists p
  3. L44
    specialize odd_half_positive_complement_exists h
  4. L45
    specialize odd_half_positive_complement_exists m
  5. L46
    apply odd_half_positive_complement_exists
  6. L47
    exact hp
  7. L48
    exact hmpositive
  8. L49
    exact hmle
10Separate the logical casesL50–51

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

  1. L50
    cases hcomplement
  2. L51
    cases hcomplement_witness
11Establish hpsuccL52–55

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

  1. L52
    have hpsucc : p = S (2 * h)
  2. L53
    trans 2 * h + 1
  3. L54
    exact hp
  4. L55
    simp
12Establish hkmodtL56–63

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

  1. L56
    have hkmodt : ModEq(p,2 · h · m,x)Definitions: ModEq(p,2 · h · m,x)Original native command in the exact edition
  2. L57
    specialize predecessor_multiple_mod_complement p
  3. L58
    specialize predecessor_multiple_mod_complement (2 * h)
  4. L59
    specialize predecessor_multiple_mod_complement m
  5. L60
    specialize predecessor_multiple_mod_complement x
  6. L61
    apply predecessor_multiple_mod_complement
  7. L62
    exact hpsucc
  8. L63
    exact hcomplement_witness_right
13Establish hnlocaltL64–71

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

  1. L64
    have hnlocalt : ModEq(p,n,x)Definitions: ModEq(p,n,x)Original native command in the exact edition
  2. L65
    specialize mod_eq_trans p
  3. L66
    specialize mod_eq_trans n
  4. L67
    specialize mod_eq_trans ((2 * h) * m)
  5. L68
    specialize mod_eq_trans x
  6. L69
    apply mod_eq_trans
  7. L70
    exact hsigned_right_right
  8. L71
    exact hkmodt
14Establish hrtL72–81

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

  1. L72
    have hrt : r = x
  2. L73
    specialize canonical_remainder_from_mod p
  3. L74
    specialize canonical_remainder_from_mod n
  4. L75
    specialize canonical_remainder_from_mod q
  5. L76
    specialize canonical_remainder_from_mod r
  6. L77
    specialize canonical_remainder_from_mod x
  7. L78
    apply canonical_remainder_from_mod
  8. L79
    exact hdivision
  9. L80
    exact hrbelow
  10. L81
    exact hcomplement_witness_left
15Use earlier factsL82–82

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

  1. L82
    exact hnlocalt
16Separate the logical casesL83–84

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

  1. L83
    right
  2. L84
    split
17Use earlier factsL85–85

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

  1. L85
    exact hsigned_right_left
18Calculate and transport equalitiesL86–87

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

  1. L86
    trans x + m
  2. L87
    congr
19Use earlier factsL88–88

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

  1. L88
    exact hrt
20Calculate and transport equalitiesL89–89

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

  1. L89
    refl
21Use earlier factsL90–90

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

  1. L90
    exact hcomplement_witness_right

Library-wide reading audit

Original defined command ledger · 90 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro n
  4. 0004intro q
  5. 0005intro r
  6. 0006intro m
  7. 0007intro s
  8. 0008intro hp
  9. 0009intro hdivision
  10. 0010intro hrbelow
  11. 0011intro hmpositive
  12. 0012intro hmle
  13. 0013intro hsigned
  14. 0014have hhalfbelow : Lt(h,p)
    Exact native replay linehave hhalfbelow : exists d. d + S h = p
  15. 0015specialize odd_half_strictly_below_modulus p
  16. 0016specialize odd_half_strictly_below_modulus h
  17. 0017apply odd_half_strictly_below_modulus
  18. 0018exact hp
  19. 0019have hmbelow : Lt(m,p)
    Exact native replay linehave hmbelow : exists gsp_lt_gap_gsd_m_below_p. gsp_lt_gap_gsd_m_below_p + S m = p
  20. 0020specialize lt_of_le_of_lt m
  21. 0021specialize lt_of_le_of_lt h
  22. 0022specialize lt_of_le_of_lt p
  23. 0023apply lt_of_le_of_lt
  24. 0024exact hmle
  25. 0025exact hhalfbelow
  26. 0026cases hsigned
  27. 0027cases hsigned_left
  28. 0028left
  29. 0029split
  30. 0030exact hsigned_left_left
  31. 0031specialize canonical_remainder_from_mod p
  32. 0032specialize canonical_remainder_from_mod n
  33. 0033specialize canonical_remainder_from_mod q
  34. 0034specialize canonical_remainder_from_mod r
  35. 0035specialize canonical_remainder_from_mod m
  36. 0036apply canonical_remainder_from_mod
  37. 0037exact hdivision
  38. 0038exact hrbelow
  39. 0039exact hmbelow
  40. 0040exact hsigned_left_right
  41. 0041cases hsigned_right
  42. 0042have hcomplement : ∃ t. Lt(t,p) ∧ t + m = p
    Exact native replay linehave hcomplement : exists t. (exists gsp_lt_gap_gsd_t_below_p. gsp_lt_gap_gsd_t_below_p + S t = p) /\ t + m = p
  43. 0043specialize odd_half_positive_complement_exists p
  44. 0044specialize odd_half_positive_complement_exists h
  45. 0045specialize odd_half_positive_complement_exists m
  46. 0046apply odd_half_positive_complement_exists
  47. 0047exact hp
  48. 0048exact hmpositive
  49. 0049exact hmle
  50. 0050cases hcomplement
  51. 0051cases hcomplement_witness
  52. 0052have hpsucc : p = S (2 * h)
  53. 0053trans 2 * h + 1
  54. 0054exact hp
  55. 0055simp
  56. 0056have hkmodt : ModEq(p,2 · h · m,x)
    Exact native replay linehave hkmodt : exists wpp_mod_left_gsd_local_predecessor_mod wpp_mod_right_gsd_local_predecessor_mod. ((2 * h) * m) + p * wpp_mod_left_gsd_local_predecessor_mod = (x) + p * wpp_mod_right_gsd_local_predecessor_mod
  57. 0057specialize predecessor_multiple_mod_complement p
  58. 0058specialize predecessor_multiple_mod_complement (2 * h)
  59. 0059specialize predecessor_multiple_mod_complement m
  60. 0060specialize predecessor_multiple_mod_complement x
  61. 0061apply predecessor_multiple_mod_complement
  62. 0062exact hpsucc
  63. 0063exact hcomplement_witness_right
  64. 0064have hnlocalt : ModEq(p,n,x)
    Exact native replay linehave hnlocalt : exists wpp_mod_left_gsd_local_n_mod_t wpp_mod_right_gsd_local_n_mod_t. (n) + p * wpp_mod_left_gsd_local_n_mod_t = (x) + p * wpp_mod_right_gsd_local_n_mod_t
  65. 0065specialize mod_eq_trans p
  66. 0066specialize mod_eq_trans n
  67. 0067specialize mod_eq_trans ((2 * h) * m)
  68. 0068specialize mod_eq_trans x
  69. 0069apply mod_eq_trans
  70. 0070exact hsigned_right_right
  71. 0071exact hkmodt
  72. 0072have hrt : r = x
  73. 0073specialize canonical_remainder_from_mod p
  74. 0074specialize canonical_remainder_from_mod n
  75. 0075specialize canonical_remainder_from_mod q
  76. 0076specialize canonical_remainder_from_mod r
  77. 0077specialize canonical_remainder_from_mod x
  78. 0078apply canonical_remainder_from_mod
  79. 0079exact hdivision
  80. 0080exact hrbelow
  81. 0081exact hcomplement_witness_left
  82. 0082exact hnlocalt
  83. 0083right
  84. 0084split
  85. 0085exact hsigned_right_left
  86. 0086trans x + m
  87. 0087congr
  88. 0088exact hrt
  89. 0089refl
  90. 0090exact hcomplement_witness_right