vanishes_at_two_iff_flat
plain-language theorem explainer
Under the anchor-free structural cost hypotheses, a ledger cost vanishes at the orbit of two if and only if it vanishes at every positive ratio orbit. Classification and nondegeneracy arguments cite this to collapse global flatness to a single-point check. The proof routes through the cost-display identity and the fact that a degenerate trace at two forces the rational trace to be identically two on positives.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free structural cost hypotheses (base without two, sign-reversing, monotone, zero-calibrated doubled trace). Then $(F(2))_{\mathbb{Q}} = 0$ if and only if $(F(q))_{\mathbb{Q}} = 0$ for every ratio orbit $q$ with positive rational value.
background
The module classifies gauge orbits of native cost maps on ratio orbits under anchor-free structural hypotheses. SansAnchorHypotheses packages base-sans-two, sign-reversing, monotonicity, and zero-calibrated doubled-trace conditions, matching the PRC structural native-cost pack without an anchor.
Cost is read through the display identity: for any such $F$ and orbit $q$, the rational value of $F(q)$ equals half the rational trace at $q$ minus one. Thus vanishing of cost is equivalent to the trace taking the degenerate value $2$. Upstream, cost vanishes at orbit two exactly when the rational trace at $2$ equals $2$; separately, if that trace equals $2$, then the rational trace equals $2$ at every positive rational.
Ratio orbits are the integer-rational orbits of the primitive recognition calculus; two is the orbit of the integer $2$. The local goal is to promote single-point freeness at two into freeness on the whole positive ray.
proof idea
Bidirectional constructor.
Forward: assume $F$ vanishes at two. For any positive-ratio orbit $q$, apply cost_display to write $(F q)_{\mathbb{Q}}$ as half the rational trace minus one. Feed vanishes_at_two_iff_trace_two into rationalTrace_pos_eq_two_of_two_eq_two to replace that trace by $2$, then norm_num yields zero; cast back to the rational equality.
Reverse: instantiate the universal statement at orbit two, using that two has positive rational value.
why it matters
This is the flatness dichotomy for the anchor-free ledger: free at two means free everywhere on positives. Downstream, strict_somewhere_iff_charges_at_two dualizes it: nondegeneracy (strict inequality somewhere among positive ratios) is exactly charging a nonzero amount at two, so the only flat monotone inhabitant is the sign cost.
The main classification theorem GaugeOrbitIsSignedPowerFamily_of_sixExponentials case-splits on whether the rational trace at two equals two; the degenerate branch is the sign gauge, and this lemma underwrites reading that branch as global vanishing of cost. In the Recognition cost story this sits under J-uniqueness (T5) and the RCL: before selecting $J$ by leastness, one must know which structural inhabitants are identically zero on positives versus signed powers. It does not itself select $J$ or force the exponent parity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.