SansAnchorHypotheses
plain-language theorem explainer
Packages the four structural axioms on a ratio-orbit map F that replace the two-point anchor: reciprocal RCL base, sign reversal, monotonicity on positive integer orbits, and zero-calibration of the doubled trace. Downstream gauge-orbit classification cites this pack as the sole hypothesis bundle. As a Prop structure it is pure packaging, not a proved statement.
Claim. A map $F$ from rational orbits to rational orbits satisfies the anchor-free native-cost hypotheses when (i) it obeys the reciprocal, normalization-invariant Recognition Composition Law pack without a two-point calibration, (ii) $F(-q)=-F(q)-2$ whenever the displays are opposite, (iii) $F$ is monotone on positive integer orbits, and (iv) the doubled trace $T=2(F+1)$ is zero-calibrated.
background
In the Primitive Recognition Calculus, costs are maps on RatioOrbit displays (signed numerator over a nonzero distinction denominator). The Recognition Composition Law on such maps is the algebraic skeleton of the J-cost $J(x)=(x+x^{-1})/2-1$. The full structural native-cost pack usually includes a two-point anchor that fixes the value at orbit two; the present module works without that anchor.
BaseSansTwo is exactly the RCL pack stripped of two_calibrated: reciprocity $F(q)\sim F(q^{-1})$, invariance under distinction normalization, and the canonical RCL identity on products and quotients. Sign reversal encodes orientation flip on the doubled trace: $T(-q)=-T(q)$, written on displays as $F(-q)=-F(q)-2$. Monotonicity says cost does not decrease as positive integer imbalance grows. Zero-calibration of nativeCostDoubledTrace F pins the doubled trace at the zero display.
The module sits in Cost.RealCharacterFactorization and imports the PRC native-cost uniqueness and real-trace root layers, so these four fields match the foundation ledger's PRCStructuralNativeCostHypothesesSansAnchor interface.
proof idea
No proof body: this is a Prop-valued structure bundling four named fields. Inhabitation is by supplying proofs of BaseSansTwo F, sign-reversal, monotonicity, and zero-calibration of the doubled trace. Downstream lemmas project the fields (e.g. hS.sign_reversing) rather than re-proving the pack.
why it matters
This pack is the single hypothesis interface for the gauge-orbit classification of native costs. Downstream results in GaugeOrbitClassification all take SansAnchorHypotheses F: cost at zero is pinned by sign reversal alone; negative displays reduce to positive ones; nondegeneracy is equivalent to excluding the pure sign gauge; a nondegenerate inhabitant charges positively at orbit two; and on the nontrivial branch the cost is $J$ of a power character extended from the integers to every positive rational.
By dropping the two-point anchor, the classification separates the RCL-plus-symmetry skeleton from the calibration that would force the classical J-cost at a single scale. That separation is what lets the real-character factorization identify power-law characters and the degenerate sign branch without presupposing T5 J-uniqueness at the two-point. The pack therefore feeds the cost side of the forcing chain while remaining compatible with the foundation uniqueness theorems that restore full J when anchors return.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.