vanishes_at_two_iff_trace_two
plain-language theorem explainer
Cost of an anchor-free structural ledger vanishes at the ratio orbit 2 exactly when its rational trace there equals the degenerate value 2. Classification proofs cite this to split the flat sign-gauge case from nontrivial signed-power costs. The argument is a two-sided arithmetic rewrite through the identity cost = trace/2 − 1 at orbit two.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free structural cost hypotheses (base-sans-two, sign-reversing, monotone, zero-calibrated doubled trace). Then the rational display of $F$ at the orbit $2$ is zero if and only if the rational trace of $F$ at $2$ equals $2$.
background
In the gauge-orbit cost ledger, each structural cost $F$ is a map on ratio orbits. The verifier display toRat sends an orbit to a positive rational; the distinguished orbit two has display $2$. The rational trace is the doubled-trace display read as a real function of rational arguments.
The private identity cost_display states that under the anchor-free pack, the real embedding of the cost at any orbit $q$ equals half the rational trace at $q$'s display, shifted by one: $((F q).\mathrm{toRat}:\mathbb{R}) = \mathrm{rationalTrace},F,q.\mathrm{toRat}/2 - 1$. This is the discrete form of the $J$-cost relation $J(x)=(x+x^{-1})/2-1$ (T5).
SansAnchorHypotheses packages base-sans-two, sign-reversal, monotonicity, and zero-calibration of the doubled trace, matching the PRC structural native-cost hypotheses without an anchor.
proof idea
Instantiate cost_display at orbit two and rewrite two.toRat = 2 via two_toRat, obtaining
$((F,\mathrm{two}).\mathrm{toRat}:\mathbb{R}) = \mathrm{rationalTrace},F,2,/,2 - 1$.
Forward: if the left side is $0$, substitute and linarith forces the trace equal to $2$. Reverse: if the trace is $2$, the display identity collapses to $0$ by norm_num, then cast back to the rational equality. No structural lemmas beyond the display identity are needed.
why it matters
This is the local degeneracy test that opens the anchor-free gauge classification. Downstream, vanishes_at_two_iff_flat lifts vanishing at two to vanishing on every positive ratio ("charging nothing at one point is charging nothing anywhere"). charges_at_two_iff_not_signGauge and charges_positively_at_two convert nonvanishing into exclusion of the pure sign cost and into a strict positivity inequality.
The main classification theorem GaugeOrbitIsSignedPowerFamily_of_sixExponentials cases on rationalTrace G 2 = 2: the degenerate branch is the sign gauge; the nondegenerate branch is a signed power of a nonnegative integer exponent (via six-exponentials input and the monotone-power existence theorem). In framework terms this is the discrete gate between the flat $J\equiv 0$ orbit and the nontrivial $J$-costs forced by T5 uniqueness, before leastness selects $J$ itself in Cost.UnitFromMinimality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.