PA0072 · theorem

gauss_half_range_signed_choices

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

A prime odd half-range and a nondivisible multiplier provide a signed choice at every decoded entry.

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. ∀ b. ∀ c. p = 2 · h + 1 → Prime(p) → ¬Dvd(p,a) → Range(b,c,1,h) → ∀ x. Lt(x,h) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (Lt(0,z) ∧ (Le(z,h) ∧ ((n = 0 ∨ n = 1) ∧ (n = 0 ∧ ModEq(p,a · y,z) ∨ n = 1 ∧ ModEq(p,a · y,2 · h · z)))))

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 PD0003 Dvd PD0004 Prime PD0008 ModEq PD0013 BetaAt PD0018 Range

9 occurrences

In local proof propositions

PD0001 Le PD0003 Dvd PD0007 DivRem PD0013 BetaAt PD0030 UnitResidue

7 occurrences

Exact expanded native-PA statement
forall p h a b c. p = 2 * h + 1 -> ((~(p = 1) /\ forall gsp_prime_left_half_range_prime gsp_prime_right_half_range_prime. p = gsp_prime_left_half_range_prime * gsp_prime_right_half_range_prime -> gsp_prime_left_half_range_prime = 1 \/ gsp_prime_right_half_range_prime = 1)) -> (~(exists gsp_divisor_factor_half_range_multiplier. a = p * gsp_divisor_factor_half_range_multiplier)) -> (forall gsp_range_index_half_range_source. (exists gsp_lt_gap_half_range_source_range_bound. gsp_lt_gap_half_range_source_range_bound + S gsp_range_index_half_range_source = h) -> (((exists gsp_beta_height_half_range_source_range_entry. gsp_beta_height_half_range_source_range_entry + S (1 + gsp_range_index_half_range_source) = S ((S (gsp_range_index_half_range_source)) * c)) /\ exists gsp_beta_quotient_half_range_source_range_entry. b = gsp_beta_quotient_half_range_source_range_entry * S ((S (gsp_range_index_half_range_source)) * c) + (1 + gsp_range_index_half_range_source)))) -> (forall gsp_choice_index_half_range_choices. (exists gsp_lt_gap_half_range_choices_choice_bound. gsp_lt_gap_half_range_choices_choice_bound + S gsp_choice_index_half_range_choices = h) -> (exists gsp_value_half_range_choices_choice gsp_magnitude_half_range_choices_choice gsp_sign_half_range_choices_choice. (((exists ff_h_gsp_half_range_choices_choice_source. ff_h_gsp_half_range_choices_choice_source + S (gsp_value_half_range_choices_choice) = S ((S (gsp_choice_index_half_range_choices)) * c)) /\ exists ff_q_gsp_half_range_choices_choice_source. b = ff_q_gsp_half_range_choices_choice_source * S ((S (gsp_choice_index_half_range_choices)) * c) + (gsp_value_half_range_choices_choice))) /\ ((exists gsp_lt_gap_half_range_choices_choice_positive. gsp_lt_gap_half_range_choices_choice_positive + S 0 = gsp_magnitude_half_range_choices_choice) /\ ((exists gsp_le_gap_half_range_choices_choice_bounded. gsp_le_gap_half_range_choices_choice_bounded + gsp_magnitude_half_range_choices_choice = h) /\ ((gsp_sign_half_range_choices_choice = 0 \/ gsp_sign_half_range_choices_choice = 1) /\ (((gsp_sign_half_range_choices_choice = 0 /\ (exists gsp_mod_left_half_range_choices_choice_lower gsp_mod_right_half_range_choices_choice_lower. (a * gsp_value_half_range_choices_choice) + p * gsp_mod_left_half_range_choices_choice_lower = (gsp_magnitude_half_range_choices_choice) + p * gsp_mod_right_half_range_choices_choice_lower)) \/ (gsp_sign_half_range_choices_choice = 1 /\ (exists gsp_mod_left_half_range_choices_choice_reflected gsp_mod_right_half_range_choices_choice_reflected. (a * gsp_value_half_range_choices_choice) + p * gsp_mod_left_half_range_choices_choice_reflected = ((2 * h) * gsp_magnitude_half_range_choices_choice) + p * gsp_mod_right_half_range_choices_choice_reflected)))))))))

