A_of_theta
plain-language theorem explainer
The kernel action is defined as the negative logarithm of the sine of the sensor angle θ. Analysts of recognition budgets cite this to compute minimal angles and show divergence at small scales. It is supplied as a direct definition that composes immediately with classical results on the logarithm and sine functions.
Claim. The kernel action is given by $A(θ) := -log(sin θ)$ for real $θ$.
background
The Recognition Angle module defines objects for analyzing sensor angles in three-dimensional Euclidean space. R3 is an alias for Euclidean 3-space. The angleAt function computes the geometric angle at one point between directions to two others, defaulting to zero on degeneracies. The kernel action is introduced as $A(θ) = -log(sin θ)$, which measures the information cost of angle θ. The threshold for a budget Amax is arcsin of exp(−Amax).
proof idea
The declaration is a direct definition that negates the real logarithm of the sine of the input angle. No additional lemmas or tactics are invoked beyond the standard library functions for real numbers.
why it matters
This definition anchors the recognition-angle program by supplying the explicit kernel action used in limit and threshold results. Downstream theorems establish divergence of the action as θ tends to zero and the budget-dependent minimal angle. It supports the information thermodynamics framework by quantifying costs that align with the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.