BT00R7

floor_sqrt_strict_upper_bound

Alpha body-checked · checked-use disabled

The floor-square graph projects its strict successor-square bound.

Exact expanded PA statement

forall x s. (((exists bcs_sqrt_lower_gap_projection. bcs_sqrt_lower_gap_projection + (s) * (s) = (x)) /\ exists bcs_sqrt_upper_gap_projection. bcs_sqrt_upper_gap_projection + S (x) = S (s) * S (s))) -> exists k. k + S x = S s * S s

Structural proof guide

The floor-square graph projects its strict successor-square bound.

Direct prerequisites: none. The authored body proceeds by case analysis (1).

Proof neighborhood

Direct dependencies

none

Direct dependents

BT00X4 bertrand_floor_power_product_le_h_from_total BT010B floor_sqrt_two_le_of_two_lt

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro x
  2. 0002intro s
  3. 0003intro h
  4. 0004cases h
  5. 0005exact h_right