Proof neighborhood

Direct theorem prerequisites

PA0031 prime_nonzero PA001D division_remainder_exists PA0034 beta_half_range_entry_bounds PA0038 euclid_prime_dvd_product PA0039 divisor_le_nonzero PA003A lt_not_le PA000H mul_comm PA0071 gauss_pointwise_signed_half_choice

Direct theorem dependents

PA0075 gauss_half_range_signed_prefix_exists

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

92 script commands · 24 reading checkpoints · 9 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 (8)
prime nonzerodivision remainder existsbeta half range entry boundseuclid prime dvd productdivisor le nonzerolt not lemul commgauss pointwise signed half choice
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 b
  5. L5
    intro c
  6. L6
    intro hp
  7. L7
    intro hprime
  8. L8
    intro hnotdiv
  9. L9
    intro hrange
  10. L10
    intro i
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hi
03Establish hsourceL12–15

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

  1. L12
    have hsource : BetaAt(b,c,i,1 + i)Definitions: BetaAt(b,c,i,1 + i)Original native command in the exact edition
  2. L13
    specialize hrange i
  3. L14
    apply hrange
  4. L15
    exact hi
04Establish hboundsL16–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta half range entry bounds.

  1. L16
    have hbounds : UnitResidue(p,1 + i)Definitions: UnitResidue(p,1 + i)Original native command in the exact edition
  2. L17
    specialize beta_half_range_entry_bounds p
  3. L18
    specialize beta_half_range_entry_bounds h
  4. L19
    specialize beta_half_range_entry_bounds b
  5. L20
    specialize beta_half_range_entry_bounds c
  6. L21
    specialize beta_half_range_entry_bounds i
  7. L22
    specialize beta_half_range_entry_bounds (1 + i)
  8. L23
    apply beta_half_range_entry_bounds
  9. L24
    exact hp
  10. L25
    exact hrange
05Use earlier factsL26–27

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

  1. L26
    exact hi
  2. L27
    exact hsource
06Separate the logical casesL28–28

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

  1. L28
    cases hbounds
07Establish hp0L29–34

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

  1. L29
    have hp0 : ~(p = 0)
  2. L30
    intro hpzero
  3. L31
    specialize prime_nonzero p
  4. L32
    apply prime_nonzero
  5. L33
    exact hprime
  6. L34
    exact hpzero
08Establish hdivL35–39

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

  1. L35
    have hdiv : ∃ q. ∃ r. DivRem(a · (1 + i),p,q,r)Definitions: DivRem(a · (1 + i),p,q,r)Original native command in the exact edition
  2. L36
    specialize division_remainder_exists p
  3. L37
    specialize division_remainder_exists (a * (1 + i))
  4. L38
    apply division_remainder_exists
  5. L39
    exact hp0
09Separate the logical casesL40–42

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

  1. L40
    cases hdiv
  2. L41
    cases hdiv_witness
  3. L42
    cases hdiv_witness_witness
10Establish hrem0L43–44

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

  1. L43
    have hrem0 : ~(x1 = 0)
  2. L44
    intro hremzero
11Establish hmultipleL45–45

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

  1. L45
    have hmultiple : Dvd(p,a · (1 + i))Definitions: Dvd(p,a · (1 + i))Original native command in the exact edition
12Construct an explicit witnessL46–46

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

  1. L46
    exists x
13Calculate and transport equalitiesL47–47

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

  1. L47
    trans p * x + x1
14Use earlier factsL48–48

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

  1. L48
    exact hdiv_witness_witness_left
15Calculate and transport equalitiesL49–49

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

  1. L49
    rewrite hremzero
