quadraticWitness_continuous
plain-language theorem explainer
The quadratic cost witness G(t)=t²/2 is continuous on the reals. Anyone citing the T5 ledger no-go needs this fact: continuity is one of the four hypotheses in the Aczél-style package that still fails to force Cosh-Add. The proof is a one-line unfold plus Mathlib's fun_prop automation.
Claim. The map $G:\mathbb{R}\to\mathbb{R}$ given by $G(t)=t^2/2$ is continuous.
background
This module sits in the T5 verification layer. From ledger structure (T3) it derives reciprocal symmetry $F(x)=F(1/x)$ and unit normalization $F(1)=0$, then proves a no-go: those constraints plus continuity and unit log-curvature do not force the Cosh-Add (d'Alembert) identity that pins down the unique admissible cost $J$.
The quadratic witness is the explicit counterexample $G(t)=t^2/2$. Upstream it is defined as even, vanishing at the origin, continuous, with unit second derivative at zero, yet it fails Cosh-Add. Continuity of $G$ is one of the four properties fed into the Aczél-style hypothesis that the no-go refutes.
In the Recognition forcing chain, T5 asserts uniqueness of $J(x)=(x+x^{-1})/2-1$. The honest chain treats the composition law C6 as an independent load-bearing hypothesis, not a ledger consequence.
proof idea
Term-mode one-liner: unfold the definition $G(t)=t^2/2$, then invoke Mathlib's fun_prop to discharge continuity of polynomials (powers and scalar division) on $\mathbb{R}$. No custom lemmas.
why it matters
Feeds directly into aczel_hypothesis_refuted, the kernel-checked no-go certificate (Finding 2 resolution). That theorem shows the Aczél-style package
symmetry + unit + continuity + unit second-derivative calibration
does not imply Cosh-Add; the witness is exactly $G(t)=t^2/2$. Continuity is the third hypothesis passed into that package, so this lemma is a required premise of the refutation.
Framework role: it keeps T5 honest. Ledger structure forces only symmetry and unit; C6 (Recognition Composition Law / Cosh-Add) remains independent. Without the continuous quadratic counterexample, an earlier false claim that T5 was unconditionally forced from T1–T4 would stand. The result therefore underwrites the corrected forcing chain in which J-uniqueness still needs the composition law as a separate axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.