BT00R6

floor_sqrt_lower_bound

Alpha body-checked · checked-use disabled

The floor-square graph projects its lower 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 * s = x

Structural proof guide

The floor-square graph projects its lower square bound.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

BT010D floor_sqrt_three_mul_le_double

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_left