PRCStructuralNativeCostHypotheses
plain-language theorem explainer
The structural ledger packages base native-cost axioms (reciprocity, normalization invariance, RCL, unit-zero, orbit-2 anchor) with sign reversal, monotonicity on positive integer orbits, and zero-orbit calibration of the doubled trace. Cost-classification and uniqueness proofs in the PRC native layer cite this bundle as the working hypothesis set. It is a Prop-structure definition: the four fields are the content; there is no proof body.
Claim. For a map $F$ from rational orbits to rational orbits, the structural native-cost hypotheses assert four packages: (i) the base native axioms (reciprocity $F(q)\sim F(q^{-1})$, normalization invariance, the nonzero composition law, unit-zero, and the single orbit-$2$ anchor); (ii) sign reversal $F(-q)=-F(q)-2$; (iii) monotonicity of $F$ on positive integer orbits under the display order; (iv) zero-calibration of the doubled trace $T=2(F+1)$ at the zero orbit.
background
A rational orbit is an integer numerator over a nonzero orbit denominator: the discrete display surface on which PRC-native cost lives before real completion. The base native package (reciprocity, normalization invariance, the nonzero composition law, unit-zero, and the single orbit-2 anchor) is the discrete stand-in for the continuous J-cost axioms; the orbit-2 anchor rules out the identically-zero cost until internal real completion exists.
Sign reversal says that flipping orientation of a distinction negates the doubled trace: with $T=2(F+1)$, one has $T(-q)=-T(q)$, written on displays as $F(-q)=-F(q)-2$. Monotonicity restricts to positive integer orbits and requires that cost not decrease as the imbalance grows. Zero-calibration fixes the doubled-trace convention at the zero orbit.
Relative to the round-2 slim ledger, the countable prime-pair product family and the signed-unit calibration are both dropped; nothing that replaces them mentions the canonical cost by name. The structural ledger is therefore a thinner, more intrinsic hypothesis set.
proof idea
No proof: this is a Prop-valued structure definition. It conjoins four named hypothesis packages as fields on a map $F$ from rational orbits to rational orbits. Inhabitants are built by supplying proofs of each field (as in the non-vacuity theorem for the canonical selected native cost). Downstream theorems pattern-match on the bundle and project the needed field.
why it matters
This is the working hypothesis object for the structural uniqueness program in the PRC native-cost layer. The uniqueness target is exactly: every $F$ satisfying the structural ledger agrees with the on-orbit cost in cross-display. From that target one derives that the attached character is the identity on positive integer orbits (the round-5 engine), that positivity is a theorem rather than an axiom, and that the prime-pair product family is redundant against monotonicity (every structural inhabitant already satisfies the full slim ledger).
An equivalence theorem identifies the structural ledger with the anchor-free ledger plus the orbit-2 anchor, so later arguments can treat the last field separately. Non-vacuity is witnessed by the canonical selected native cost. In the broader Recognition chain this is the discrete ledger that forces the unique J-shaped cost (T5 / RCL) on the rational surface before continuous completion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.