cert
plain-language theorem explainer
Packages the three structural facts for the Physics domain at recognition rung 46 into a single certificate: domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Anyone citing the mod-46 structural physics prediction uses this bundle. The definition is a pure field assembly from three already-proved sibling lemmas.
Claim. The Physics-domain structural certificate at rung 46 is the triple of 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_mod46 records a structural Recognition Science prediction for the Physics domain at recognition rung 46. Status is a structural theorem with no sorry and no extra axioms.
The certificate structure bundles three properties of the local domain cost. Domain cost is the RS cost functional specialized to this physics module: it vanishes when the two arguments coincide (identity recognition) and stays nonnegative for positive mass/energy-like arguments. The canonical threshold is the positive cutoff used to separate admissible from inadmissible recognition events in this domain.
Upstream, nonnegativity of recognition cost is the standard J-cost fact: every recognition event has cost at least zero because $J$ is nonnegative on the positive reals (the identity event sits at the $J$-minimum $x=1$). The three field proofs in this module specialize that pattern to domainCost and the local threshold.
proof idea
One-line structure inhabitant. Each of the three fields is filled by the corresponding sibling lemma already proved in the same module: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No extra tactics or rewriting; pure field assignment.
why it matters
Gives a single named witness that the Physics rung-46 structural package is fully discharged. Downstream consumers (none yet wired in this graph) can take cert rather than re-proving the three cost/threshold facts. In the RS forcing picture this sits under the cost layer (T5 J-uniqueness and the Recognition Composition Law): domain cost inherits the J-shape, so diagonal zero and off-diagonal nonnegativity are the local echo of $J(1)=0$ and $J\ge 0$. The positive canonical threshold is the domain-level gate that keeps the structural prediction nontrivial. Closes the certificate side of Plan v7 pass 120 for this module; no open scaffolding remains here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.