Pith. sign in
module module low

IndisputableMonolith.Physics.CondensedMatterPhasesFromConfigDim

show as:
view Lean formalization →

Catalogues condensed-matter phases as discrete labels forced by configuration dimension in Recognition Science, together with a count and a certificate that the enumeration is complete. A condensed-matter theorist or RS auditor would cite it when linking phase taxonomy to the D=3 forcing step. The module is definitional: an inductive phase type, a cardinality lemma, and a cert bundle; no deep analytic proof.

claimThe module introduces a finite type of condensed-matter phases derived from configuration dimension, a count of those phases, and a certificate asserting that the enumeration matches the RS-forced phase list in $D=3$.

background

Recognition Science forces spatial dimension $D=3$ at step T8 of the unified forcing chain, after the eight-tick octave (period $2^3$) and the golden-ratio fixed point $\phi$. Configuration space in that dimension supports only a discrete set of stable condensed-matter phase labels once the recognition cost $J$ and the ladder structure are fixed.

The module sits in the Physics domain and imports only Mathlib and the RS Constants layer (where the native time quantum is $\tau_0=1$ tick). It does not re-derive $D=3$; it consumes that landmark and turns it into an explicit phase taxonomy.

Sibling objects are an inductive (or enumerated) type of phases, a natural-number count of inhabitants, and a certificate structure packaging the claim that the count and the labels are the complete RS list.

proof idea

This is a definition module with light certification, not a deep proof development. It declares the phase type, proves (or computes) that its cardinality equals a fixed natural number, and packages both into a certificate record. Any nontrivial content is by direct case analysis or rfl on a finite enum; there is no appeal to analytic estimates or continuum limits.

why it matters in Recognition Science

Gives Physics a named, countable phase list tied to configuration dimension so later RS results can refer to solid, liquid, gas, and related phases without ad-hoc strings. Downstream use is currently empty in the graph, so the module is a leaf taxonomy rather than a lemma feeding a parent theorem. It anchors the condensed-matter side of the $D=3$ landmark (T8) and keeps phase language consistent with the eight-tick and $\phi$-ladder scaffolding used elsewhere in the monolith.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)