RSForcingChain003Cert
plain-language theorem explainer
Certificate structure for RS forcing-chain module 3 (gap-45 at D=3): diagonal domain cost vanishes, domain cost is nonnegative on positive arguments, and the canonical threshold is positive. Downstream code cites it to build and inhabit the module certificate. Pure structure definition; fields are filled by sibling lemmas, not proved here.
Claim. A certificate for forcing-chain module 3 is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals $0$; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Foundation RS Module 3 treats the Recognition Science gap $g_D=D^2(D+2)=45$ at spatial dimension $D=3$, called the minimum depth for self-reference. The module is marked structural (zero sorry, zero axioms).
Domain cost is the local cost on pairs of real parameters (a measure scale and an event scale). The canonical threshold is a fixed positive real cutoff used in the module's forcing steps. The structure packages three Prop obligations on these objects rather than proving them.
Upstream, ObserverForcing records that every recognition-event cost is nonnegative, via nonnegativity of the J-cost on positive states. That global fact is the conceptual ancestor of the local nonnegativity field here.
proof idea
No proof body: this is a structure declaration. The three fields are typed propositions. The inhabitant cert fills them by assigning the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. cert_inhabited then wraps that inhabitant to show the type is nonempty.
why it matters
Earns its place as the typed interface for module-3 cost and threshold facts in the RS forcing chain. Downstream, cert constructs a concrete value and cert_inhabited proves Nonempty of the certificate, locking the structural status of the gap-45 module.
In the broader chain, D=3 is forced at T8 and the eight-tick octave (period $2^3$) sits at T7; gap $g_D=45$ is the self-reference depth tied to that dimension. The certificate does not itself force D or derive $g_D$, but it is the Lean handle that later steps cite when those identities are needed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.