pith. sign in
module module moderate

IndisputableMonolith.Measurement.RecognitionAngle.ActionSmallAngle

show as:
view Lean formalization →

This module defines geometric primitives for small-angle recognition measurements in R3, including the unit direction map and action as a function of angle. It introduces the minimum angle threshold thetaMin together with divergence of action at small scales and infeasibility below that threshold. These objects support angular feasibility calculations. The module consists of definitions and basic specifications relying on imported classical analysis axioms.

claimIn $R^3$, let $dir(x,y)$ be the unit vector from $x$ to $y$ (zero on degeneracy). Define $A_of_theta$ as the action for angle $theta$, with $thetaMin$ the infimum angle such that $A(theta) < Amax$ for positive budget $Amax$; action diverges as $theta to 0$ and recognition is infeasible below $thetaMin$.

background

The module sits in the Measurement.RecognitionAngle domain and imports classical real-analysis and functional-equation results as axioms. It introduces R3 as Euclidean three-space, dir as the normalized direction map, angleAt for local angle extraction, and A_of_theta for the action-angle relation. The small-angle regime is captured by thetaMin, the divergence statement action_small_angle_diverges, and the range and infeasibility predicates theta_min_spec, theta_min_range, infeasible_below_thetaMin.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the angular primitives required by BlindCone, which defines the blind-cone set at a point x for a given action budget Amax and proves existence of a positive threshold angle under Amax>0. It also feeds TemporalGating, which abstracts the discrete sampling/gating windows (eight-tick) and defines a feasibility predicate combining the angular threshold with temporal admissibility.

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)