cert
plain-language theorem explainer
Packages the three BIT-kernel deep-v4 side conditions (vanishing diagonal cost, nonnegativity of domain cost, positive canonical threshold) into a single certificate record. Anyone citing the deep BIT kernel from J-cost uses this inhabited witness. The body is a pure structure instance wiring three already-proved sibling lemmas.
Claim. There is a certificate asserting: (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
The module builds the deep v4 BIT kernel (bosonic vacuum fluctuations of size $J(\varphi)/45$ per recognition tick) directly from the Recognition Science J-cost. Cumulative Z-aging is the tick-sum of that per-tick cost; the structural layer here only needs the cost algebra, not the cosmological $N\sim 10^{48}$ count.
domainCost is the local cost functional on pairs of positive reals used by this kernel. The certificate structure BITKernel4DeepCert packages three elementary properties of that cost and of the fixed positive threshold that gates the kernel: diagonal vanishing, nonnegativity off the diagonal, and positivity of the threshold.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing (cost_nonneg: "The cost of any recognition event is non-negative"), via Cost.Jcost_nonneg. The present certificate is the domain-cost specialization of that idea plus the two companion facts.
proof idea
One-line structure instance. The three fields of BITKernel4DeepCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No new algebra is performed; the definition only assembles those proofs into the certificate record.
why it matters
Gives a single named witness that the deep-v4 BIT kernel's cost side-conditions hold, so later kernel theorems can take one hypothesis instead of three. Sits in the Foundation layer that derives BIT vacuum structure from J-cost (T5 J-uniqueness: $J(x)=(x+x^{-1})/2-1$). The module claims structural status (0 sorry, 0 axiom); this certificate is the packaging step that makes that claim usable. No downstream consumers are recorded yet; the natural next use is any theorem that assumes BITKernel4DeepCert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.