IndisputableMonolith.Materials.Grain5
Packages the domain-cost functional, canonical threshold, and GS5 grain certificate for Recognition Science materials. Materials theorists cite it for nonnegativity of domain cost and the positive cutoff that gates grain stability. Structure is definitions plus short positivity and evaluation lemmas on top of the imported J-cost.
claimIntroduces a domain cost $C_{\mathrm{dom}}$ built from the RS $J$-cost, a canonical threshold $\theta_{\mathrm{can}}>0$, and an inhabited certificate asserting the GS5 grain inequalities in RS-native units.
background
Recognition Science materials work reuses the same cost that appears in the forcing chain. The Cost import supplies $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$); Constants supplies the RS tick $\tau_0$. Grain models treat a spatial domain as a discrete recognition structure whose defect is scored by $J$.
Domain cost aggregates that defect over the grain. The canonical threshold is the positive cutoff used to decide stability or acceptance of the GS5 configuration. Sibling facts record the value of domain cost at distinguished points, prove nonnegativity, and package the GS5 claim as a certificate type with an inhabitation witness.
proof idea
Definition-and-lemma module, not a deep derivation. Domain cost is defined from the imported cost functional; evaluation-at-equality and nonnegativity are short algebraic facts. Canonical threshold is a positive constant (positivity lemma). GrainGS5Cert and the inhabited cert wrapper package the GS5 inequalities as a certificate structure rather than a long tactic proof.
why it matters in Recognition Science
Sits in the Materials domain of the RS monolith and standardizes how a grain model (GS5) is scored and certified against the $J$-cost. The certificate pattern matches other RS cert objects: a named structure plus inhabitation. No downstream used-by edges are recorded in the graph yet, so the module is presently a leaf packaging layer for grain-threshold claims rather than a step inside T0–T8. It keeps materials statements aligned with RS-native units ($c=1$, cost from $J$, tick from Constants) instead of ad hoc continuum energies.
scope and limits
- Does not derive continuum elastic moduli or PDE grain-boundary limits.
- Does not prove GS5 is the unique admissible grain model.
- Does not match experimental grain-boundary energies outside RS units.
- Does not extend the T0–T8 forcing chain; materials packaging only.
- Does not supply dynamics or time evolution of grains.