AngleCouplingAxioms
plain-language theorem explainer
The AngleCouplingAxioms structure packages the four conditions on a real function H that select the cosine solution to the d'Alembert functional equation. Researchers deriving the angle branch of the Recognition Science forcing chain cite it when establishing uniqueness of the coupling function. The definition directly assembles the d'Alembert relation, continuity, normalization at zero, and second-derivative calibration without additional lemmas.
Claim. A function $H:ℝ→ℝ$ satisfies the angle coupling axioms when $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, $H$ is continuous, $H(0)=1$, and the second derivative satisfies $H''(0)=-1$.
background
In the Recognition Science framework the angle functional equation is the dual to the cost functional equation. The d'Alembert relation admits two branches distinguished by the sign of the second derivative at the origin. The cost side (from Cost.FunctionalEquation.H and CostAxioms.Calibration) uses positive curvature to recover the shifted J-cost $H(x)=J(x)+1$, while the angle side uses negative curvature to recover cosine. Upstream results from CostAxioms supply the normalization and calibration patterns mirrored here, and UniversalForcingSelfReference supplies the self-referential forcing that closes the chain.
proof idea
This declaration is a structure definition that directly bundles the four axioms dAlembert, continuous, normalized, and calibrated. No tactics or lemmas are applied; the structure serves as a hypothesis carrier for the subsequent rigidity theorem.
why it matters
AngleCouplingAxioms supplies the hypothesis bundle for THEOREM_angle_coupling_rigidity, which states that any H satisfying these axioms equals the cosine function. It completes the angle branch of the forcing chain (T5 J-uniqueness mirrored to angle), parallel to the cost side. The structure appears in the Recognition Science derivation of geometric necessity for the angle coupling, with references to Aczél's work on functional equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.