PrimitiveRigidityHypotheses
plain-language theorem explainer
Packages the primitive rigidity assumption used by CPT forced factorization: for a fixed observable, the ratio coordinate is independent of state. Anyone citing uniqueness of the reparametrization on the realized cost image needs this hypothesis (or an equivalent). It is a Prop-valued structure with a single field, not a proved statement.
Claim. Given a ratio-cost scaffold $R$ on state space $S$ and observable space $O$, the primitive rigidity hypothesis asserts that for every fixed $o \in O$ and all states $s_1,s_2 \in S$, the ratio coordinate satisfies $\iota_S(s_1)/\iota_O(o) = \iota_S(s_2)/\iota_O(o)$.
background
The CPT Forced Factorization module states the paper's forced-factorization claims in hypothesis-explicit form: a ratio-induced canonical cost scaffold, certificate hypotheses written out, existence of a reparametrization on the realized cost image, and state-independence only under an explicit rigidity hypothesis. No hidden assumptions are used.
A ratio-cost scaffold supplies positive embeddings $\iota_S : S \to \mathbb{R}$ and $\iota_O : O \to \mathbb{R}$. The ratio coordinate is $r(s,o) = \iota_S(s)/\iota_O(o)$; it is the input to the canonical reciprocal cost used in factorization arguments. The sibling rigidity package at the cost level asks that the cost $C$ itself be state-independent for fixed $o$. The present structure is the weaker, ratio-level form of that demand.
proof idea
No proof body: this is a Prop-valued structure definition. It records a single field, ratio-level state collapse, namely $\forall s_1,s_2,o., r(s_1,o)=r(s_2,o)$. Downstream lemmas (primitive-to-rigidity, forced factorization from primitives) consume an instance of this structure as a named hypothesis rather than deriving the collapse.
why it matters
This is the rigidity half of the primitive hypothesis bundle for CPT forced factorization. It is consumed by primitive-to-rigidity (which lifts ratio-level collapse plus certificate data to the cost-level rigidity package) and by the strong uniqueness theorem forced-factorization-unique-of-primitives, which concludes existence and uniqueness of a reparametrization $\varphi$ on the realized cost codes. The export CPT_FACTOR_forced_factorization_unique_of_primitives re-exports that uniqueness under the same primitive pair. In the module's design, state-independence is never smuggled in: it appears only when this hypothesis (or the cost-level rigidity package) is supplied. That keeps the Lean layer aligned with the paper's claim that factorization uniqueness is conditional on explicit rigidity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.