casimirStabilityCert
plain-language theorem explainer
Packages the Casimir geometry lower bound and the vacuum-stability bridge into a single certificate record. Anyone citing the module's claim that renormalized Casimir energy stays finite and compatible with vacuum uniqueness would point here. The body is a pure structure instance: two already-proved fields are filled by name.
Claim. There is a stability certificate whose fields assert: (i) for every positive plate separation $a$, the finite-geometry lower bound is strictly less than the renormalized ideal Casimir energy density at $a$; (ii) uniqueness of the vacuum implies vacuum stability (the existing structural schema).
background
The module treats the renormalized Casimir energy between plates: it is negative, yet finite for every positive separation. A geometry-dependent lower bound finiteGeometryLowerBound is compared against the ideal energy density, and that comparison is tied to the ambient vacuum-stability schema from VacuumStability.
CasimirStabilityCert is the structure that packages both claims: a universal strict inequality finiteGeometryLowerBound a < idealEnergyDensity a for every plate separation, and the proposition VacuumStability.uniqueness_implies_stability. Upstream, idealEnergyDensity_bounded_below proves the inequality by unfolding the lower-bound definition and a linear-arithmetic step; casimir_bound_compatible_with_vacuum_stability is a one-line bridge that re-exports the structural RS vacuum-stability result.
proof idea
Definitional structure instance, not a tactic proof. The bounded_below field is filled by the theorem idealEnergyDensity_bounded_below; the vacuum_stability_schema field is filled by casimir_bound_compatible_with_vacuum_stability, which itself is a wrapper around VacuumStability.rs_vacuum_stability_structural. No new reasoning occurs at this declaration.
why it matters
Closes the CasimirStabilityBound module by exhibiting a concrete certificate that the geometry lower bound and the vacuum-stability schema hold together. In the Recognition QFT layer this is the bookkeeping object that records "Casimir energy is bounded below and does not break vacuum uniqueness," consistent with the broader vacuum-stability story. No downstream consumers are wired yet (used_by is empty); the value is local completeness of the bound-plus-schema package rather than a step in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.