Pith. sign in
module module low

IndisputableMonolith.Physics.Structural_Physics_mod26

show as:
view Lean formalization →

Module packaging domain-level cost, a canonical positive threshold, and the StructPhysicsM26Cert bundle for structural physics (mod 26). RS structural-layer work cites the nonnegativity and threshold-positivity facts. Content is mostly definitions plus short positivity lemmas drawn from the Cost import.

claimDefines a domain cost $C_{\mathrm{dom}}$, equality and nonnegativity facts for it, a canonical threshold $\theta_{\mathrm{can}}>0$, and an inhabited certificate $\mathrm{StructPhysicsM26Cert}$ packaging those structural-physics (mod-26) inequalities.

background

Recognition Science measures mismatch with the J-cost from the Cost module (the unique symmetric cost forced by the Recognition Composition Law). Constants supplies the RS-native tick $\tau_0=1$. This physics module sits above those imports and specializes cost language to a domain-level functional used in the structural (mod-26) layer.

Sibling definitions introduce domainCost (a cost assigned to a domain configuration), its evaluation identity and nonnegativity, and canonicalThreshold with a positivity lemma. The certificate type StructPhysicsM26Cert bundles those facts so downstream structural arguments can assume a single inhabited package rather than re-proving elementary cost inequalities.

The local setting is structural physics inside the RS monolith: cost nonnegativity and a fixed positive threshold that gate when a configuration is treated as structurally admissible, before mass-ladder or coupling numerics are attached.

proof idea

Definition-heavy module. Core objects (domainCost, canonicalThreshold, StructPhysicsM26Cert) are defs or structures. Supporting lemmas are short: nonnegativity of domain cost and positivity of the canonical threshold, obtained by reduction to the imported Cost API and elementary real arithmetic. cert_inhabited supplies a witness that the certificate type is nonempty. No deep tactic development; the argument is packaging plus positivity.

why it matters in Recognition Science

Gives the structural-physics (mod-26) layer a single certificate surface for domain cost and threshold facts, so later physics modules need not reopen Cost lemmas. No downstream edges are wired in the current graph (used_by empty), so this is presently a leaf package rather than a step inside T0–T8 forcing, the mass ladder, or the alpha band. It still aligns with the RS pattern of isolating cost nonnegativity and positive thresholds before geometric or coupling claims. Parent consumers would be structural admissibility or mod-26 consistency theorems once those imports land.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)