16Use earlier factsL50–50

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

  1. L50
    apply PA3
17Establish hfactorL51–57

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclid prime dvd product.

  1. L51
    have hfactor : Dvd(p,a) ∨ Dvd(p,1 + i)Definitions: Dvd(p,a)Dvd(p,1 + i)Original native command in the exact edition
  2. L52
    specialize euclid_prime_dvd_product p
  3. L53
    specialize euclid_prime_dvd_product a
  4. L54
    specialize euclid_prime_dvd_product (1 + i)
  5. L55
    apply euclid_prime_dvd_product
  6. L56
    exact hprime
  7. L57
    exact hmultiple
18Separate the logical casesL58–58

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

  1. L58
    cases hfactor
19Use earlier factsL59–60

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

  1. L59
    apply hnotdiv
  2. L60
    exact hfactor_left
20Establish hpleL61–70

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

  1. L61
  2. L62
    specialize divisor_le_nonzero p
  3. L63
    specialize divisor_le_nonzero (1 + i)
  4. L64
    apply divisor_le_nonzero
  5. L65
    exact hbounds_left
  6. L66
    exact hfactor_right
  7. L67
    specialize lt_not_le (1 + i)
  8. L68
    specialize lt_not_le p
  9. L69
    apply lt_not_le
  10. L70
    exact hbounds_right
21Use earlier factsL71–71

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

  1. L71
    exact hple
22Establish hdecompL72–81

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

  1. L72
    have hdecomp : a * (1 + i) = x * p + x1
  2. L73
    trans p * x + x1
  3. L74
    exact hdiv_witness_witness_left
  4. L75
    congr
  5. L76
    apply mul_comm
  6. L77
    refl
  7. L78
    specialize gauss_pointwise_signed_half_choice p
  8. L79
    specialize gauss_pointwise_signed_half_choice h
  9. L80
    specialize gauss_pointwise_signed_half_choice a
  10. L81
    specialize gauss_pointwise_signed_half_choice b
23Use earlier factsL82–91

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

  1. L82
    specialize gauss_pointwise_signed_half_choice c
  2. L83
    specialize gauss_pointwise_signed_half_choice i
  3. L84
    specialize gauss_pointwise_signed_half_choice (1 + i)
  4. L85
    specialize gauss_pointwise_signed_half_choice x
  5. L86
    specialize gauss_pointwise_signed_half_choice x1
  6. L87
    apply gauss_pointwise_signed_half_choice
  7. L88
    exact hp
  8. L89
    exact hsource
  9. L90
    exact hdecomp
  10. L91
    exact hdiv_witness_witness_right
24Use earlier factsL92–92

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

  1. L92
    exact hrem0

Library-wide reading audit

