PRCNativeCostHypothesesSansTwoCalibration
plain-language theorem explainer
Bundles the four base axioms a native cost map on ratio orbits must obey when the two-point calibration anchor is dropped: reciprocal symmetry, normalization invariance, the Recognition Composition Law on nonzero orbits, and F(1)=0. Cited by anyone checking that power-generated, signed-power, sign-gauge, or square costs sit on the free ledger. Pure Prop structure; no proof body.
Claim. For a map $F$ from ratio orbits to ratio orbits, the following hold: (i) $F(q)$ is cross-equivalent to $F(q^{-1})$ for every orbit $q$; (ii) $F(q)$ is cross-equivalent to $F$ of the normalized form of $q$; (iii) whenever $x,y$ have nonzero rational displays, $F(xy)+F(x/y)$ is cross-equivalent to $2F(x)F(y)+2F(x)+2F(y)$; (iv) $F(1)=0$.
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. Two orbits are cross-equivalent when the signed-orbit products of numerator against opposite denominator balance (the PRC form of rational equality). Reciprocal sends an orbit to its inverse (zero to zero), and normalization collapses a ratio to a canonical representative.
The Recognition Composition Law (RCL) is the functional equation forced on the J-cost in the T5 uniqueness step of the forcing chain: $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Here it is stated entirely on ratio-orbit arithmetic with the constant two, using cross-equivalence rather than external rationals.
This module packages native-cost minimality certificates. The present structure is the base layer of that ledger with the two-point anchor stripped out, so candidate costs can be checked against free structural fields alone.
proof idea
Definitional Prop structure: four named fields, no proof body. Instances are built by supplying reciprocal, normalized_invariant, canonical_rcl, and unit_zero. Downstream proofs typically discharge each field by rewriting cross-equivalence to rational equality of verifier displays, then applying the corresponding identity for the concrete cost (e.g. inv_pow and jq_inv for power-generated costs, or signedPow_inv for signed powers).
why it matters
This is the free side of the native-cost ledger: every structural check that deliberately omits two-point calibration lands here. Downstream, PRCSlimSansTwoCalibrationHypotheses extends it by prime-pair product, signed-unit, and zero calibration. Power-generated, even-power, signed-power, and sign-gauge costs all inhabit it (powerGeneratedNativeCost_base, signedPowerNativeCost_base, signGaugeNativeCost_base_sans_two).
The structural ledger uses it to isolate orientation: evenPowerGeneratedNativeCost_sans_signReversing shows even powers satisfy the whole anchor-free package except sign reversal, and native_ledger_refutes_the_square_cost shows the continuum's $\lambda=2$ countermodel satisfies every field here yet fails the full sans-anchor ledger on orientation alone. That separation is the discrete analogue of T5 J-uniqueness under RCL without continuum calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.