cost_at_neg
plain-language theorem explainer
Negative ratio-orbit displays of an anchor-free native cost are fixed by the positive ones: in rational coordinates, F(q) equals -F(orbit of -q) minus 2. Gauge-orbit classification cites this when filling the negative ray for both the degenerate (sign) and nondegenerate (signed-power) branches. The proof is a direct application of the sign-reversing field of the anchor-free hypothesis pack, after a ring identity on the orbit map.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost hypotheses (base without two, sign-reversing, monotone, zero-calibrated doubled trace). For every ratio orbit $q$, $$(F\,q)^{\mathrm{rat}} = -\bigl(F(\mathrm{orbit}(-q^{\mathrm{rat}}))\bigr)^{\mathrm{rat}} - 2.$$
background
The module classifies native costs on ratio orbits up to gauge, under the anchor-free pack SansAnchorHypotheses. That pack bundles four structural axioms: a base law away from the special point two, a sign-reversing identity, monotonicity, and zero-calibration of the doubled trace. The cost here is the native cost induced on ratio orbits, not the summed event cost of cosmology or the J-cost of a single recognition event; those appear only as ambient vocabulary.
Ratio orbits are the discrete displays of positive and negative rational ratios used by the primitive recognition calculus. The map ratioOrbitOfRat sends a rational back to its orbit representative; toRat reads the rational coordinate of a display. Sign-reversal on displays is the structural stand-in for orientation flip: the cost on a negative display is forced once the positive side is known.
The local setting is the gauge-orbit classification of native costs: every F obeying the pack is either the pure sign cost (degenerate anchor) or a sign-extended power cost (nondegenerate branch).
proof idea
Term-mode one-liner. Instantiate the sign_reversing field of the anchor-free hypothesis pack at the pair (orbit of $-q$, $q$). The side condition that these two orbits are related by rational negation is discharged by rewriting through ratioOrbitOfRat_toRat and a ring identity. No further case split or monotonicity is used.
why it matters
This lemma is the negative-ray filler for the two main classification theorems in the same module. degenerate_is_signGauge quotes it after showing the cost vanishes on every positive display when the trace at two equals two; orientation reversal then matches the sign gauge everywhere. nontrivial_is_signedPower uses the same identity to extend a positive power character to a signed power on all orbits.
In the broader Recognition framework the result is local bookkeeping inside the cost layer, not a forcing-chain step (T5–T8). It ensures that once the positive J-type cost is fixed, the orientation-reversed displays cannot introduce a second independent degree of freedom. Without it the gauge classification would leave the negative half-line open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.