RigidityHypotheses
plain-language theorem explainer
Packages the explicit rigidity assumption that a two-argument cost C is independent of the state and depends only on the observable. Forced-factorization and state-profile uniqueness theorems take this bundle as a hypothesis so state-independence is never smuggled in. As a Prop structure it has no proof body; it is the named interface for the paper's rigidity step.
Claim. Given a ratio-cost scaffold on state space $S$ and observable space $O$, and a cost $C:S\to O\to\mathbb{R}$, the rigidity hypotheses assert $$\forall s_1,s_2\in S,\;\forall o\in O,\quad C(s_1,o)=C(s_2,o).$$ Equivalently, $C$ factors through a state-free profile $\psi:O\to\mathbb{R}$.
background
The module is the hypothesis-explicit Lean layer for CPT forced factorization: ratio-induced canonical cost, certificate hypotheses stated openly, reparametrization on the realized cost image, and state-independence only under an explicit rigidity hypothesis. No hidden assumptions.
A ratio-cost scaffold supplies positive embeddings $\iota_S:S\to\mathbb{R}{>0}$ and $\iota_O:O\to\mathbb{R}{>0}$ so that ratios enter the canonical reciprocal cost. The cost $C$ is an arbitrary real-valued map on states and observables; elsewhere in the framework recognition costs are typically $J$-costs (the unique symmetric cost $J(x)=(x+x^{-1})/2-1$), but this bundle does not fix that form.
The companion certificate-hypothesis bundle handles cost-image reparametrization. Rigidity is separated so that state-free factorization is visibly optional and auditable.
proof idea
Definitional structure, not a proved theorem. It is a single-field Prop record whose only obligation is universal state-independence of $C$ at fixed observable. Downstream lemmas (e.g. unique state-free profile) unpack the field and pick a default state when $S$ is inhabited, defining $\psi(o):=C(s_0,o)$.
why it matters
This is the named rigidity interface for paper Theorem 5.1. Export theorems CPT_FACTOR_forced_factorization, CPT_FACTOR_forced_factorization_unique, and CPT_FACTOR_phi_independent_of_state all require it alongside certificate hypotheses. In-module consumers include forced_factorization, forced_factorization_unique, existsUnique_state_profile, and the bridge primitive_to_rigidity.
Architecturally it enforces claim honesty: the module doc states state-independence holds only under this explicit hypothesis. That keeps the CPT factorization chain from silently assuming $C$ is already a function of the observable alone, which would collapse the two-layer (cost-code reparametrization plus state-free profile) story. It does not itself invoke T5–T8 or the RCL; it is a verification-layer hypothesis shape those physics landmarks can later discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.