Jcost_three
plain-language theorem explainer
The recognition cost at ratio 3 equals 2/3. Holography and census-pricing arguments cite this as the triple-cover evaluation of the T5 J-cost. The proof unfolds the closed form J(x)=(x+x^{-1})/2-1 and finishes by numeric normalization.
Claim. The recognition cost satisfies $J(3)=\frac{2}{3}$, where $J(x)=\frac{1}{2}\bigl(x+x^{-1}\bigr)-1$.
background
In Recognition Science the unique cost forced by the Recognition Composition Law (T5) is $J(x)=\frac12(x+x^{-1})-1$ for $x>0$. It vanishes only at $x=1$ and is the character anomaly of a balanced $2\times2$ transfer: if $W$ has $\det W=1$ and a real eigenvalue $x\neq0$, then $\mathrm{Tr}(W)=x+x^{-1}$ and $\mathrm{Tr}(W)/2-1=J(x)$.
SeamTransferCore develops the per-closure half of the Scale-Holonomy Trace Core. Balance forces the reciprocal leg; the trace is then forced; the character anomaly equals $J$. Integer arguments $n$ arise as $n$-fold retrace (cover) ratios on the seam fiber. The value $J(3)$ is the absolute surplus cost of the triple cover, used with $J(2)$ to form the numeric trace-carrier signature.
proof idea
Term-mode one-liner: unfold the definition of Cost.Jcost, which is $(x+x^{-1})/2-1$, then apply norm_num to evaluate at $x=3$. Explicitly, $(3+1/3)/2-1=(10/3)/2-1=5/3-1=2/3$. No external lemmas beyond the definition and numeric normalization.
why it matters
Feeds cover_cost_ratio_eq, which proves the trace-carrier signature $J(3)/J(2)=8/3$. That ratio is the panel's numeric falsifier (Live Bet 2): pairing pricing and linear surplus pricing are distinguished at the triple cover. The module doc ties the $n$-fold retrace observables (absolute surplus $n-1$, relative surplus $(n-1)/n$) to exactly $J(n)$; this lemma supplies the $n=3$ evaluation.
Within the forcing chain it is a concrete instance of T5 J-uniqueness, not a new derivation of $J$. It closes the arithmetic side of the holographic seam-transfer reduction: once character anomaly equals $J$, cover costs become ordinary rational numbers that census observables can match or refute.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.