PRCNativeCostHypothesesSansRcl
plain-language theorem explainer
Packages four base axioms on a native cost map F from ratio orbits to ratio orbits: reciprocity under inversion, invariance under normalization, F(1)=0, and calibration at 2. Anyone assembling slim ledger cost hypotheses without the Recognition Composition Law cites this bundle. It is a Prop-valued structure definition, not a proved theorem.
Claim. For a map $F$ sending ratio orbits to ratio orbits, the following hold: $F(q)$ is cross-multiplication equivalent to $F(q^{-1})$ for every ratio orbit $q$; $F(q)$ is cross-equivalent to $F$ of the normalized form of $q$; $F(1)=0$; and $F(2)$ is cross-equivalent to the native on-ratio cost of $2$.
background
In the Primitive Recognition Calculus (PRC), quantities live on distinction orbits rather than classical rationals. A ratio orbit is an integer numerator over a nonzero distinction-nat denominator. Two ratio orbits are identified by cross-equivalence when the scaled numerators balance as signed orbits (the internal PRC stand-in for rational equality).
The total reciprocal on ratio orbits sends zero to zero and otherwise inverts, matching the reciprocal automorphism of the cost algebra and the reciprocal recognition event in the ledger. Normalization collapses a ratio orbit to a canonical representative via distinction-nat reduction.
This module certifies native-cost minimality hypotheses. The present structure isolates the base fields that do not mention the nonzero Recognition Composition Law (RCL), so later slim-ledger packages can add prime-pair, signed-unit, and zero calibrations separately.
proof idea
No proof body: this is a Prop-valued structure definition. It declares four fields on a candidate cost map F (RatioOrbit to RatioOrbit): reciprocal (crossEq of F(q) with F of the reciprocal), normalized_invariant (crossEq of F(q) with F of the normalized ratio), unit_zero (strict equality F(one)=zero), and two_calibrated (crossEq of F(two) with the native on-ratio display of two). Downstream structures inhabit the type by supplying proofs of each field.
why it matters
Native cost minimality in PRC aims to force the J-cost shape without smuggling in the full Recognition Composition Law at the outset. This bundle is the RCL-free base layer. It is the first field of PRCSlimSansRclHypotheses ("Slim ledger minus the nonzero RCL"), which then adds prime-pair product cost, signed-unit calibration, and zero calibration.
In the broader forcing chain, J-uniqueness (T5) and the RCL identity J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y) are the algebraic heart of Recognition Science. Isolating what can be stated before nonzero RCL keeps the certificate modular: reciprocity, normalization invariance, and the unit/two anchors can be checked or assumed independently of the composition law that eventually pins J(x)=(x+x^{-1})/2-1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.