PRCStructuralNativeCostHypothesesSansAnchor
plain-language theorem explainer
Anchor-free structural ledger for a native cost map F on ratio orbits: reciprocal/normalization base, sign reversal F(-q)=-F(q)-2, monotonicity on positive integer orbits, and zero-calibration of the doubled trace. Cited by gauge-orbit classification and real-character factorization. Pure Prop structure bundling four fields; no proof content.
Claim. A map $F$ from ratio orbits to ratio orbits satisfies the anchor-free structural native-cost hypotheses when (i) it is reciprocal and normalization-invariant, (ii) orientation reversal gives $F(-q)=-F(q)-2$, (iii) on positive integer orbits cost is nondecreasing in the imbalance, and (iv) the doubled trace $T=2(F+1)$ is zero-calibrated.
background
Ratio orbits are rational displays: signed-orbit numerator over a nonzero distinction-nat denominator. Native cost is a map $F$ on those orbits; the doubled trace is $T=2(F+1)$. The Recognition Composition Law and J-uniqueness (T5) force the continuum cost shape; here the discrete ledger records which algebraic properties a candidate $F$ must obey before continuum comparison.
The base pack without the two-point anchor keeps only reciprocal symmetry ($F(q)$ cross-equal to $F(1/q)$) and invariance under distinction-nat normalization. Sign reversal says reversing orientation negates the doubled trace: $T(-q)=-T(q)$, written on displays as $F(-q)=-F(q)-2$. Monotonicity restricts to positive integer orbits and requires nondecreasing cost as the rational imbalance grows. Zero-calibration pins the doubled trace at the identity orbit.
This module sits in Primitive Recognition Calculus and imports the minimality-certificate base. The two-point anchor is deliberately stripped so classification can treat every structural inhabitant before fixing the unit scale.
proof idea
Definition only: a Prop-valued structure with four fields. No tactics, no lemmas applied. Inhabitants are built by supplying proofs of the base sans-two pack, sign reversal, monotonicity, and zero-calibration of the doubled trace of $F$. Downstream theorems pattern-match on those four projections.
why it matters
This is the hypothesis interface for the anchor-free gauge-orbit story. Downstream, every structural inhabitant factors through a real ratio character, and the closed classification states that $F$ is either the zero-exponent sign cost or a sign-extended power cost at some nonnegative integer exponent. The open odd-power variant uses the same pack. Explicit inhabitants (sign gauge; every signed power) discharge the structure fieldwise, so the ledger is inhabited at every allowed exponent.
In the RS forcing chain this sits under native-cost uniqueness toward J (T5) and the continuum comparison that continuum gauges exceed the native gauge. Removing the two-point anchor isolates structural shape from unit calibration, which is what lets the signed-power family close without fixing the rung-two value early.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.