cubeGeneratedNativeCost_sansAnchor
plain-language theorem explainer
The cube-generated native cost on ratio orbits satisfies the full structural ledger with the unit anchor stripped: base hypotheses without two-point calibration, sign-reversal, monotonicity, and zero-calibrated doubled trace. Anyone arguing that the anchor is a genuine gauge choice (not forced structure) cites this witness. Proof is a one-line specialization of the odd-power family at parameter 1.
Claim. Let $F$ be the cube-generated native cost map on ratio orbits. Then $F$ satisfies the anchor-free structural native-cost ledger: the base native-cost hypotheses without two-point calibration, sign-reversal, monotonicity, and zero-calibration of the doubled trace of $F$.
background
In the Primitive Recognition Calculus, a native cost is a map $F$ on ratio orbits whose doubled-trace and comparison properties encode the J-cost structure forced by the Recognition Composition Law. The structural ledger packages the properties that are genuinely forced (base axioms, sign-reversal, monotonicity, zero-calibration of the doubled trace) separately from a final unit-fixing anchor.
PRCStructuralNativeCostHypothesesSansAnchor is exactly that package with the anchor field removed: base without two-calibration, sign-reversing, monotone, and zero-calibrated doubled trace. The cube-generated map is the $k=1$ member of the odd-power family of native costs (odd powers $2k+1$), sitting next to the canonical cost as a gauge sibling rather than an impostor.
Upstream cost notions (observer J-cost on recognition events, multiplicative-recognizer derived cost, rung-coarsened weighted sums) supply the ambient language; this module isolates which of those properties survive without fixing the unit.
proof idea
One-line term proof: instantiate the already-proved odd-power certificate oddPowerGeneratedNativeCost_sansAnchor at parameter $1$. That lemma shows every odd-power generator meets the sans-anchor structural ledger; the cube case is exactly the $k=1$ slot, so no extra algebra is needed here.
why it matters
This witness is the concrete counterexample fed into PRCStructuralSansAnchorUniquenessTarget_refuted, whose doc-comment states the punchline: the anchor is a genuine unit gauge; the anchor-free structural ledger does not force the canonical cost; everything else is structure and the last field is a choice of unit.
In the Recognition forcing chain, T5 fixes the J-cost shape and the RCL constrains composition, but units remain a gauge. Showing that cube-generated native cost clears every structural field without the anchor separates forced ledger content from calibration. That separation keeps the uniqueness target honest: uniqueness holds only after the anchor is restored, not from structure alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.