PrimitiveCertificateHypotheses
plain-language theorem explainer
A Prop-valued hypothesis bundle for CPT cost reparametrization, stated at the ratio level rather than the cost level. It packages three axioms: the observed cost depends only on the ratio coordinate, equal canonical costs imply equal ratios, and the cost is monotone in the canonical cost at fixed state. Downstream uniqueness theorems cite it to derive the ordinary certificate bundle and force a unique reparametrization on the realized cost image.
Claim. Fix a ratio-cost scaffold $R$ on state space $S$ and observable space $O$, and a cost $C:S\times O\to\mathbb{R}$. The primitive certificate hypotheses assert: (i) equal ratios imply equal costs; (ii) equal canonical reciprocal costs imply equal ratios; (iii) at fixed state, $C$ is monotone in the canonical cost.
background
The module is the hypothesis-explicit Lean layer for CPT forced factorization: ratio-induced canonical cost, certificate hypotheses stated openly, existence of a reparametrization on the realized cost image, and state-independence only under an explicit rigidity hypothesis. No hidden assumptions.
A RatioCostSpace supplies positive embeddings $\iota_S:S\to\mathbb{R}{>0}$ and $\iota_O:O\to\mathbb{R}{>0}$. The ratio coordinate is the quotient of those embeddings; the canonical cost is the reciprocal cost built from that ratio (the usual $J$-style scaffold used by CPT factorization). The ordinary certificate bundle asks that $C$ depend only on cost; this structure pushes the same demand one level down, to ratios, and adds a cost-to-ratio bridge so dependence-on-cost becomes a derived fact.
proof idea
No proof body: this is a structure (Prop bundle) with three fields. The fields are the mathematical content. Downstream, primitive_to_certificate is a one-line constructor that copies depends_on_ratio and monotone_in_cost, then derives the missing cost-level dependence from depends_on_ratio plus ratio_of_cost_eq. The rigidity companion is assembled similarly via primitive_to_rigidity.
why it matters
This is the primitive entry point for the paper's forced-factorization uniqueness claim. forced_factorization_unique_of_primitives (and the export CPT_FACTOR_forced_factorization_unique_of_primitives) take this bundle plus primitive rigidity and conclude there is a unique reparametrization $\varphi$ on the realized cost codes. Internally those theorems call primitive_to_certificate to recover the ordinary H1/H2 certificate hypotheses, so the ratio-level package is strictly stronger and more economical as an assumption surface.
In the Recognition framework this sits in the verification layer that polices how physical costs may be rewritten once the ratio scaffold is fixed. It does not itself invoke T5–T8 or the RCL; it only constrains the cost-reparametrization step that those landmarks feed into when CPT factorization is checked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.