charges_positively_at_two
plain-language theorem explainer
Any nondegenerate structural cost on ratio orbits that is nonzero at orbit two is strictly positive there. Classification and monotonicity arguments cite this to replace a disequality by an inequality. The proof upgrades the lower bound on the rational trace at 2 to a strict inequality, then reads positivity off the cost-display identity.
Claim. Let $F$ be a ratio-orbit map satisfying the anchor-free structural cost hypotheses. If $(F\,2)^{\mathbb{Q}} \neq 0$, then $(F\,2)^{\mathbb{Q}} > 0$.
background
The module classifies gauge orbits of structural recognition costs on ratio orbits: maps $F$ obeying the Recognition Composition Law pack without the two-point calibration anchor (SansAnchorHypotheses). Values live in a rational display (F q).toRat.
The doubled trace rationalTrace F x is the honest real function on rational displays obtained from the native doubled-trace presentation. The private identity cost_display states that the cost display is the trace display halved and shifted: $((F q)^{\mathbb{Q}}:\mathbb{R}) = \mathrm{rationalTrace},F,q^{\mathbb{Q}}/2 - 1$. In particular at orbit two this becomes $(F,2)^{\mathbb{Q}} = \mathrm{rationalTrace},F,2/2 - 1$.
Upstream, rationalTrace_nat_ge_two gives $\mathrm{rationalTrace},F,n \ge 2$ for every natural $n\ge 2$ under the same hypotheses, and vanishes_at_two_iff_trace_two equates vanishing cost at two with the degenerate trace value $2$. The ledger's native monotonicity is non-strict (PRCNativeCostMonotone: $\le\to\le$ on positive integer orbits).
proof idea
Apply rationalTrace_nat_ge_two at $n=2$ to obtain $\mathrm{rationalTrace},F,2 \ge 2$. The nonvanishing hypothesis plus vanishes_at_two_iff_trace_two rules out equality, so the trace is strictly above $2$. Rewrite via cost_display at orbit two (after two_toRat) and finish by linarith on the shifted half-trace, then cast back to rationals.
why it matters
Nondegeneracy at orbit two is the concrete positivity gate for the anchor-free gauge classification. Downstream, strict_somewhere_iff_charges_at_two equates charging anything at two with the cost order being strict somewhere on positive ratios; its doc-comment notes that the ledger only assumes non-strict monotonicity and that the unique flat inhabitant is the sign cost. The main classification theorem GaugeOrbitIsSignedPowerFamily_of_sixExponentials case-splits on whether the rational trace at $2$ equals $2$: the degenerate branch is the sign gauge, and the complementary branch needs a positive charge rather than a mere disequality when selecting signed power families.
In the Recognition framework this sits inside the cost/J layer that feeds T5 J-uniqueness and the RCL. It does not itself select $J$; leastness and unit selection live in Cost.UnitFromMinimality. The audit script records it as an explicit hypothesis rather than an ambient axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.