PA00DQ

odd_half_cross_product_gap

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

The odd half-products differ by the explicit positive gap h+k+1.

Exact expanded PA statement

forall h k. (exists edt_lt_gap_odd_half_cross_gap. edt_lt_gap_odd_half_cross_gap + S ((2 * k + 1) * h) = (2 * h + 1) * S k)

Structural proof guide

Generated structural guide

The odd half-products differ by the explicit positive gap h+k+1.

Use the direct prerequisites mul_add, add_mul, mul_assoc, mul_comm, add_assoc, add_comm, one_mul, mul_one, mul_succ_left as previously established PA formulas.

The proof proceeds by certified simplification (1).

Referenced ingredients

PA000A mul_add PA0016 add_mul PA000B mul_assoc PA000H mul_comm PA0009 add_assoc PA000F add_comm PA000M one_mul PA0002 mul_one PA000G mul_succ_left

Proof neighborhood

Direct dependencies

PA000A mul_add PA0016 add_mul PA000B mul_assoc PA000H mul_comm PA0009 add_assoc PA000F add_comm PA000M one_mul PA0002 mul_one PA000G mul_succ_left

Direct dependents

PA00DR odd_half_division_quotient_bounded

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 h
  2. 0002intro k
  3. 0003exists h + k
  4. 0004simp [mul_add, add_mul, mul_assoc, mul_comm, add_assoc, add_comm, one_mul, mul_one, mul_succ_left]
  5. 0005congr
  6. 0006trans (h + k) + (h + (k * h + k * h))
  7. 0007symm
  8. 0008apply add_assoc
  9. 0009trans (k + h) + (h + (k * h + k * h))
  10. 0010congr
  11. 0011apply add_comm
  12. 0012refl
  13. 0013apply add_assoc