certificate_depends_on_ratio
plain-language theorem explainer
Equal ratio coordinates force equal certificate values whenever the certificate hypotheses hold. CPT factorization arguments cite this to reduce cost comparison to the ratio scaffold. The proof is a one-line field projection from the hypothesis bundle.
Claim. Let $R$ be a ratio-cost space on state type $S$ and observer type $O$, and let $C:S\to O\to\mathbb{R}$ be a certificate cost. If the certificate hypotheses hold for $(R,C)$, then for all $s_1,s_2\in S$ and $o_1,o_2\in O$, equality of the ratio coordinates $r_R(s_1,o_1)=r_R(s_2,o_2)$ implies $C(s_1,o_1)=C(s_2,o_2)$.
background
The module is the hypothesis-explicit Lean layer for CPT forced factorization: ratio-induced canonical cost, certificate hypotheses stated openly, reparametrization only on the realized cost image, and state-independence only under an explicit rigidity hypothesis. No hidden assumptions are used.
A RatioCostSpace supplies positive real embeddings $\iota_S:S\to\mathbb{R}{>0}$ and $\iota_O:O\to\mathbb{R}{>0}$. The ratio coordinate is the positive real $r_R(s,o)=\iota_S(s)/\iota_O(o)$ that feeds the canonical reciprocal cost (the J-cost scaffold used throughout Recognition Science). Certificate hypotheses package two dependence axioms on a map $C:S\to O\to\mathbb{R}$: ratio-level dependence (equal ratio implies equal $C$) and the stronger cost-level dependence (equal canonical cost implies equal $C$).
Upstream cost constructions (observer J-cost on recognition events, multiplicative-recognizer derived cost, PRC quotient J-cost, rung-coarsened weighted sums) all instantiate the same pattern: cost is a function of a positive ratio. This lemma isolates the ratio-level half of that pattern as an explicit, reusable projection.
proof idea
One-line term proof: the goal is definitionally the depends_on_ratio field of the CertificateHypotheses structure, so the proof is just h.depends_on_ratio. No rewriting, no external lemmas.
why it matters
In the CPT forced-factorization program, certificates must factor through the ratio scaffold before any monotone reparametrization on the realized cost image can be stated. This declaration is the named, citable form of that ratio-level dependence axiom: it turns a structure field into a theorem that downstream factorization and rigidity arguments can apply by name.
The module pairs it with the stronger cost-level dependence and with existence of a reparametrization onto CostCode R (not all of $\mathbb{R}$), keeping surjectivity claims honest. Framework-wise it sits under the J-uniqueness / RCL cost layer (T5): once cost is forced to be a function of the positive ratio, equal ratios must give equal certificates. No downstream users are wired yet in the graph; the lemma is infrastructure for the factorization and rigidity bundles in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.