Pith. sign in
module module moderate

IndisputableMonolith.Materials.Crystal_Structure2_FromConfigDim

show as:
view Lean formalization →

Materials module that ties configuration-space dimension to three-dimensional crystal geometry via a domain cost and a positive canonical threshold. It packages a Bravais-3 certificate and proves the certificate type is inhabited. Condensed-matter or RS materials workers cite it when forcing lattice class from cost geometry rather than from empirics. The development is mostly definitions plus elementary nonnegativity and inhabitance arguments on top of the Cost import.

claimOn configuration domains one has a cost $C$ (nonnegative, with an evaluation identity at distinguished points), a strictly positive canonical threshold $\theta$, and a certificate type asserting that admissible crystal geometries are three-dimensional Bravais lattices; that certificate type is inhabited.

background

Recognition Science forces spatial dimension $D=3$ in the unified forcing chain (T8) and equips dynamics with the J-cost $J(x)=(x+x^{-1})/2-1$ from the Cost layer. Materials work asks which discrete geometries minimize recognition cost once the ambient dimension is fixed.

This module sits in the Materials domain. It imports Constants (RS time quantum $\tau_0=1$ tick) and Cost, then introduces a domain-level cost functional, its pointwise evaluation identity, and nonnegativity. A canonical threshold is defined and shown positive. Those pieces feed a Bravais-3 certificate: a propositional package that the only cost-admissible crystal structures in the forced dimension are the classical three-dimensional Bravais classes.

Sibling names indicate the local API: domain cost, threshold positivity, the certificate structure, and an inhabitance lemma that the certificate is realizable.

proof idea

Definition-heavy module rather than a single deep theorem. Domain cost is introduced and related to evaluation at canonical configurations; nonnegativity is recorded as a lemma. The canonical threshold is defined from the cost data and proved strictly positive. Bravais3Cert packages the dimensional and lattice-class constraints; cert and cert_inhabited supply a concrete witness that the certificate type is nonempty. Arguments are elementary algebraic or positivity steps on top of the Cost import, not a long tactic script.

why it matters in Recognition Science

Gives the Materials layer a cost-native route from configuration dimension to three-dimensional Bravais geometry, aligned with T8 ($D=3$) and the J-cost infrastructure. Downstream pages can assume an inhabited Bravais-3 certificate instead of postulating lattice class by hand. No further used_by edges are recorded yet, so the module presently closes a local scaffolding gap: crystal structure as a derived certificate from config-dimension and cost, ready for phonon, band, or defect developments that need a forced 3D lattice backdrop.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)