Original defined command ledger · 92 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro hp
  7. 0007intro hprime
  8. 0008intro hnotdiv
  9. 0009intro hrange
  10. 0010intro i
  11. 0011intro hi
  12. 0012have hsource : BetaAt(b,c,i,1 + i)
    Exact native replay linehave hsource : ((exists gsp_beta_height_half_range_source_entry_i. gsp_beta_height_half_range_source_entry_i + S (1 + i) = S ((S (i)) * c)) /\ exists gsp_beta_quotient_half_range_source_entry_i. b = gsp_beta_quotient_half_range_source_entry_i * S ((S (i)) * c) + (1 + i))
  13. 0013specialize hrange i
  14. 0014apply hrange
  15. 0015exact hi
  16. 0016have hbounds : UnitResidue(p,1 + i)
    Exact native replay linehave hbounds : (~(1 + i = 0) /\ (exists gsp_half_value_bound_gap. gsp_half_value_bound_gap + S (1 + i) = p))
  17. 0017specialize beta_half_range_entry_bounds p
  18. 0018specialize beta_half_range_entry_bounds h
  19. 0019specialize beta_half_range_entry_bounds b
  20. 0020specialize beta_half_range_entry_bounds c
  21. 0021specialize beta_half_range_entry_bounds i
  22. 0022specialize beta_half_range_entry_bounds (1 + i)
  23. 0023apply beta_half_range_entry_bounds
  24. 0024exact hp
  25. 0025exact hrange
  26. 0026exact hi
  27. 0027exact hsource
  28. 0028cases hbounds
  29. 0029have hp0 : ~(p = 0)
  30. 0030intro hpzero
  31. 0031specialize prime_nonzero p
  32. 0032apply prime_nonzero
  33. 0033exact hprime
  34. 0034exact hpzero
  35. 0035have hdiv : ∃ q. ∃ r. DivRem(a · (1 + i),p,q,r)
    Exact native replay linehave hdiv : exists q r. a * (1 + i) = p * q + r /\ (exists gsp_half_value_bound_gap. gsp_half_value_bound_gap + S (r) = p)
  36. 0036specialize division_remainder_exists p
  37. 0037specialize division_remainder_exists (a * (1 + i))
  38. 0038apply division_remainder_exists
  39. 0039exact hp0
  40. 0040cases hdiv
  41. 0041cases hdiv_witness
  42. 0042cases hdiv_witness_witness
  43. 0043have hrem0 : ~(x1 = 0)
  44. 0044intro hremzero
  45. 0045have hmultiple : Dvd(p,a · (1 + i))
    Exact native replay linehave hmultiple : exists k. a * (1 + i) = p * k
  46. 0046exists x
  47. 0047trans p * x + x1
  48. 0048exact hdiv_witness_witness_left
  49. 0049rewrite hremzero
  50. 0050apply PA3
  51. 0051have hfactor : Dvd(p,a) ∨ Dvd(p,1 + i)
    Exact native replay linehave hfactor : (exists u. a = p * u) \/ exists v. 1 + i = p * v
  52. 0052specialize euclid_prime_dvd_product p
  53. 0053specialize euclid_prime_dvd_product a
  54. 0054specialize euclid_prime_dvd_product (1 + i)
  55. 0055apply euclid_prime_dvd_product
  56. 0056exact hprime
  57. 0057exact hmultiple
  58. 0058cases hfactor
  59. 0059apply hnotdiv
  60. 0060exact hfactor_left
  61. 0061have hple : Le(p,1 + i)
    Exact native replay linehave hple : exists k. k + p = 1 + i
  62. 0062specialize divisor_le_nonzero p
  63. 0063specialize divisor_le_nonzero (1 + i)
  64. 0064apply divisor_le_nonzero
  65. 0065exact hbounds_left
  66. 0066exact hfactor_right
  67. 0067specialize lt_not_le (1 + i)
  68. 0068specialize lt_not_le p
  69. 0069apply lt_not_le
  70. 0070exact hbounds_right
  71. 0071exact hple
  72. 0072have hdecomp : a * (1 + i) = x * p + x1
  73. 0073trans p * x + x1
  74. 0074exact hdiv_witness_witness_left
  75. 0075congr
  76. 0076apply mul_comm
  77. 0077refl
  78. 0078specialize gauss_pointwise_signed_half_choice p
  79. 0079specialize gauss_pointwise_signed_half_choice h
  80. 0080specialize gauss_pointwise_signed_half_choice a
  81. 0081specialize gauss_pointwise_signed_half_choice b
  82. 0082specialize gauss_pointwise_signed_half_choice c
  83. 0083specialize gauss_pointwise_signed_half_choice i
  84. 0084specialize gauss_pointwise_signed_half_choice (1 + i)
  85. 0085specialize gauss_pointwise_signed_half_choice x
  86. 0086specialize gauss_pointwise_signed_half_choice x1
  87. 0087apply gauss_pointwise_signed_half_choice
  88. 0088exact hp
  89. 0089exact hsource
  90. 0090exact hdecomp
  91. 0091exact hdiv_witness_witness_right
  92. 0092exact hrem0