PA00FH

gauss_count_sum_mod_two_from_quotient_sums

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

Two oriented count/quotient congruences plus the exact floor-sum identity give e+f == h*k modulo two.

Exact expanded PA statement

forall e f Q U h k. (exists gcsp_u_e_q gcsp_v_e_q. e + 2 * gcsp_u_e_q = Q + 2 * gcsp_v_e_q) -> (exists gcsp_u_f_u gcsp_v_f_u. f + 2 * gcsp_u_f_u = U + 2 * gcsp_v_f_u) -> Q + U = h * k -> (exists gcsp_u_sum_product gcsp_v_sum_product. e + f + 2 * gcsp_u_sum_product = h * k + 2 * gcsp_v_sum_product)

Structural proof guide

Generated structural guide

Two oriented count/quotient congruences plus the exact floor-sum identity give e+f == h*k modulo two.

Use the direct prerequisites mod_eq_add as previously established PA formulas.

The proof proceeds by intermediate claims (1), equality transport (1).

Referenced ingredients

PA0022 mod_eq_add

Proof neighborhood

Direct dependencies

PA0022 mod_eq_add

Direct dependents

PA00FP conditional_qres_same_status_from_oriented_gauss_counts PA00FV conditional_qres_opposite_status_from_oriented_gauss_counts

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 e
  2. 0002intro f
  3. 0003intro Q
  4. 0004intro U
  5. 0005intro h
  6. 0006intro k
  7. 0007intro heq
  8. 0008intro hfu
  9. 0009intro hsum
  10. 0010have hjoined : exists gcsp_u_sum_qu gcsp_v_sum_qu. e + f + 2 * gcsp_u_sum_qu = Q + U + 2 * gcsp_v_sum_qu
  11. 0011specialize mod_eq_add 2
  12. 0012specialize mod_eq_add e
  13. 0013specialize mod_eq_add Q
  14. 0014specialize mod_eq_add f
  15. 0015specialize mod_eq_add U
  16. 0016apply mod_eq_add
  17. 0017exact heq
  18. 0018exact hfu
  19. 0019rewrite hsum at hjoined
  20. 0020exact hjoined