pith. sign in
theorem

ode_cos_unit_uniqueness

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

plain-language theorem explainer

The unit-frequency cosine uniqueness theorem states that any C² function f:ℝ→ℝ obeying f''(t)=-f(t) with f(0)=1 and f'(0)=0 must equal cos(t). Recognition Science researchers cite it when discharging the cosine branch of the Aczél–Kannappan classification inside the d'Alembert reduction. The proof subtracts the cosine function to produce a difference that satisfies the same ODE with zero initial data, then invokes the zero-uniqueness lemma.

Claim. Let $f:ℝ→ℝ$ be twice continuously differentiable. Suppose $f''(t)=-f(t)$ for all $t$, $f(0)=1$, and $f'(0)=0$. Then $f(t)=cos(t)$ for all $t$.

background

The AxiomDischargePlan module reduces the classical aczel_kannappan_continuous_dAlembert axiom to ODE uniqueness statements after the cosh case has already been settled by dAlembert_cosh_solution_aczel. The shifted cost H(x)=J(x)+1 converts the Recognition Composition Law into the d'Alembert equation H(xy)+H(x/y)=2H(x)H(y). The cosine case appears when the second derivative carries a negative sign, in contrast to the hyperbolic case already handled.

proof idea

Define g(t):=f(t)-cos(t). Verify that g remains C², satisfies g''=-g by direct computation of the second derivative using the known derivative of cosine, and meets g(0)=0 together with g'(0)=0. The claim follows at once by applying ode_neg_zero_uniqueness to g.

why it matters

This result supplies the unit-frequency input required by the downstream ode_cosine_case theorem, which rescales to obtain the general solution H(x)=cos(βx) for β>0. It completes the analytic discharge of the Aczél–Kannappan classification, allowing the full reduction of the continuous d'Alembert axiom to the existing cosh solution plus these ODE statements. In the Recognition framework it supports passage from the functional equation for H to concrete solutions that enter the phi-ladder and eight-tick octave structure.

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

papers checked against this theorem (showing 1 of 1)