BaseSansTwo
plain-language theorem explainer
Packages the core algebraic hypotheses on a cost map F over ratio orbits: reciprocity, normalization invariance, the Recognition Composition Law, and vanishing at the unit. Omits the two-point calibration on purpose. Downstream anchor-free native-cost packs cite it as the base layer. Structure definition only; no proof body.
Claim. A predicate on maps $F$ from ratio orbits to ratio orbits asserting four properties: (i) $F(q)$ is cross-multiplication-equivalent to $F(q^{-1})$; (ii) $F$ is invariant under ratio normalization up to that same equivalence; (iii) whenever the rational displays of $x,y$ are nonzero, $F$ obeys the Recognition Composition Law $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ in orbit arithmetic; (iv) $F(1)=0$. No two-point calibration hypothesis is included.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator: the internal stand-in for a positive rational. Equality of orbits is not definitional identity but cross-multiplication balance of scaled signed orbits (the internal PRC rational relation). Reciprocal, product, quotient, and addition are total operations on these displays; the verifier map to $\mathbb{Q}$ is only a transport wrapper.
The Recognition Composition Law (RCL) is the functional equation that forces the unique cost $J(x)=(x+x^{-1})/2-1$ on the positive reals (forcing chain T5). Here it is written entirely in ratio-orbit arithmetic, with the constant two appearing as an orbit rather than a real scalar.
This module factors real characterizations of native cost. The present pack is the RCL core stripped of the two-point anchor that would fix the scale at a second calibration point.
proof idea
Definitional structure with four Prop fields and no proof body. Each field is a quantified statement over ratio orbits using cross-equivalence, reciprocal, normalize-ratio, mul/div/add, and the unit/zero constants. Downstream structures simply embed an instance of this pack as a field.
why it matters
Feeds SansAnchorHypotheses, which adds sign-reversal, monotonicity, and zero-calibration of the doubled trace to match the structural native-cost hypotheses without an anchor. That pack is the bridge from pure RCL algebra on ratio orbits to uniqueness of the native cost character (the real factorization path toward T5 J-uniqueness).
By isolating the RCL core from two-point calibration, the framework can prove what follows from reciprocity, normalization, unit vanishing, and composition alone, then reintroduce scale separately. This is the algebraic skeleton of the Recognition Composition Law inside PRC, before real embedding or ladder constants enter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.