cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single BIT-kernel-3 certificate: diagonal vanishing, non-negativity on positive masses/energies, and a positive canonical threshold. Cosmologists or RS auditors citing the BIT dark-energy drift band [0, J(φ)] use this object as the structural witness. The definition is a pure structure assembly of three already-proved sibling lemmas.
Claim. There is a BIT kernel-3 certificate whose fields assert: (i) for every nonzero real $r$, the domain cost of $(r,r)$ vanishes; (ii) for all positive $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module builds the BIT kernel family v3 from the Recognition Science J-cost. Module status is structural (zero sorry, zero axiom). The physical target is BIT dark-energy drift: $\delta w_0$ lies in the closed interval $[0, J(\varphi)]$, with canonical kernel $K(z)=1/(1+z)$. At best fit $\delta w_0=0$ one recovers pure $\Lambda$; at the upper edge $\delta w_0=J(\varphi)$ the maximum BIT drift is $0.118$ in the equation of state.
Domain cost is the local cost functional on mass/energy pairs used by the kernel certificate. The structure BITKernel3Cert packages three Prop fields: diagonal vanishing of domain cost, non-negativity for positive arguments, and positivity of the canonical threshold. Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost non-negativity.
proof idea
One-line structure construction. The three certificate fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No further tactic work or algebraic reduction occurs; the definition is pure packaging.
why it matters
Gives the inhabited certificate object for BIT kernel family v3, the structural witness behind the dark-energy drift band $\delta w_0\in[0,J(\varphi)]$. That band sits on the J-cost uniqueness landmark (forcing-chain T5) and the golden-ratio fixed point $\varphi$ (T6). Downstream the sibling cert_inhabited and any kernel-family theorems that demand a BITKernel3Cert instance consume this value. No open sorry is closed here; the declaration simply materializes the already-proved field lemmas as a single named certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.