cert
plain-language theorem explainer
Packages three Logo5 facts into one certificate: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Cited by anyone needing a single RSLogo5Cert witness for the structural Logo5 theorem. Construction is a direct field assembly of three sibling lemmas already proved in-module.
Claim. There is a Logo5 certificate recording that the domain cost satisfies $\mathrm{cost}(r,r)=0$ for every nonzero real $r$, that $\mathrm{cost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold is strictly positive.
background
The module treats the Recognition Science logo curve $J(x)=(x+1/x)/2-1$ on $(0,\infty)$ as the structural core of the framework: minimum $J=0$ at $x=1$, rising to $J(\varphi)$ at the golden ratio. Status is a structural theorem with zero sorry and zero axioms.
domainCost is the two-argument cost used on the logo plot; the certificate demands it vanish when both slots equal any nonzero $r$, and stay nonnegative for positive mass and energy. canonicalThreshold is the positive cutoff paired with that cost. Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity.
RSLogo5Cert is the structure bundling exactly those three propositions; this definition is the concrete inhabitant.
proof idea
Pure structure construction, not a tactic proof. The three fields of RSLogo5Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No further rewriting or case analysis occurs.
why it matters
Gives the single packaged witness that the Logo5 structural theorem needs: one curve $J(x)=(x+1/x)/2-1$ carrying the recognition cost story (T5 J-uniqueness in the forcing chain). The module frames this as the absolute final Logo5 session, zero sorry. No downstream users are recorded yet; the sibling cert_inhabited is the natural consumer. It does not itself derive $J$ or force $\varphi$, but freezes the certificate interface those results sit behind.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.