pith. sign in
module module high

IndisputableMonolith.Measurement.RecognitionAngle.BlindCone

show as:
view Lean formalization →

This module defines the blind cone at a point x with action budget Amax as the set of pairs (y,z) whose separation angle at x is below the minimal recognizable threshold thetaMin(Amax). Researchers working on angular resolution in Recognition Science cite it when bounding unresolvable directions under finite action. The module is purely definitional and imports its core objects directly from the ActionSmallAngle module.

claimFor $x,y,z$ in $R^3$ and budget $Amax$, the blind cone is the set of pairs $(y,z)$ such that the angle at $x$ satisfies $angleAt(x,y,z) < thetaMin(Amax)$, where $thetaMin(A) := arcsin(exp(-A))$ and $A_of_theta(theta) := -log(sin theta)$.

background

The module sits inside the Measurement.RecognitionAngle program and imports the core objects defined in ActionSmallAngle. That upstream module supplies R3 as a convenient alias for three-dimensional Euclidean space, the function angleAt x y z giving the geometric angle at x between directions to y and z, the kernel action A_of_theta theta = -log(sin theta), and the budget-dependent minimal angle thetaMin Amax = arcsin(exp(-Amax)). These objects encode the Recognition Science relation between action cost and angular resolution: smaller angles require exponentially larger action.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the central geometric object for the recognition-angle program, directly feeding the sibling declarations blindCone, blind_cone_exists and theta_min_le_pi_half. It closes the definitional step that converts the action budget Amax into an explicit angular exclusion region, enabling later theorems that bound measurement precision under the Recognition Composition Law and the phi-ladder mass formulas.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)