phi_independent_of_state
plain-language theorem explainer
Under an explicit rigidity hypothesis, a two-argument certificate cost C(s,o) collapses to a single state-free profile ψ(o). Anyone citing the CPT forced-factorization rigidity step (paper Thm. 5.1) needs this existence statement. The proof is a one-line witness: evaluate C at the default state and invoke state-independence.
Claim. Let $S$ be inhabited and $O$ any type. Fix a ratio-cost scaffold $R$ on $(S,O)$ and a certificate $C:S\to O\to\mathbb{R}$. If the rigidity hypothesis holds (i.e. $C(s_1,o)=C(s_2,o)$ for all states $s_1,s_2$ and all $o$), then there exists a state-free profile $\psi:O\to\mathbb{R}$ such that $C(s,o)=\psi(o)$ for every $s$ and $o$.
background
The module is the hypothesis-explicit Lean layer for CPT forced factorization: ratio-induced canonical cost, certificate hypotheses stated openly, cost-image reparametrization, and state-independence only under an explicit rigidity bundle. No hidden assumptions are smuggled in.
A RatioCostSpace supplies positive real embeddings of the state type $S$ and the observable type $O$, giving the ratio coordinate that feeds the canonical reciprocal cost. The certificate is an arbitrary map $C:S\to O\to\mathbb{R}$.
RigidityHypotheses is the Prop bundle whose sole field is state-independence: $C(s_1,o)=C(s_2,o)$ for all pairs of states and every observable. The present theorem is the existential packaging of that field: a single profile $\psi$ that forgets the state argument entirely.
proof idea
Term-mode existence proof. Because $S$ is inhabited, pick the default state and define the witness $\psi(o):=C(\mathrm{default},o)$. For arbitrary $s$ and $o$, the rigidity field independent_of_state applied to $(s,\mathrm{default},o)$ yields $C(s,o)=C(\mathrm{default},o)=\psi(o)$. No further lemmas are required.
why it matters
This is the rigidity half of the CPT forced-factorization package. Downstream it is re-exported as CPT_FACTOR_phi_independent_of_state ("State-independence under explicit rigidity hypothesis (paper Thm. 5.1 rigidity step)") and is an input hypothesis to both the in-module forced_factorization and the assembled export CPT_FACTOR_forced_factorization ("Assembled forced-factorization theorem (paper Thm. 5.1)").
In the Recognition framework the point is claim honesty: factorization of the certificate into a pure observable profile is not free; it is gated on an explicit rigidity hypothesis. The module doc stresses that state-independence appears only under that hypothesis, keeping the Lean shape aligned with the paper's strongest currently defensible claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.