ode_cosh_status
plain-language theorem explainer
The unique solution to the ODE H'' = H with H(0) = 1 and H'(0) = 0 is the hyperbolic cosine. A researcher deriving the recognition cost from the functional equation would cite this standard ODE result. The declaration records the fact as a definition because uniqueness follows from the Picard-Lindelöf theorem on Lipschitz initial-value problems.
Claim. The unique solution to the differential equation $H'' = H$ with initial conditions $H(0) = 1$, $H'(0) = 0$ is $H(x) = 2^{-1}(e^x + e^{-x})$.
background
The module Meta.Axioms maintains an axiom registry that separates physical postulates from well-known mathematical facts accepted for pragmatic reasons. This entry labels the ODE uniqueness claim as a standard mathematical fact, cross-referenced to FunctionalEquation.lean and the Picard-Lindelöf theorem. The registry table explicitly places ode_cosh_uniqueness in the Mathematical Fact row alongside ode_zero_uniqueness and dAlembert_to_ODE.
proof idea
One-line definition that assigns the status string to the ODE uniqueness claim.
why it matters
The declaration supplies the ODE foundation used when the functional equation is solved for the recognition cost. It appears in the module summary table under Mathematical Fact and supports the identification of the cosh form that appears in T5 J-uniqueness. No open problem is closed; the entry simply documents a prerequisite for later steps that reach the phi-ladder and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.