jcost_composesThrough_rclCombiner
plain-language theorem explainer
The recognition cost $J(x)=\frac12(x+x^{-1})-1$ composes through the RCL combiner: $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ for positive $x,y$. Anyone citing ledger-composition forcing of $J$, or the Phase 3 certificate, needs this non-vacuity check. Proof unfolds both sides and closes by field simplification and ring.
Claim. For all real $x,y>0$, the recognition cost $J(x)=\frac12(x+x^{-1})-1$ satisfies $J(xy)+J(x/y)=2\,J(x)\,J(y)+2\,J(x)+2\,J(y)$. Equivalently, $J$ composes through the RCL combiner $P(u,v)=2uv+2u+2v$: the symmetric two-point combination of $J$ equals $P$ evaluated at the single-point costs.
background
This module is the Phase 3 endpoint that derives the recognition composition law from the ledger rather than assuming it. A cost $F$ is said to compose through a binary combiner $P$ when
$$F(xy)+F(x/y)=P(Fx,Fy)\qquad(x,y>0).$$
That identity is the factorization/composability input: the two-point combination is governed by a law of the two single-point costs.
Here $J$ is the RS recognition cost $J(x)=\frac12(x+x^{-1})-1$, and the RCL combiner is the canonical polynomial $P(u,v)=2uv+2u+2v$ (right-hand side of the Recognition Composition Law). Phase 3 already forces any primitive ledger-posting combiner with directional regularity to equal this $P$. The residual bare composability statement is isolated in CostComposesThrough; the present theorem shows $J$ itself is a fixed point of that setup, so the construction is non-vacuous.
proof idea
Direct term proof. Introduce positive $x,y$; extract $x\neq0$ and $y\neq0$ from positivity. Unfold the definitions of $J$ and of the RCL combiner $P(u,v)=2uv+2u+2v$. field_simp clears the inverses that appear in $J(xy)$ and $J(x/y)$; ring finishes the resulting polynomial identity. No external lemmas are required beyond the two definitions.
why it matters
Non-vacuity half of the ledger-composition story: $J$ is a genuine fixed point of the composition law it forces. Downstream it is applied three ways. First, it yields that $J$ itself satisfies the recognition composition law (one-line wrapper through the RCL-combiner implication). Second, it witnesses that $J$'s symmetric combination is cost-determined, so the factorization-existence condition is inhabited. Third, it is a field of the ledger-composition certificate that packages the whole Phase 3 closure.
In the broader framework this is the concrete check that the T5 cost $J(x)=\cosh(\log x)-1$ realises the RCL $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. The module replaces the bare SatisfiesCompositionLaw hypothesis of law_of_logic_forces_jcost by a ledger-side composability statement; this theorem shows that residual is attained by $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.