Pith. sign in
module module moderate

IndisputableMonolith.Materials.RS_MAT_Structural_006

show as:
view Lean formalization →

Materials module packaging the RS-MAT structural certificate 006: a nonnegative domain cost built from the RS J-cost, a positive canonical threshold, and an inhabited certificate record tying them together. Materials and condensed-matter workers in the RS stack cite it when they need a named structural gate rather than an ad-hoc inequality. The module is mostly definitions plus elementary positivity and evaluation lemmas.

claimThe module introduces a domain cost $C$ (from the RS $J$-cost), proves $C \ge 0$ and an evaluation identity at equality cases, fixes a canonical threshold $\theta > 0$, and packages an inhabited certificate $\mathrm{Cert}_{006}$ asserting the structural materials claim that the domain cost sits relative to $\theta$ as required by RS-MAT structural item 006.

background

Recognition Science measures mismatch with the unique cost $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$), forced by the Recognition Composition Law and the T5 uniqueness step of the forcing chain. The Cost import supplies that $J$-infrastructure; Constants supplies the RS-native tick $\tau_0 = 1$ and related units.

In the materials layer, structural claims are not free-floating inequalities. They are packaged as named certificates that compare a domain-level cost functional against a fixed positive threshold. This module is the 006 entry in that structural series: it defines the domain cost, records nonnegativity and an on-equality evaluation lemma, and names the canonical threshold used as the gate.

The local setting is therefore certificate-shaped rather than dynamical: no evolution equations, only the static cost-threshold pair needed by downstream materials arguments that import RS_MAT_Structural_006.

proof idea

Definition-heavy module, not a deep proof development. The domain cost is introduced as a def from the imported Cost layer; domainCost_nonneg and domainCost_at_eq are short positivity and evaluation lemmas. The canonical threshold is a positive constant (canonicalThreshold_pos). The certificate type RSMATStructural006Cert bundles those facts; cert and cert_inhabited discharge inhabitance so callers can obtain a witness without reconstructing the inequalities. No multi-step tactic chains beyond elementary real arithmetic on $J$.

why it matters in Recognition Science

Gives the materials stack a stable, named structural gate (item 006) instead of repeating ad-hoc $J$-cost bounds. Downstream used_by edges are empty in the current graph, so this module is a leaf certificate: it is meant to be imported by later RS materials theorems that need a certified domain-cost threshold. It sits under the broader RS cost uniqueness story (T5 / RCL) and the Constants native-unit conventions, keeping materials claims aligned with the same $J$ that forces $\varphi$, the eight-tick octave, and $D = 3$ elsewhere in the monolith. Closes a scaffolding slot for structural materials bookkeeping rather than a physics derivation step.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)