CertificateHypotheses
plain-language theorem explainer
Bundles three explicit hypotheses on a certificate functional C relative to a ratio-cost scaffold: C is constant on equal ratio coordinates, constant on equal canonical costs, and monotone in canonical cost at fixed state. Downstream CPT forced-factorization theorems (paper Thm. 5.1) take this bundle as input. Pure Prop structure; no proof content.
Claim. Fix a ratio-cost scaffold $R$ on types $S,O$ and a certificate $C:S\to O\to\mathbb{R}$. The certificate hypotheses assert: (i) $\mathrm{ratio}_R(s_1,o_1)=\mathrm{ratio}_R(s_2,o_2)$ implies $C(s_1,o_1)=C(s_2,o_2)$; (ii) equal canonical costs imply equal $C$; (iii) for each fixed $s$, $C(s,\cdot)$ is monotone nondecreasing in the canonical cost.
background
The module is the hypothesis-explicit Lean layer for CPT forced factorization: ratio-induced canonical cost scaffold, certificate assumptions stated openly, existence of a reparametrization on the realized cost image, and state-independence only under a separate rigidity hypothesis. No hidden assumptions.
A RatioCostSpace on types $S$ (states) and $O$ (observables) supplies positive real embeddings $\iota_S$, $\iota_O$. From these one forms a ratio coordinate and a canonical reciprocal cost (the doubled $J$-style cost on that ratio). The certificate $C$ is an arbitrary real-valued functional of state and observable; the three fields below constrain how $C$ may depend on those coordinates.
Upstream cost constructions (multiplicative-recognizer derived cost, rung-coarsen total recognition cost, calibration self-similar dressings) motivate why a certificate should factor through ratio or canonical cost, but this structure does not import those theorems as axioms.
proof idea
Definitional Prop structure, not a theorem. The three fields are named hypotheses: ratio-level functional dependence, the stronger cost-level dependence (used for image reparametrization existence), and monotonicity in canonical cost at fixed state. Instantiation is by supplying proofs of those three properties; projection lemmas such as certificate_depends_on_ratio simply unpack the first field.
why it matters
This is the explicit assumption pack for paper Thm. 5.1's factorization and monotone-reparametrization layer. Downstream, exists_monotone_reparam and the export CPT_FACTOR_exists_monotone_reparam take it as the sole hypothesis and produce a monotone profile on the realized cost image (CostCode). The assembled theorems CPT_FACTOR_forced_factorization and CPT_FACTOR_forced_factorization_unique combine it with a separate rigidity bundle to force state-free factorization with uniqueness.
In the Recognition framework this keeps the CPT verification chain honest: ratio/cost dependence and monotonicity are not smuggled in. It sits under the broader forcing story (T5 $J$-uniqueness and the Recognition Composition Law supply the canonical cost shape) without claiming those laws here. Open question touched: whether physical certificates automatically satisfy the three fields, or only after rigidity is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.