cert_inhabited
plain-language theorem explainer
The RS summary certificate packing three structural cost properties is inhabited: domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Anyone citing the Plan-v7 summary certificate uses this existence fact. The proof is a one-line term witness from the already-built certificate value.
Claim. The type of RS summary certificates is nonempty: there exists a package asserting (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$, (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and (iii) the canonical threshold is strictly positive.
background
This module is the Plan-v7 structural summary certificate for Recognition Science: one functional equation $J(x)=(x+x^{-1})/2-1$ forced by four axioms, with the usual cascade (phi fixed point, gap-45, $D=3$, derived constants). Status is structural theorem, zero sorry and zero axiom.
The certificate structure bundles three elementary facts about the domain cost (the two-argument cost built from the RS $J$-cost) and the canonical threshold. Domain cost vanishes when the two arguments agree and nonzero; it is nonnegative for positive measure and expectation; the threshold used as a comparison scale is positive. Those three propositions are the fields of the structure; the present theorem only asserts that at least one such package exists.
proof idea
One-line term proof. The sibling value cert already assembles the three field proofs into an element of the certificate structure. The theorem is exactly Nonempty.intro applied to that witness: ⟨cert⟩. No further rewriting or case analysis.
why it matters
Closes the existence half of the Plan-v7 summary certificate in Foundation. Downstream consumers that need a single inhabited Prop packing diagonal vanishing, nonnegativity, and positive threshold can cite this rather than re-proving the three fields. It sits under the module claim that $J$ is uniquely forced and that the usual RS cascade (phi, eight-tick octave, $D=3$, constant band) follows; it does not itself re-derive those landmarks. With empty used-by in the current graph it functions as a terminal packaging lemma for the summary session.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.