module module high

`IndisputableMonolith.Measurement.RecognitionAngle.AngleFunctionalEquation`

The module supplies the functional equation for the recognition angle by diagonalizing the ODE f'' = -f via characteristic roots ±i and the real energy invariant. Researchers proving T5 J-uniqueness cite these results when handling oscillatory components of the cost functional. The structure uses direct differentiation for the complex form together with conservation of E = f² + (f')².

claimThe ODE $f'' + f = 0$ has characteristic equation $r^2 + 1 = 0$ with roots $\pm i$; the real energy $E = f^2 + (f')^2$ is conserved, and the complex form satisfies $(f' - i f)' = -i(f' - i f)$.

background

The module resides in the Measurement domain and imports functional-equation helpers from IndisputableMonolith.Cost.FunctionalEquation, whose doc-comment states it supplies lemmas for the T5 cost uniqueness proof. It introduces the second-order linear ODE f'' = -f together with its complex diagonalization and the energy method that keeps E = f² + (f')² constant. Standard Mathlib calculus and trigonometric libraries supply the derivative and mean-value tools.

proof idea

The module structures its argument through a collection of lemmas: energy constancy via direct differentiation, zero-solution uniqueness under initial conditions, and verification that cosine satisfies the ODE plus regularity hypotheses. It applies Mathlib's deriv and trig identities without further scaffolding.

why it matters in Recognition Science

The module feeds the T5 cost-uniqueness argument by furnishing the angle functional equation that complements the imported Cost.FunctionalEquation lemmas. It supplies the oscillatory component required for the J-uniqueness step in the forcing chain.

scope and limits

Does not prove the full T5 J-uniqueness theorem.
Does not treat the ODE f'' = +f or other signs.
Does not include boundary-value problems beyond initial conditions.
Does not supply numerical or physical interpretations.

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