PA00C2

odd_half_strictly_below_modulus

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

The half of an odd modulus p=2h+1 is strictly below p.

Exact expanded PA statement

forall p h. p = 2 * h + 1 -> (exists frp_gap_magnitude_half_below. frp_gap_magnitude_half_below + S h = p)

Structural proof guide

Generated structural guide

The half of an odd modulus p=2h+1 is strictly below p.

Use the direct prerequisites mul_succ_left, mul_zero_left, zero_add, add_succ_left, add_assoc as previously established PA formulas.

The proof proceeds by equality transport (1), certified simplification (1).

Referenced ingredients

PA000G mul_succ_left PA000D mul_zero_left PA0001 zero_add PA000E add_succ_left PA0009 add_assoc

Proof neighborhood

Direct dependencies

PA000G mul_succ_left PA000D mul_zero_left PA0001 zero_add PA000E add_succ_left PA0009 add_assoc

Direct dependents

PA00C6 odd_signed_division_branch_exact PA00D8 distinct_odd_prime_half_products_ne PA00DP distinct_primes_own_odd_half_scaled_remainder_nonzero

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 hp
  4. 0004exists h
  5. 0005rewrite hp
  6. 0006simp [mul_succ_left, mul_zero_left, zero_add, add_succ_left, add_assoc]