PRCSlimSansTwoCalibrationHypotheses
plain-language theorem explainer
Packages the native-cost axioms on a map F of rational orbits without fixing the value at the orbit 2. It bundles reciprocity, normalization invariance, and the Recognition Composition Law with prime-pair product calibration, signed-unit calibration, and zero-orbit doubled-trace calibration. Uniqueness targets and the bridge back to the full slim ledger cite this class. Pure Prop-structure definition; no proof content.
Claim. For a map $F$ from rational orbits to rational orbits, the slim native-cost package without two-point calibration asserts four blocks: (i) base fields of reciprocity $F(q)\sim F(q^{-1})$, normalization invariance, and the Recognition Composition Law on products and quotients; (ii) prime-pair product calibration; (iii) signed-unit calibration; (iv) the doubled trace $T_F(q)=2\bigl(F(q)+1\bigr)$ satisfies $T_F(0)=0$.
background
In the Primitive Recognition Calculus, costs act on rational orbits: each orbit is an integer numerator over a nonzero distinction-natural denominator. A native cost is a map $F$ on those orbits meant to realize the unique J-cost forced by the Recognition Composition Law (RCL), $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, which is the T5 uniqueness landmark $J(x)=(x+x^{-1})/2-1$.
The base package without the two-point anchor already requires reciprocity, invariance under normalization of the ratio display, and the canonical RCL identity on nonzero orbits. Two further calibrations pin multiplicative structure at prime pairs and at signed units. Separately, the doubled d'Alembert trace $T_F(q)=2(F(q)+1)$ is the character form $\chi(q)+\chi(q)^{-1}$ for generated costs; the nonzero d'Alembert law does not constrain $T(0)$, so zero-orbit compatibility $T_F(0)=0$ is stated on its own.
The missing two-point anchor is the single equality $F(2)=J(2)$ (equivalently the on-orbit display of 2). This structure deliberately omits that field so one can study the residual class and prove that the anchor is necessary for uniqueness.
proof idea
No proof: this is a Prop-valued structure definition. It is the conjunction of four named hypothesis bundles on $F$: the base-sans-two native-cost fields, prime-pair product calibration, signed-unit calibration, and zero-calibration of the doubled trace of $F$. Inhabitation is discharged later by separate theorems that supply each field.
why it matters
This is the working hypothesis class for native-cost uniqueness once the two-point anchor at 2 is stripped. Downstream, the uniqueness target states that every $F$ in this class agrees with the canonical on-orbit J-display at every rational orbit. The bridging iff shows the full slim ledger is exactly this class plus $F(2)=J(2)$, so any counterexample here is a necessity statement about the slim ledger's own two-point field.
Non-vacuity is immediate: the canonical selected native cost inhabits the class, and the Liouville twist also satisfies every slim field except the two-point anchor. That pair of witnesses separates the residual freedom from the forced J-shape and ties the package to T5 J-uniqueness and the RCL in the forcing chain. The open pressure point is whether uniqueness holds on this thinner class, or whether the two-point calibration is indispensable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.