cost_at_zero
plain-language theorem explainer
When a ratio-orbit display is zero, any native cost map satisfying the anchor-free hypotheses is forced to rational value -1. Gauge-orbit classification cites this to close the zero branch of the display trichotomy on both the degenerate and nondegenerate sides. The proof is a direct hit of the sign-reversing axiom at the pair (q,q), finished by linear arithmetic; character data and zero-calibration are unused.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost hypotheses (base away from the two-point, sign-reversing, monotone, and zero-calibrated). If $q$ is a ratio orbit whose rational display equals $0$, then the rational display of $F(q)$ equals $-1$.
background
Ratio orbits are the PRC-native displays of rationals: a signed-orbit numerator over a nonzero orbit denominator, recovered in the verifier by the ordinary quotient map to $\mathbb{Q}$. The ambient module classifies native cost maps on these displays up to gauge.
The anchor-free hypothesis pack on a cost map $F$ bundles four properties: a base condition away from the two-point, sign-reversal, monotonicity, and zero-calibration of the doubled trace. The present result uses only the sign-reversing fragment. As the doc-comment records, "orientation reversal alone pins the cost, with no character and no appeal to the zero calibration field."
In the Recognition cost calculus the forced $J$-cost (T5) is fixed by the Recognition Composition Law; at the singular zero display only the orientation-reversal identity remains to set the value, independently of any positive-character data.
proof idea
Short term proof. Instantiate the sign-reversing field of the anchor-free pack at the pair $(q,q)$, discharging the side condition by rewriting the display of $q$ to $0$ and normalizing the resulting numeral. The returned relation is an affine constraint on the rational display of $F(q)$. Close with linear arithmetic, which solves that constraint to display value $-1$. Monotonicity, the base-sans-two clause, and zero-calibration are never invoked.
why it matters
Local pin for both branch theorems of gauge-orbit classification in this module. The degenerate branch identifies the flat-trace case with the pure sign cost: after the cost is shown to vanish on every positive display, "orientation reversal fills in the rest," and the zero case is exactly this lemma. The nondegenerate branch likewise trichotomizes on the sign of the display and needs the zero value to match the sign-extended power cost.
Framework-wise, T5 forces the unique $J$-cost via the Recognition Composition Law; the gauge-orbit analysis shows native cost maps on ratio orbits collapse to either the sign gauge or a signed power. The common zero-display value $-1$ is the shared normalization of both branches. The claim is fully proved, with no scaffold left open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.