pith. sign in
module module high

IndisputableMonolith.Measurement.RecognitionAngle.ActionSmallAngle

show as:
view Lean formalization →

This module defines the unit direction in R3, the angle function, small-angle action, and the minimal threshold angle with its range and divergence properties. It is imported by modules on blind cones and temporal gating to build recognition feasibility predicates. The module consists of definitions and basic lemmas on ranges and infeasibility, drawing on imported classical axioms.

claimIntroduces the unit direction function returning the normalized vector from $x$ to $y$ in $R^3$ (zero on degeneracy), the angle at a point, the action $A$ as a function of angle, and the minimal angle threshold with the properties that action diverges below the threshold and the threshold lies in a specified interval.

background

The module sits in the Measurement domain and imports classical mathematical results declared as axioms from real analysis and functional equations. It works in Euclidean three-space R3 to define directional quantities for recognition processes. The supplied doc-comment for the direction function states it returns the unit vector from x to y, zero on degeneracy. Downstream modules use these to define blind-cone sets for action budgets and eight-tick temporal windows.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Supplies the angular threshold and action divergence facts required by the blind-cone module (existence of positive threshold angle under Amax>0) and the temporal gating module (feasibility predicate combining angular threshold with temporal admissibility). It bridges the imported classical axioms to the recognition geometry used in the eight-tick octave and D=3 spatial setting.

scope and limits

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)