Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Proof of `A bounded rounded ellipsoid search with answer-or-cut replies` (1st statement)

groundedproofs/Lax263307Proofs/RoundedOracleSearch.lean · lax-263307

What this proof establishes

thm✓Lax263307.RoundedOracleSearch (1st statement)

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Identify the stored center with the registered sequence. Its grid and magnitude bounds give a linear encoding bound independent of incoming normals.