primitive_to_certificate
plain-language theorem explainer
If a certificate cost satisfies the primitive ratio-level package (ratio dependence, a cost-to-ratio bridge, and cost monotonicity), then it satisfies the full certificate hypotheses used for CPT factorization. Anyone citing forced factorization from primitives needs this implication. The proof is a short structure fill-in: copy two fields and derive cost-level dependence by composing the bridge with ratio dependence.
Claim. Let $R$ be a ratio-cost space on types $S,O$ and let $C:S\to O\to\mathbb{R}$. If $C$ obeys the primitive certificate package (equal ratio implies equal $C$, equal canonical cost implies equal ratio, and monotonicity in the canonical cost), then $C$ obeys the full certificate hypotheses: equal ratio implies equal $C$, equal canonical cost implies equal $C$, and the same monotonicity.
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 are used.
A RatioCostSpace supplies positive embeddings $\iota_S:S\to\mathbb{R}$ and $\iota_O:O\to\mathbb{R}$. From these one forms a ratio coordinate and a canonical reciprocal cost on pairs $(s,o)$. Certificate hypotheses package three properties of a map $C:S\to O\to\mathbb{R}$: dependence on the ratio, the stronger dependence on the canonical cost (needed for image reparametrization), and monotonicity in that cost.
The primitive bundle is weaker at the surface: it keeps ratio dependence and monotonicity, but replaces cost dependence by a bridge ratio_of_cost_eq (equal canonical costs imply equal ratios). The doc-comment states the design intent: cost-level dependence is meant to be derived from ratio-level dependence plus that bridge.
proof idea
Term-mode structure construction via refine. Two fields of CertificateHypotheses are copied verbatim from the primitive package: depends_on_ratio and monotone_in_cost.
The remaining field depends_on_cost is filled by a short intro: given equal canonical costs, apply the primitive bridge ratio_of_cost_eq to obtain equal ratios, then apply depends_on_ratio to conclude equal certificate values. No external lemmas are needed beyond the field projections of the hypothesis structures.
why it matters
This is the hinge that lets the strong forced-factorization theorem run from primitive ratio-level assumptions rather than from the stronger cost-level package. Downstream, forced_factorization_unique_of_primitives takes PrimitiveCertificateHypotheses (and a primitive rigidity package) and concludes unique factorization through a cost code; it relies on this implication to reach the certificate layer where reparametrization existence is stated.
In the Recognition verification stack, CPT factorization is the check that observable certificates factor through the canonical J-cost geometry on ratios. Making the primitive-to-certificate step explicit keeps the paper's claim honest: cost dependence is not an extra axiom when the cost-to-ratio bridge is present. The module's forced-factorization program (ratio scaffold, certificate hypotheses, image reparametrization, rigidity) sits downstream of the T5 J-uniqueness and RCL landmarks, but this lemma itself is pure hypothesis bookkeeping inside that verification layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.