Pith. sign in
module module moderate

IndisputableMonolith.Chemistry.Nematic3_Order_Param_FromJCost

show as:
view Lean formalization →

Defines a three-fold nematic order parameter built from the RS J-cost on a domain, together with a nonnegativity lemma, a canonical positive threshold, and an inhabited certificate type Nematic3Cert. Chemists or condensed-matter theorists working in the RS chemistry layer would cite it when they need a J-derived scalar that flags nematic order. The module is mostly definitions plus elementary positivity and equality facts.

claimOn a domain equipped with the Recognition Science cost $J$, define a domain cost functional, prove it is nonnegative and agrees with pointwise evaluation, fix a canonical positive threshold, and package these data into an inhabited certificate $\mathrm{Nematic3Cert}$ for three-fold nematic order.

background

Recognition Science measures mismatch by 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$; Constants supplies the RS-native tick $\tau_0$.

In the chemistry layer one needs a scalar order parameter that detects three-fold nematic alignment. This module lifts $J$ to a domain-level cost (domainCost), records that the lift is nonnegative and coincides with pointwise evaluation, and introduces a fixed positive canonical threshold against which the cost is compared. The resulting data are bundled as Nematic3Cert.

The setting is purely kinematic: no dynamical equations or microscopic Hamiltonian appear; only the cost geometry and a threshold comparison.

proof idea

Definition-heavy module. domainCost is introduced as the domain lift of $J$; domainCost_at_eq and domainCost_nonneg are short algebraic or pointwise arguments from the known nonnegativity of $J$. canonicalThreshold is a concrete positive constant; canonicalThreshold_pos is immediate positivity. Nematic3Cert packages the cost and threshold; cert and cert_inhabited supply a default inhabited instance. No deep tactic scripts; the argument is definitional plus elementary positivity.

why it matters in Recognition Science

Supplies the chemistry-side order-parameter primitive that later RS chemistry developments can use to mark three-fold nematic phases without leaving the J-cost geometry. It sits downstream of Cost (T5 J-uniqueness) and Constants, and keeps the chemistry layer aligned with the same cost that forces $\phi$, the eight-tick octave, and $D=3$. No downstream consumers are recorded yet in the mirror graph; the module is infrastructure for future nematic or liquid-crystal certificates in IndisputableMonolith.Chemistry.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)