structural_iff_sansAnchor_and_two_calibrated
plain-language theorem explainer
The full structural native-cost ledger on a map F of ratio orbits is equivalent to the same ledger with the orbit-2 anchor stripped, conjoined with the single calibration that F fixes the orbit of two. Anyone working the PRC uniqueness or gauge-orbit analysis cites this to isolate the anchor as an independent last field. The proof is a pure structure-field shuffle: unpack and repack the nested hypotheses both ways.
Claim. For any map $F$ on ratio orbits, $F$ satisfies the structural native-cost ledger (reciprocity, normalization invariance, canonical RCL, unit-zero, orbit-2 anchor, sign reversal, monotonicity, and zero-orbit calibration) if and only if $F$ satisfies that same ledger without the orbit-2 anchor and $F$ sends the orbit of two to the canonical orbit of two.
background
In the Primitive Recognition Calculus native-cost development, a candidate cost generator is a map $F$ on ratio orbits. The structural ledger packages the base native-cost axioms (reciprocity, normalization invariance, the nonzero composition law, unit-zero) together with sign reversal, monotonicity, and the zero-orbit convention, plus one discrete anchor: calibration on the orbit of two.
The companion structure drops only that anchor, keeping sign reversal, monotonicity, and zero calibration on top of the base axioms without two-calibration. The module's surrounding notes stress that the odd-power family $q \mapsto q^{2k+1}$ fills the anchor-free ledger, while distinct powers disagree at the anchor; the anchor is therefore the coordinate that picks one point of an infinite gauge orbit.
Locally this declaration is bookkeeping for that split: it makes precise that the structural ledger is exactly the anchor-free structural ledger plus the orbit-2 cross-equality condition.
proof idea
Bidirectional structure surgery, no external lemmas. The forward direction takes a full structural package, projects the nested native fields (reciprocal, normalized invariant, canonical RCL, unit-zero) together with sign reversal, monotonicity, and zero calibration into the sans-anchor structure, and peels off two_calibrated as the separate conjunct. The reverse direction rebuilds the native block by inserting the supplied two-calibration back into the base-sans-two fields, then restores sign reversal, monotonicity, and zero calibration. Both arms are pure field reassembly via constructor / rintro.
why it matters
This is the free-side bookkeeping behind the slogan that the form is forced and the unit is a choice. Downstream commentary in the same module records that the odd-power family inhabits the anchor-free ledger and that distinct members disagree at the anchor, so the gauge orbit is infinite and the anchor is the discrete coordinate on it. Isolating the anchor as an independent conjunct lets later uniqueness arguments treat monotonicity and sign reversal as the filters that kill round-3 impostors (Liouville and two-adic twists), while the remaining one-parameter family is pinned by orbit-2 calibration alone.
In the broader Recognition forcing chain this sits under the native J-cost uniqueness story (T5 J-uniqueness and the Recognition Composition Law): the structural ledger is the PRC packaging of those algebraic constraints plus orientation and order, and this iff shows the last field is precisely the unit choice. No downstream theorems yet depend on it (used_by is empty), so it is infrastructure for the gauge-orbit and uniqueness closure rather than a cited parent itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.