module module high

`IndisputableMonolith.Measurement.RecognitionAngle.AngleFunctionalEquation`

The module develops the ODE theory for f'' = -f by diagonalizing into complex exponentials and proving energy conservation E = f² + (f')² is constant. It supports T5 cost uniqueness in Recognition Science by supplying the oscillatory analysis needed for the angle functional equation. Arguments proceed via energy differentiation, zero-uniqueness, and regularity bootstrap using imported calculus lemmas.

claimFor twice differentiable $f$ satisfying $f'' = -f$, the energy $E = f^2 + (f')^2$ is constant. Solutions are unique given initial values $f(0)$ and $f'(0)$, and admit the form $f(x) = A cos x + B sin x$ (or equivalent complex exponential diagonalization with roots $r = ±i$).

background

The module sits in Measurement.RecognitionAngle and imports Mathlib calculus (Deriv, MeanValue, Trigonometric) plus the Cost.FunctionalEquation module. The upstream module supplies lemmas for the T5 cost uniqueness proof. It treats the negative-energy case of the second-order linear ODE, using the energy method noted in the doc-comment: if f'' = -f then (f' - i f)' = -i (f' - i f), with real form E constant.

proof idea

The module organizes its content as a chain of lemmas: ode_neg_energy_constant establishes E constancy by direct differentiation; ode_zero_uniqueness_neg and ode_cos_uniqueness prove uniqueness from initial data; cos_satisfies_* lemmas verify that cosine meets the ODE and regularity hypotheses; bootstrap and differentiability steps close the regularity argument using mean-value and derivative rules from Mathlib.

why it matters in Recognition Science

The module supplies the ODE infrastructure required for the angle functional equation that feeds T5 J-uniqueness in the forcing chain. It closes the oscillatory component of the cost functional setup, enabling the transition from the Recognition Composition Law to the phi-ladder mass formula. No direct downstream declarations are listed, but the sibling lemmas are positioned to support higher RecognitionAngle results.

scope and limits

Does not treat the positive-energy ODE f'' = +f.
Does not derive the J-cost function or phi-ladder directly.
Does not address boundary conditions beyond initial-value uniqueness.
Does not connect to spatial dimension D = 3 or the alpha band.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.FunctionalEquation module_import

declarations in this module (23)

theorem ode_neg_energy_constant L62
theorem ode_zero_uniqueness_neg L102
theorem cos_second_deriv_eq L118
theorem cos_initials L130
theorem ode_cos_uniqueness_contdiff L137
def ode_linear_regularity_bootstrap_hypothesis_neg L191
def ode_regularity_continuous_hypothesis_neg L195
def ode_regularity_differentiable_hypothesis_neg L199
theorem cos_satisfies_bootstrap_neg L203
theorem cos_satisfies_continuous_neg L208
theorem cos_satisfies_differentiable_neg L213
theorem ode_cos_uniqueness L218
def dAlembert_continuous_implies_smooth_hypothesis_neg L242
def dAlembert_to_ODE_hypothesis_neg L249
theorem cos_dAlembert_smooth L254
theorem cos_dAlembert_to_ODE L259
theorem cos_dAlembert L264
theorem dAlembert_cos_solution L275
structure AngleCouplingAxioms L312
structure AngleStandardRegularity L325
theorem THEOREM_angle_coupling_rigidity L338
theorem cos_satisfies_axioms L355
theorem cos_satisfies_regularity L365