StructPhysicsM56Cert
plain-language theorem explainer
Certificate type packing three structural axioms for the physics-domain cost at recognition rung 56: diagonal vanishing, non-negativity on positive arguments, and positivity of the canonical threshold. Anyone discharging the module's structural physics prediction cites the inhabited instance of this type. Pure structure definition; no proof body.
Claim. A structural physics certificate at recognition rung 56 is a record of three properties: the domain cost of any nonzero real against itself vanishes; the domain cost of any two strictly positive reals is non-negative; and the canonical recognition threshold is strictly positive.
background
The module states a structural Recognition Science prediction for the Physics domain at recognition rung 56, with status structural theorem (zero sorry, zero axiom). Rung indexing sits on the phi-ladder used throughout RS mass and scale formulae.
The certificate refers to a domain cost on pairs of reals (mass and energy style arguments in the physics specialization) together with a canonical threshold scalar. Upstream, recognition-event cost is already known to be non-negative: "The cost of any recognition event is non-negative," via non-negativity of the J-cost $J(x)=(x+x^{-1})/2-1$ at positive state. The present fields lift that positivity discipline into a domain-level package, adding diagonal vanishing (zero self-cost) and a positive threshold cut.
proof idea
No proof body: the declaration is a structure whose three fields are propositions. Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Those lemmas, not this structure, carry the actual arguments.
why it matters
This type is the interface the module exports for its structural physics claim. The concrete witness cert assembles the three field proofs, and cert_inhabited records Nonempty of the certificate, closing the module's structural-theorem status.
In the broader RS stack, such certificates pin domain-level cost axioms before numerical mass or coupling predictions are attached. The non-negativity field echoes the foundation result that every recognition event has non-negative J-cost; diagonal vanishing encodes the identity minimum of that cost. The positive threshold is the cut used by later physics-domain comparisons. No open scaffold remains in this module once the certificate is inhabited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.