PRCDoubledTraceZeroCalibrated
plain-language theorem explainer
Zero-orbit calibration for doubled-trace maps on ratio orbits: T sends the zero orbit to a value cross-equivalent to zero. Native-cost uniqueness and minimality packs cite this as the zero constraint that nonzero d'Alembert alone cannot force. Defined directly as cross-multiplication balance of T(0) against the zero orbit; no proof body.
Claim. A map $T$ from ratio orbits to ratio orbits is zero-calibrated when $T(0)$ is cross-equivalent to the zero orbit, i.e., the signed-orbit cross-multiplication of numerator and denominator balances.
background
In the Primitive Recognition Calculus, a ratio orbit is a signed-orbit numerator over a nonzero distinction-nat denominator. Two ratio orbits stand in the crossEq relation when scaled numerators balance as signed orbits; that is the internal PRC stand-in for rational equality (K4.10).
Doubled traces come from character-style cost maps on ratio orbits. The nonzero d'Alembert law constrains the map away from zero but leaves $T(0)$ free. Character traces meant to match the native recognition cost send the zero orbit to zero, so their doubled trace vanishes there. The doc-comment states the gap explicitly: "The nonzero d'Alembert law cannot constrain $T(0)$, but character traces with the intended zero image have doubled trace $0$ at the zero orbit."
The surrounding module packages uniqueness hypotheses for the native cost; this definition isolates the zero-orbit clause those packs require.
proof idea
Definitional one-liner. The property is exactly cross-equivalence of $T$ at the zero orbit with the zero orbit: RatioOrbit.crossEq (T RatioOrbit.zero) RatioOrbit.zero. No tactics, no lemmas applied; it is a Prop-valued abbreviation for that balance statement.
why it matters
Feeds the slim and strengthened native-cost hypothesis packs (PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses, SansAnchorHypotheses) and the certificates that exclude competitors such as the zero-flat cost. Downstream gauge-orbit results (signedPowerNativeCost_zero_calibrated, signGaugeNativeCost_zero_calibrated) discharge it for concrete character costs. Layer discrimination uses the failure of zero-flat cost exactly at this clause (zeroFlatNativeCost_slim_excluded).
In the Recognition forcing chain this supports T5 J-uniqueness: the native cost is singled out by reciprocity, RCL on nonzero orbits, and zero calibration. Without the clause, zero-flat impostors pass every nonzero axiom. It is the missing zero-orbit compatibility that doubled-trace uniqueness arguments need once d'Alembert is restricted off zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.