cert
plain-language theorem explainer
Packages three elementary domain-cost facts into the structural certificate for RS foundation module 1: diagonal vanishing, nonnegativity for positive arguments, and a positive canonical threshold. Anyone citing the module's structural prediction (J-cost shape, phi, D=3) can point at this inhabitant. The body is a pure structure assembly of three already-proved field lemmas.
Claim. There is a certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module RS_FDN_Structural_001 records the first structural prediction of Recognition Science: the cost is the unique J-form $J(x)=\frac12(x+1/x)-1$, phi is the golden ratio fixed point, and spatial dimension $D=3$ is forced. Status is a structural theorem block with no sorry and no axioms.
The certificate structure bundles three real-analytic side conditions on a two-argument domain cost (the local stand-in for recognition cost between a measured value and an expected value). Diagonal vanishing says matched measure and expectation cost nothing. Nonnegativity is the usual cost axiom for positive inputs. The canonical threshold is a positive cutoff used later as a recognition gate.
Upstream, ObserverForcing already proves that every recognition-event cost is nonnegative via Jcost_nonneg on a positive state; the present nonnegativity field is the domain-cost analogue of that fact.
proof idea
One-line structure inhabitant. Each field is filled by a named sibling lemma already in the module: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No further tactic work; the definition is pure record assembly.
why it matters
Gives a single named witness that the three elementary cost/threshold obligations of structural module 1 hold. Downstream consumers (none linked yet in the graph) can depend on cert rather than on the three lemmas separately, which keeps the structural theorem surface small.
In the broader forcing chain this sits under the T5 J-uniqueness landmark ($J(x)=(x+x^{-1})/2-1$) and the module claim that phi and $D=3$ are forced. It does not itself force J, phi, or dimension; it only certifies the cost-side bookkeeping those later steps rely on. Closes no open sorry; the module is already zero-sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.