PA00CP

gauss_eisenstein_prefix_pointwise_mod_two

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

Aligned Gauss and Eisenstein prefixes satisfy x == q+m+s modulo two pointwise.

Exact expanded PA statement

forall p h a b c tb tc qb qc rb rc mb mc sb sc. p = 2 * h + 1 -> (exists sdp_odd_gep_scale. a = 2 * sdp_odd_gep_scale + 1) -> (forall gsp_range_index_gep_half. (exists gsp_lt_gap_gep_half_range_bound. gsp_lt_gap_gep_half_range_bound + S gsp_range_index_gep_half = h) -> (((exists gsp_beta_height_gep_half_range_entry. gsp_beta_height_gep_half_range_entry + S (1 + gsp_range_index_gep_half) = S ((S (gsp_range_index_gep_half)) * c)) /\ exists gsp_beta_quotient_gep_half_range_entry. b = gsp_beta_quotient_gep_half_range_entry * S ((S (gsp_range_index_gep_half)) * c) + (1 + gsp_range_index_gep_half)))) -> (forall esd_index_gep_scaled esd_value_gep_scaled. (exists esd_gap_gep_scaled. esd_gap_gep_scaled + S esd_index_gep_scaled = h) -> (((exists ff_h_esd_gep_scaled_decoded. ff_h_esd_gep_scaled_decoded + S (esd_value_gep_scaled) = S ((S (esd_index_gep_scaled)) * tc)) /\ exists ff_q_esd_gep_scaled_decoded. tb = ff_q_esd_gep_scaled_decoded * S ((S (esd_index_gep_scaled)) * tc) + (esd_value_gep_scaled))) -> esd_value_gep_scaled = a * (1 + esd_index_gep_scaled)) -> (forall fdp_index_gep_division. (exists gsp_lt_gap_gep_division_index_bound. gsp_lt_gap_gep_division_index_bound + S fdp_index_gep_division = h) -> exists fdp_value_gep_division fdp_quotient_gep_division fdp_remainder_gep_division. (((exists ff_h_fdp_gep_division_source. ff_h_fdp_gep_division_source + S (fdp_value_gep_division) = S ((S (fdp_index_gep_division)) * tc)) /\ exists ff_q_fdp_gep_division_source. tb = ff_q_fdp_gep_division_source * S ((S (fdp_index_gep_division)) * tc) + (fdp_value_gep_division))) /\ ((((exists ff_h_fdp_gep_division_quotient_entry. ff_h_fdp_gep_division_quotient_entry + S (fdp_quotient_gep_division) = S ((S (fdp_index_gep_division)) * qc)) /\ exists ff_q_fdp_gep_division_quotient_entry. qb = ff_q_fdp_gep_division_quotient_entry * S ((S (fdp_index_gep_division)) * qc) + (fdp_quotient_gep_division))) /\ ((((exists ff_h_fdp_gep_division_remainder_entry. ff_h_fdp_gep_division_remainder_entry + S (fdp_remainder_gep_division) = S ((S (fdp_index_gep_division)) * rc)) /\ exists ff_q_fdp_gep_division_remainder_entry. rb = ff_q_fdp_gep_division_remainder_entry * S ((S (fdp_index_gep_division)) * rc) + (fdp_remainder_gep_division))) /\ (fdp_value_gep_division = p * fdp_quotient_gep_division + fdp_remainder_gep_division /\ (exists gsp_lt_gap_gep_division_remainder_bound. gsp_lt_gap_gep_division_remainder_bound + S fdp_remainder_gep_division = p))))) -> (forall gsp_index_gep_signed. (exists gsp_lt_gap_gep_signed_index_bound. gsp_lt_gap_gep_signed_index_bound + S gsp_index_gep_signed = h) -> (exists gsp_value_gep_signed_entry gsp_magnitude_gep_signed_entry gsp_sign_gep_signed_entry. (((exists ff_h_gsp_gep_signed_entry_source. ff_h_gsp_gep_signed_entry_source + S (gsp_value_gep_signed_entry) = S ((S (gsp_index_gep_signed)) * c)) /\ exists ff_q_gsp_gep_signed_entry_source. b = ff_q_gsp_gep_signed_entry_source * S ((S (gsp_index_gep_signed)) * c) + (gsp_value_gep_signed_entry))) /\ ((((exists ff_h_gsp_gep_signed_entry_magnitude. ff_h_gsp_gep_signed_entry_magnitude + S (gsp_magnitude_gep_signed_entry) = S ((S (gsp_index_gep_signed)) * mc)) /\ exists ff_q_gsp_gep_signed_entry_magnitude. mb = ff_q_gsp_gep_signed_entry_magnitude * S ((S (gsp_index_gep_signed)) * mc) + (gsp_magnitude_gep_signed_entry))) /\ ((((exists ff_h_gsp_gep_signed_entry_sign. ff_h_gsp_gep_signed_entry_sign + S (gsp_sign_gep_signed_entry) = S ((S (gsp_index_gep_signed)) * sc)) /\ exists ff_q_gsp_gep_signed_entry_sign. sb = ff_q_gsp_gep_signed_entry_sign * S ((S (gsp_index_gep_signed)) * sc) + (gsp_sign_gep_signed_entry))) /\ ((exists gsp_lt_gap_gep_signed_entry_positive. gsp_lt_gap_gep_signed_entry_positive + S 0 = gsp_magnitude_gep_signed_entry) /\ ((exists gsp_le_gap_gep_signed_entry_bounded. gsp_le_gap_gep_signed_entry_bounded + gsp_magnitude_gep_signed_entry = h) /\ ((gsp_sign_gep_signed_entry = 0 \/ gsp_sign_gep_signed_entry = 1) /\ (((gsp_sign_gep_signed_entry = 0 /\ (exists gsp_mod_left_gep_signed_entry_lower gsp_mod_right_gep_signed_entry_lower. (a * gsp_value_gep_signed_entry) + p * gsp_mod_left_gep_signed_entry_lower = (gsp_magnitude_gep_signed_entry) + p * gsp_mod_right_gep_signed_entry_lower)) \/ (gsp_sign_gep_signed_entry = 1 /\ (exists gsp_mod_left_gep_signed_entry_reflected gsp_mod_right_gep_signed_entry_reflected. (a * gsp_value_gep_signed_entry) + p * gsp_mod_left_gep_signed_entry_reflected = ((2 * h) * gsp_magnitude_gep_signed_entry) + p * gsp_mod_right_gep_signed_entry_reflected))))))))))) -> (forall i x q m s. (exists gsp_lt_gap_gep_index. gsp_lt_gap_gep_index + S i = h) -> (((exists ff_h_gep_source_entry. ff_h_gep_source_entry + S (x) = S ((S (i)) * c)) /\ exists ff_q_gep_source_entry. b = ff_q_gep_source_entry * S ((S (i)) * c) + (x))) -> (((exists ff_h_gep_quotient_entry. ff_h_gep_quotient_entry + S (q) = S ((S (i)) * qc)) /\ exists ff_q_gep_quotient_entry. qb = ff_q_gep_quotient_entry * S ((S (i)) * qc) + (q))) -> (((exists ff_h_gep_magnitude_entry. ff_h_gep_magnitude_entry + S (m) = S ((S (i)) * mc)) /\ exists ff_q_gep_magnitude_entry. mb = ff_q_gep_magnitude_entry * S ((S (i)) * mc) + (m))) -> (((exists ff_h_gep_sign_entry. ff_h_gep_sign_entry + S (s) = S ((S (i)) * sc)) /\ exists ff_q_gep_sign_entry. sb = ff_q_gep_sign_entry * S ((S (i)) * sc) + (s))) -> (exists sdp_u_gep_prefix_result sdp_v_gep_prefix_result. (x) + 2 * sdp_u_gep_prefix_result = (q + m + s) + 2 * sdp_v_gep_prefix_result))

