IndisputableMonolith.Cost.FunctionalEquationStrict
Strengthens the T5 cost-uniqueness route by dropping the explicit continuity hypothesis on the cost functional. Limit-form log calibration already supplies the continuity Aczél's d'Alembert argument needs, so only the composition law and log calibration are essential. The older three side premises stay in the interface as derived consequences so existing callers still type-check. Cite when quoting the unconditional J-cost identification.
claimUnder the Recognition Composition Law and limit-form logarithmic calibration, any admissible cost $F:(0,\infty)\to\mathbb{R}$ coincides with the unique $J$-cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$), without a separate hypothesis that $F$ is continuous on $(0,\infty)$.
background
Recognition Science forces the cost functional at step T5 of the unified forcing chain: the unique symmetric cost is $J(x)=\frac{x+x^{-1}}{2}-1$. The algebraic skeleton is the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, which is the multiplicative form of d'Alembert's equation after the change of variables $x=e^t$.
The sibling module FunctionalEquation packages T5 helper lemmas. AczelProof supplies Aczél's smoothness theorem: any continuous $H:\mathbb{R}\to\mathbb{R}$ solving $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ is real analytic (integration bootstrap from continuous to $C^\infty$). Classically one therefore assumes $F$ continuous on $(0,\infty)$ before invoking Aczél.
This module records that a limit-form logarithmic calibration hypothesis already yields that continuity, so the explicit $C((0,\infty))$ premise is redundant for the T5 variant used here.
proof idea
Argument structure, not a single theorem: (1) start from the composition law plus limit-form log calibration; (2) derive continuity of $F$ on $(0,\infty)$ from the calibration limits, removing the need to assume it; (3) feed the resulting continuous d'Alembert solution into the Aczél smoothness pipeline from the imported proof module; (4) identify the analytic solution with $J$ via the existing FunctionalEquation T5 helpers. The three non-essential interface premises are proved as corollaries of the essential pair so legacy callers keep the same type.
why it matters in Recognition Science
Closes a hygiene gap on the T5 J-uniqueness step: the forcing chain should not carry an extra continuity axiom once log calibration is present. Downstream, the sibling results that law-of-logic plus log calibration force the $J$-cost, and that composition plus log-curvature force $J$ unconditionally, sit on this stricter interface. In the broader RS picture this is the cost half of the T5 landmark ($J(x)=\cosh(\log x)-1$), which later pins $\phi$ (T6), the eight-tick octave (T7), and $D=3$ (T8). No external used-by edges are recorded yet; the module is infrastructure for those unconditional T5 wrappers.
scope and limits
- Does not reprove Aczél smoothness; imports that analytic bootstrap.
- Does not remove composition or log-calibration; only drops explicit continuity.
- Does not by itself force $\phi$, the eight-tick period, or $D=3$.
- Does not claim the three retained side premises are independent axioms.
- Does not address discrete or non-positive domains outside $(0,\infty)$.