pith. sign in
theorem

ode_cosine_case

proved
show as:
module
IndisputableMonolith.Foundation.AxiomDischargePlan
domain
Foundation
line
152 · github
papers citing
1 paper (below)

plain-language theorem explainer

The cosine case theorem shows that any C² function H satisfying the initial-value problem H(0) = 1, H'(0) = 0 and H''(x) + β² H(x) = 0 for β > 0 coincides with the cosine function of frequency β. It is invoked during the case analysis that discharges the classical Aczél–Kannappan axiom in the Recognition Science foundation module. The argument reduces the general β to the unit case by the substitution H_β(t) := H(t/β) and applies the already-proved unit-frequency uniqueness result.

Claim. Let $H : ℝ → ℝ$ be twice continuously differentiable with $H(0) = 1$, $H'(0) = 0$, and $H''(x) = -β² H(x)$ for all $x ∈ ℝ$ where $β > 0$. Then $H(x) = cos(β x)$ for all $x$.

background

In the AxiomDischargePlan module the classical input aczel_kannappan_continuous_dAlembert is reduced to three ODE cases: constant, cosine, and cosh. The cosh case is already settled by dAlembert_cosh_solution_aczel. The present theorem handles the oscillatory case. Here H denotes the shifted cost function H(x) = J(x) + 1, where J satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) and is related to the hyperbolic cosine via the change of variables that turns the multiplicative equation into the additive d'Alembert form.

proof idea

The proof defines the rescaled function H_β(t) := H(t/β). It verifies that H_β inherits C² regularity, satisfies H_β(0)=1 and (H_β)'(0)=0, and obeys the unit ODE (H_β)''(t) = -H_β(t) by direct differentiation and the chain rule together with the given second-derivative relation. The unit-frequency uniqueness theorem ode_cos_unit_uniqueness is then applied to H_β, after which the substitution t = βx recovers the claimed form for H.

why it matters

This result completes the cosine branch of the case analysis inside aczel_kannappan_via_cases, which in turn discharges the full continuous d'Alembert classification required by the Recognition Science axiom reduction. It sits downstream of the J-uniqueness (T5) and the eight-tick octave structure, ensuring that the only continuous solutions compatible with the Recognition Composition Law are the constant, cosine, and cosh families. No open scaffolding remains in this branch.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 1 of 1)