cert
plain-language theorem explainer
Packages three elementary domain-cost and threshold facts into a single certificate for the T0–T8 forcing-chain completeness module. Anyone citing structural completeness of the J-cost forcing chain would reach for this bundle. The body is a pure structure assembly: three already-proved sibling lemmas are plugged into the certificate fields.
Claim. There is a certificate recording that the domain cost vanishes on the diagonal ($\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$), is nonnegative for positive mass and energy arguments, and that the canonical threshold is strictly positive.
background
The module aims at a structural completeness statement for the Recognition Science forcing chain T0–T8: uniqueness of the J-cost, the Recognition Composition Law, forced $\varphi$, the eight-tick period, $D=3$, and the derived constants, all from the single functional cost $J$. Status claimed in the module header is zero sorry and zero axioms.
ForcingChainComp3Cert is the local certificate type. Its three fields demand: (i) the domain cost is zero when both arguments equal a nonzero real (identity events sit at the J-minimum), (ii) domain cost is nonnegative whenever mass and energy are positive, and (iii) the canonical threshold used downstream is positive. Nonnegativity of recognition cost is the classical fact that $J\ge 0$ with minimum at $x=1$ (cf. ObserverForcing: "The cost of any recognition event is non-negative").
proof idea
Definitional structure instance, not a tactic proof. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No further rewriting or case analysis occurs; the certificate is just the named bundle of those three facts.
why it matters
Gives a single inhabited certificate object that later completeness or export layers can require instead of three separate hypotheses. It sits inside the Plan-v7 "Forcing Chain T0–T8 Completeness from J-Cost" module, whose stated goal is the full structural derivation of physical constants from $J$ (T0 J-uniqueness through T8 $\Lambda$). The certificate encodes the minimal cost-positivity and threshold hygiene needed before one can talk about forced $\varphi$, the eight-tick octave, and $D=3$. No downstream consumers are wired in this graph snapshot; the sibling cert_inhabited is the natural next witness that the type is nonempty.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.