Structural proof guide

Generated structural guide

Aligned Gauss and Eisenstein prefixes satisfy x == q+m+s modulo two pointwise.

Use the direct prerequisites beta_at_unique, odd_signed_division_congruence_mod_two as previously established PA formulas.

The proof proceeds by case analysis (19), intermediate claims (12), equality transport (6).

Referenced ingredients

PA002F beta_at_unique PA00CO odd_signed_division_congruence_mod_two

Proof neighborhood

Direct dependencies

PA002F beta_at_unique PA00CO odd_signed_division_congruence_mod_two

Direct dependents

PA00CR gauss_eisenstein_terminal_sums_mod_two

Formal native tactic body

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

  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro tb
  7. 0007intro tc
  8. 0008intro qb
  9. 0009intro qc
  10. 0010intro rb
  11. 0011intro rc
  12. 0012intro mb
  13. 0013intro mc
  14. 0014intro sb
  15. 0015intro sc
  16. 0016intro hp
  17. 0017intro ha
  18. 0018intro hhalf
  19. 0019intro hscaled
  20. 0020intro hdivision
  21. 0021intro hsigned
  22. 0022intro i
  23. 0023intro x
  24. 0024intro q
  25. 0025intro m
  26. 0026intro s
  27. 0027intro hi
  28. 0028intro hx
  29. 0029intro hq
  30. 0030intro hm
  31. 0031intro hs
  32. 0032have hcanonical : ((exists gsp_beta_height_gep_proof_canonical. gsp_beta_height_gep_proof_canonical + S (1 + i) = S ((S (i)) * c)) /\ exists gsp_beta_quotient_gep_proof_canonical. b = gsp_beta_quotient_gep_proof_canonical * S ((S (i)) * c) + (1 + i))
  33. 0033specialize hhalf i
  34. 0034apply hhalf
  35. 0035exact hi
  36. 0036have hdivdata : exists x1 x2 x3. (((exists ff_h_gep_proof_div_source. ff_h_gep_proof_div_source + S (x1) = S ((S (i)) * tc)) /\ exists ff_q_gep_proof_div_source. tb = ff_q_gep_proof_div_source * S ((S (i)) * tc) + (x1))) /\ ((((exists ff_h_gep_proof_div_q. ff_h_gep_proof_div_q + S (x2) = S ((S (i)) * qc)) /\ exists ff_q_gep_proof_div_q. qb = ff_q_gep_proof_div_q * S ((S (i)) * qc) + (x2))) /\ ((((exists ff_h_gep_proof_div_r. ff_h_gep_proof_div_r + S (x3) = S ((S (i)) * rc)) /\ exists ff_q_gep_proof_div_r. rb = ff_q_gep_proof_div_r * S ((S (i)) * rc) + (x3))) /\ (x1 = p * x2 + x3 /\ (exists gsp_lt_gap_gep_proof_div_r_below. gsp_lt_gap_gep_proof_div_r_below + S x3 = p))))
  37. 0037specialize hdivision i
  38. 0038apply hdivision
  39. 0039exact hi
  40. 0040cases hdivdata
  41. 0041cases hdivdata_witness
  42. 0042cases hdivdata_witness_witness
  43. 0043cases hdivdata_witness_witness_witness
  44. 0044cases hdivdata_witness_witness_witness_right
  45. 0045cases hdivdata_witness_witness_witness_right_right
  46. 0046cases hdivdata_witness_witness_witness_right_right_right
  47. 0047have hsigneddata : exists x4 x5 x6. (((exists ff_h_gep_proof_signed_source. ff_h_gep_proof_signed_source + S (x4) = S ((S (i)) * c)) /\ exists ff_q_gep_proof_signed_source. b = ff_q_gep_proof_signed_source * S ((S (i)) * c) + (x4))) /\ ((((exists ff_h_gep_proof_signed_magnitude. ff_h_gep_proof_signed_magnitude + S (x5) = S ((S (i)) * mc)) /\ exists ff_q_gep_proof_signed_magnitude. mb = ff_q_gep_proof_signed_magnitude * S ((S (i)) * mc) + (x5))) /\ ((((exists ff_h_gep_proof_signed_sign. ff_h_gep_proof_signed_sign + S (x6) = S ((S (i)) * sc)) /\ exists ff_q_gep_proof_signed_sign. sb = ff_q_gep_proof_signed_sign * S ((S (i)) * sc) + (x6))) /\ ((exists gsp_lt_gap_gep_proof_signed_positive. gsp_lt_gap_gep_proof_signed_positive + S 0 = x5) /\ ((exists gsp_le_gap_gep_proof_signed_bounded. gsp_le_gap_gep_proof_signed_bounded + x5 = h) /\ ((x6 = 0 \/ x6 = 1) /\ (((x6 = 0 /\ (exists wpp_mod_left_gep_proof_signed_lower wpp_mod_right_gep_proof_signed_lower. (a * x4) + p * wpp_mod_left_gep_proof_signed_lower = (x5) + p * wpp_mod_right_gep_proof_signed_lower)) \/ (x6 = 1 /\ (exists wpp_mod_left_gep_proof_signed_upper wpp_mod_right_gep_proof_signed_upper. (a * x4) + p * wpp_mod_left_gep_proof_signed_upper = ((2 * h) * x5) + p * wpp_mod_right_gep_proof_signed_upper)))))))))
  48. 0048specialize hsigned i
  49. 0049apply hsigned
  50. 0050exact hi
  51. 0051cases hsigneddata
  52. 0052cases hsigneddata_witness
  53. 0053cases hsigneddata_witness_witness
  54. 0054cases hsigneddata_witness_witness_witness
  55. 0055cases hsigneddata_witness_witness_witness_right
  56. 0056cases hsigneddata_witness_witness_witness_right_right
  57. 0057cases hsigneddata_witness_witness_witness_right_right_right
  58. 0058cases hsigneddata_witness_witness_witness_right_right_right_right
  59. 0059cases hsigneddata_witness_witness_witness_right_right_right_right_right
  60. 0060have hxcanonical : x4 = 1 + i
  61. 0061specialize beta_at_unique b
  62. 0062specialize beta_at_unique c
  63. 0063specialize beta_at_unique i
  64. 0064specialize beta_at_unique x4
  65. 0065specialize beta_at_unique (1 + i)
  66. 0066apply beta_at_unique
  67. 0067exact hsigneddata_witness_witness_witness_left
  68. 0068exact hcanonical
  69. 0069have hnscale : x1 = a * x4
  70. 0070have hscale_exact : forall esd_index_gep_proof_scaled esd_value_gep_proof_scaled. (exists esd_gap_gep_proof_scaled. esd_gap_gep_proof_scaled + S esd_index_gep_proof_scaled = h) -> (((exists ff_h_esd_gep_proof_scaled_decoded. ff_h_esd_gep_proof_scaled_decoded + S (esd_value_gep_proof_scaled) = S ((S (esd_index_gep_proof_scaled)) * tc)) /\ exists ff_q_esd_gep_proof_scaled_decoded. tb = ff_q_esd_gep_proof_scaled_decoded * S ((S (esd_index_gep_proof_scaled)) * tc) + (esd_value_gep_proof_scaled))) -> esd_value_gep_proof_scaled = a * (1 + esd_index_gep_proof_scaled)
  71. 0071exact hscaled
  72. 0072trans a * (1 + i)
  73. 0073specialize hscale_exact i
  74. 0074specialize hscale_exact x1
  75. 0075apply hscale_exact
  76. 0076exact hi
  77. 0077exact hdivdata_witness_witness_witness_left
  78. 0078congr
  79. 0079refl
  80. 0080symm
  81. 0081exact hxcanonical
  82. 0082have hsignedn : ((x6 = 0 /\ (exists wpp_mod_left_gep_proof_n_mod_m wpp_mod_right_gep_proof_n_mod_m. (x1) + p * wpp_mod_left_gep_proof_n_mod_m = (x5) + p * wpp_mod_right_gep_proof_n_mod_m)) \/ (x6 = 1 /\ (exists wpp_mod_left_gep_proof_n_mod_upper wpp_mod_right_gep_proof_n_mod_upper. (x1) + p * wpp_mod_left_gep_proof_n_mod_upper = ((2 * h) * x5) + p * wpp_mod_right_gep_proof_n_mod_upper)))
  83. 0083cases hsigneddata_witness_witness_witness_right_right_right_right_right_right
  84. 0084left
  85. 0085cases hsigneddata_witness_witness_witness_right_right_right_right_right_right_left
  86. 0086split
  87. 0087exact hsigneddata_witness_witness_witness_right_right_right_right_right_right_left_left
  88. 0088rewrite hnscale
  89. 0089exact hsigneddata_witness_witness_witness_right_right_right_right_right_right_left_right
  90. 0090right
  91. 0091cases hsigneddata_witness_witness_witness_right_right_right_right_right_right_right
  92. 0092split
  93. 0093exact hsigneddata_witness_witness_witness_right_right_right_right_right_right_right_left
  94. 0094rewrite hnscale
  95. 0095exact hsigneddata_witness_witness_witness_right_right_right_right_right_right_right_right
  96. 0096have hlocal : exists sdp_u_gep_proof_final sdp_v_gep_proof_final. (x4) + 2 * sdp_u_gep_proof_final = (x2 + x5 + x6) + 2 * sdp_v_gep_proof_final
  97. 0097specialize odd_signed_division_congruence_mod_two p
  98. 0098specialize odd_signed_division_congruence_mod_two h
  99. 0099specialize odd_signed_division_congruence_mod_two a
  100. 0100specialize odd_signed_division_congruence_mod_two x4
  101. 0101specialize odd_signed_division_congruence_mod_two x1
  102. 0102specialize odd_signed_division_congruence_mod_two x2
  103. 0103specialize odd_signed_division_congruence_mod_two x3
  104. 0104specialize odd_signed_division_congruence_mod_two x5
  105. 0105specialize odd_signed_division_congruence_mod_two x6
  106. 0106apply odd_signed_division_congruence_mod_two
  107. 0107exact hp
  108. 0108exact ha
  109. 0109exact hnscale
  110. 0110exact hdivdata_witness_witness_witness_right_right_right_left
  111. 0111exact hdivdata_witness_witness_witness_right_right_right_right
  112. 0112exact hsigneddata_witness_witness_witness_right_right_right_left
  113. 0113exact hsigneddata_witness_witness_witness_right_right_right_right_left
  114. 0114exact hsignedn
  115. 0115have hxeq : x = x4
  116. 0116specialize beta_at_unique b
  117. 0117specialize beta_at_unique c
  118. 0118specialize beta_at_unique i
  119. 0119specialize beta_at_unique x
  120. 0120specialize beta_at_unique x4
  121. 0121apply beta_at_unique
  122. 0122exact hx
  123. 0123exact hsigneddata_witness_witness_witness_left
  124. 0124have hqeq : q = x2
  125. 0125specialize beta_at_unique qb
  126. 0126specialize beta_at_unique qc
  127. 0127specialize beta_at_unique i
  128. 0128specialize beta_at_unique q
  129. 0129specialize beta_at_unique x2
  130. 0130apply beta_at_unique
  131. 0131exact hq
  132. 0132exact hdivdata_witness_witness_witness_right_left
  133. 0133have hmeq : m = x5
  134. 0134specialize beta_at_unique mb
  135. 0135specialize beta_at_unique mc
  136. 0136specialize beta_at_unique i
  137. 0137specialize beta_at_unique m
  138. 0138specialize beta_at_unique x5
  139. 0139apply beta_at_unique
  140. 0140exact hm
  141. 0141exact hsigneddata_witness_witness_witness_right_left
  142. 0142have hseq : s = x6
  143. 0143specialize beta_at_unique sb
  144. 0144specialize beta_at_unique sc
  145. 0145specialize beta_at_unique i
  146. 0146specialize beta_at_unique s
  147. 0147specialize beta_at_unique x6
  148. 0148apply beta_at_unique
  149. 0149exact hs
  150. 0150exact hsigneddata_witness_witness_witness_right_right_left
  151. 0151rewrite hxeq
  152. 0152rewrite hqeq
  153. 0153rewrite hmeq
  154. 0154rewrite hseq
  155. 0155exact hlocal