IndisputableMonolith.Cost.ClassicalResults
Cost.ClassicalResults assembles provable lemmas on integrals, exponentials, and spherical caps under explicit integrability hypotheses. Researchers modeling small-angle actions in Recognition Science cite these to justify manipulations in cost calculations. The module structure consists of independent results proved via Mathlib analysis tactics and feeds directly into the recognition angle definitions.
claimCollection of classical results with integrability: positivity of spherical cap measure $\mu(C)>0$, rearrangement $\exp(\mu+\nu)=\exp\mu\,\exp\nu$, additivity of piecewise path integrals, real cosh exponential expansion, complex exponential norms, and spherical cap measure bounds.
background
The Cost domain supplies auxiliary results for J-cost and defect distance calculations. This module imports Mathlib and states each lemma with integrability hypotheses to ensure they are provable. It supplies the classical analysis needed for action integrals.
The downstream module ActionSmallAngle defines R3 as 3D Euclidean space, angleAt x y z as the geometric angle at x between directions to y and z, A_of_theta θ := -log(sin θ) as the kernel action, and thetaMin Amax := arcsin(exp(-Amax)) as the budget-dependent minimal angle.
proof idea
The module contains independent lemmas. Each applies standard Mathlib tactics for real analysis, complex numbers, and integration; no single overarching proof or term-mode reduction.
why it matters in Recognition Science
This module feeds the RecognitionAngle.ActionSmallAngle module, which introduces the core objects for the recognition angle program. It supplies the provable classical results with integrability hypotheses required for rigorous integral handling in small-angle cost computations.
scope and limits
- Does not establish results without integrability hypotheses.
- Does not address quantum or non-classical extensions.
- Does not define recognition angles or action kernels.
- Does not include numerical evaluations or simulations.
used by (1)
declarations in this module (11)
-
lemma
spherical_cap_pos -
lemma
exp_mul_rearrange -
theorem
piecewise_path_integral_additive_integrable -
theorem
real_cosh_exponential_expansion -
theorem
complex_norm_exp_ofReal -
theorem
complex_norm_exp_I_mul -
theorem
neg_log_sin_tendsto_atTop_at_zero_right -
theorem
theta_min_spec_inequality -
theorem
theta_min_range -
theorem
spherical_cap_measure_bounds -
theorem
complex_exp_mul_rearrange