StructPhysicsM66Cert
plain-language theorem explainer
A certificate bundle for the Physics structural prediction at recognition rung 66: diagonal domain cost vanishes, domain cost is nonnegative for positive mass and energy arguments, and the canonical threshold is strictly positive. Downstream code cites it as the type of the concrete `cert` witness and of the Nonempty proof. It is a pure structure definition packing three Prop fields; no proof lives here.
Claim. A structural Physics certificate at rung 66 is a record of three facts: (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 Structural_Physics_mod66 packages a structural Recognition Science prediction for the Physics domain at recognition rung 66. The module status is a structural theorem with zero sorry and zero axioms. The certificate is the interface that names the three numerical/analytic claims the domain must satisfy.
Domain cost is the Physics-side cost functional on pairs of reals (mass- and energy-like arguments). Its diagonal vanishing and nonnegativity mirror the global J-cost story: upstream, ObserverForcing records that every recognition event has nonnegative cost via Cost.Jcost_nonneg on a positive state. The canonical threshold is the positive cutoff used by the structural prediction at this rung.
The structure does not compute those quantities; sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the three fields when the concrete witness is built.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements. Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and to the one-line Nonempty theorem that wraps that witness.
why it matters
In the RS structural-certificate pattern, each domain/rung module exposes a typed bundle of the minimal analytic claims the prediction needs, then proves the bundle is inhabited. This structure is that bundle for Physics at rung 66. Downstream, the concrete witness and the Nonempty theorem are typed against it, so any later consumer can depend on diagonal cost zero, cost nonnegativity, and a positive threshold without reopening the cost definitions.
It sits in the Physics domain layer rather than in the T0–T8 forcing chain itself. The link to the foundation is the shared nonnegativity ideology of recognition cost (J-cost minimum on the identity event), specialized here to a two-argument domain cost and a rung-66 threshold. No open scaffold remains in this module once the witness is filled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.