costFromRealCharacter
plain-language theorem explainer
Defines the native recognition cost of a ratio orbit by feeding a real-valued character into the unique J-functional: $(\chi(q)+\chi(q)^{-1})/2-1$. Cost and factorization authors cite it whenever an anchor-free ledger is reconstructed from a real character. The body is a one-line abbreviation of the T5 J-form.
Claim. Given a real-valued map $\chi$ on rational orbits and an orbit $q$, the associated cost is $J(\chi(q)) := \frac{\chi(q) + \chi(q)^{-1}}{2} - 1$.
background
In Recognition Science the unique symmetric cost on positive reals is the T5 functional $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced by the Recognition Composition Law. This module lifts that cost from bare reals to the discrete ledger of ratio orbits.
A ratio orbit is a signed-integer numerator over a nonzero distinction-natural denominator (K4.7), the discrete stand-in for a positive rational. A real character is a map $\chi$ from such orbits into $\mathbb{R}$ that will later be required to satisfy the PRC real-ratio character axioms (positivity, multiplicativity on the orbit monoid, and rational traces at the small bases).
The surrounding development works in the anchor-free (sans-anchor) setting: native costs on ratio orbits that obey the structural PRC hypotheses without a distinguished basepoint. The present definition is the bridge that turns any candidate real character into a real-valued cost on orbits.
proof idea
Pure definitional abbreviation: evaluate the character at the orbit, apply the closed-form T5 expression $(\chi(q)+\chi(q)^{-1})/2-1$, and return the real. No lemmas are invoked; noncomputable only because real inversion and division are used.
why it matters
This is the cost side of the real-character factorization that the module targets. Downstream, SansAnchorRealCharacterFactorizationTarget packages the claim that every anchor-free native cost $F$ factors as $F(q)=J(\chi(q))$ for some real character $\chi$ with rational traces at the small bases (so the exponent step can fire). The agreement theorem realCharacterCandidate_cost_agrees shows that the concrete candidate character built from $F$ recovers $F$ exactly via this definition. The structural theorem in GaugeOrbitFromRealCharacter then lifts the same factorization to every structural sans-anchor cost. In the forcing chain this is the concrete realization of T5 J-uniqueness on the discrete ratio-orbit ledger, feeding the later uniqueness and gauge-orbit arguments that pin the native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.