primitive_to_rigidity
plain-language theorem explainer
From ratio-level certificate dependence and ratio-state collapse, the cost functional is independent of the state variable. CPT factorization proofs cite this to upgrade primitive rigidity into the explicit state-independence bundle. The argument is a one-field structure refine: equal ratios imply equal costs.
Claim. Let $R$ be a ratio-cost space on types $S,O$ and let $C:S\to O\to\mathbb{R}$. If $C$ depends only on the ratio coordinate of $R$, and if for every fixed $o\in O$ the ratio $R(s,o)$ is independent of $s\in S$, then $C(s_1,o)=C(s_2,o)$ for all $s_1,s_2\in S$ and $o\in O$.
background
The module is the hypothesis-explicit Lean layer for CPT forced factorization: ratio-induced canonical cost, certificate hypotheses stated openly, and state-independence only under an explicit rigidity hypothesis. No hidden assumptions.
A RatioCostSpace supplies positive real embeddings of states $S$ and observables $O$; the ratio coordinate is the quotient of those embeddings and feeds the canonical reciprocal cost. Primitive certificate hypotheses assert that equal ratios force equal costs $C$ (plus a cost-to-ratio bridge and monotonicity). Primitive rigidity is the ratio-level collapse: for fixed $o$, $\mathrm{ratio}(s_1,o)=\mathrm{ratio}(s_2,o)$ for all states. The target rigidity bundle is simply state-independence of $C$ itself.
proof idea
Term-mode structure construction. Refine the single field independent_of_state of RigidityHypotheses. For arbitrary $s_1,s_2,o$, apply primitive ratio-state collapse to obtain equal ratios, then feed that equality into the primitive certificate's depends_on_ratio clause to conclude $C(s_1,o)=C(s_2,o)$. No further lemmas.
why it matters
Feeds forced_factorization_unique_of_primitives, the strong forced-factorization theorem from primitive ratio-level assumptions (unique reparametrization $\varphi$ on the realized cost image). The module's design goal is to keep rigidity explicit rather than smuggled; this bridge converts the ratio-phrased collapse into the cost-level independence that uniqueness needs. It sits in the verification layer for CPT factorization, not in the T0–T8 forcing chain, but it is the clean interface between primitive ratio data and the certificate/rigidity packages used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.