UnitNormalizationZeroCert
plain-language theorem explainer
Packages the elementary fact that unit normalization F(1)=0 forces the log-coordinate cost to vanish at the origin: G_F(0)=0. Anyone wiring the multiplicative cost into the ODE uniqueness chain cites this certificate. The check is a one-line appeal to G_zero_of_unit from the functional-equation module.
Claim. A unit-normalization zero certificate is a trivial witness whose verification predicate asserts: for every real function $F$, if $F(1)=0$ then $G_F(0)=0$, where the log-coordinate reparametrization is $G_F(t):=F(e^t)$. The certificate always verifies.
background
In the cost calculus, the multiplicative cost $F:\mathbb{R}\to\mathbb{R}$ is reparametrized to log-coordinates by $G_F(t)=F(e^t)$. The companion shift $H_F:=G_F+1$ is the object fed to ODE uniqueness arguments. Unit normalization means $F(1)=0$: zero cost at the multiplicative identity (no deviation from the reference scale).
The module packages exactly the bridge from that normalization to the log origin. Because $t=0$ corresponds to $x=e^0=1$, the identity $G_F(0)=F(1)$ is definitional. Upstream, G_zero_of_unit records the same one-line fact: from $F(1)=0$ conclude $G_F(0)=0$ by unfolding $G$.
Local setting is the verification certificate chain: each small algebraic link is wrapped as a named cert so downstream forcing and uniqueness theorems can cite a single Prop rather than re-open the cost definitions.
proof idea
The structure itself is empty (only Repr). The content lives in the simp predicate verified, which is the universal statement $\forall F,, F(1)=0\to G_F(0)=0$.
The top-level theorem verified_any is a one-line wrapper: introduce $F$ and the unit hypothesis, then apply the upstream lemma G_zero_of_unit, which itself is simpa [G] on the hypothesis. No further algebra is required.
why it matters
This is the first hop in the documented chain $F(1)=0\to G_F(0)=0\to H(0)=1\to$ ODE initial conditions. Without the log-origin vanishing, the uniqueness theorem for the cost ODE lacks its canonical initial value $H(0)=1$.
In Recognition Science the cost $J$ (T5 uniqueness: $J(x)=(x+x^{-1})/2-1$) is normalized so the fixed point of self-similarity sits at unit scale; this certificate is the bookkeeping step that moves that normalization into the additive coordinate used by the forcing and ODE layers. No downstream consumers are wired yet in the graph (used_by empty), so the cert currently stands as a reusable leaf for later verification assemblies rather than a live dependency of a named parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.