RSForcingChain006Cert
plain-language theorem explainer
A certificate structure packaging three domain-cost axioms used in the D=3 forcing module: diagonal cost vanishes, cost is nonnegative for positive arguments, and the canonical threshold is positive. Downstream code builds a concrete inhabitant and proves the type is nonempty. The declaration is pure data; no proof lives here.
Claim. A record consisting of three properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 6 of the RS forcing chain records the structural claim that spatial dimension $D=3$ is forced by the eight-tick period $2^3$, with no free parameters (status: structural theorem, zero sorry, zero axiom).
The domain cost is the local cost functional on pairs of positive reals used in this module; its diagonal vanishes and it stays nonnegative. The canonical threshold is a positive real cutoff appearing in the same configuration. Upstream, observer-level recognition events already carry a nonnegative J-cost: "The cost of any recognition event is non-negative," obtained from nonnegativity of $J$ on positive states.
The certificate simply bundles the three numeric/cost facts the rest of the module needs before inhabiting the config.
proof idea
No proof body: this is a structure definition. The three fields are Prop-valued requirements. A later definition cert fills them by pointing at the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Nonemptiness is then immediate from that concrete record.
why it matters
This certificate is the typed interface for Module 6 of the forcing chain (T7 eight-tick octave, T8 $D=3$). Downstream, cert supplies an explicit inhabitant and cert_inhabited records Nonempty RSForcingChain006Cert, so later steps can assume the cost and threshold facts without re-proving them. It keeps the D=3 structural theorem modular: cost identity on the diagonal, cost positivity, and a positive threshold are isolated as the only local hypotheses the dimension-forcing argument consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.