pith. sign in
module module high

IndisputableMonolith.Cost.ClassicalResults

show as:
view Lean formalization →

This module supplies provable classical results for cost calculations equipped with integrability hypotheses to guarantee convergence of all integrals. Researchers working on the recognition-angle program cite it when rigorizing geometric action bounds. The module consists of independent lemmas that apply standard Mathlib facts on real analysis, spherical measures, and exponential identities rather than a single overarching argument.

claimThe module establishes results such as positivity of spherical-cap integrals $I = 0$ for $f > 0$, rearrangement identities $e^{a+b} = e^a e^b$ under integrability, additivity of piecewise path integrals, and bounds derived from $A_0 = -log(sin θ)$ together with $θ_{min} = arcsin(e^{-A_{max}})$.

background

The Cost.ClassicalResults module supplies auxiliary analytic facts required by the recognition-angle program. It works in Euclidean R^3 with the standard surface measure on the unit sphere and assumes the integrability conditions needed to interchange limits and integrals. Key objects proved here include spherical_cap_pos (strict positivity of the measure of a spherical cap), exp_mul_rearrange (multiplicative rearrangement of exponentials), piecewise_path_integral_additive_integrable (additivity of path integrals when the integrand is integrable), and complex_norm_exp_ofReal together with complex_norm_exp_I_mul (norm identities for complex exponentials). These facts are imported directly into the downstream RecognitionAngle module.

proof idea

The module is a library of targeted lemmas rather than a single theorem. Each lemma applies Mathlib tactics for continuity, positivity preservation under integration, and algebraic rearrangement of exponentials. spherical_cap_pos uses the fact that the spherical measure is positive on open sets; exp_mul_rearrange and complex_norm_exp_* rely on the functional equation of the exponential; piecewise_path_integral_additive_integrable invokes the additivity property of the Lebesgue integral under the stated integrability hypothesis. No tactic script is shared across lemmas.

why it matters in Recognition Science

The module feeds the core definitions in IndisputableMonolith.Measurement.RecognitionAngle.ActionSmallAngle, which introduces R3, angleAt x y z, A_of_theta θ := -log(sin θ), and thetaMin Amax := arcsin(exp(-Amax)). By supplying the provable classical results with integrability hypotheses, it closes the gap between geometric intuition and Lean-verified statements needed for small-angle action bounds in the recognition framework.

scope and limits

used by (1)

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

declarations in this module (11)