System
plain-language theorem explainer
A System is a non-empty list of EnergyLevel records, each pairing a real energy value with positive natural degeneracy. Researchers deriving the Boltzmann distribution from J-cost in Recognition Science cite this when modeling cost-constrained state selection. The declaration is a bare structure definition that packages the list with its length-positivity witness.
Claim. A system is a list of energy levels $(E_i, g_i)$ with $E_i : ℝ$ and $g_i : ℕ_{>0}$, together with the condition that the list has length at least one.
background
The THERMO-001 module derives the Boltzmann distribution from Recognition Science's J-cost functional. Each state carries a recognition cost J(x); lower-cost states are more probable under a fixed total-cost ledger constraint. The module imports UniversalForcingSelfReference.for for meta-realization axioms and RRF.Foundation.Ledger.empty for balance tracking. EnergyLevel is the sibling structure supplying energy : ℝ and degeneracy : ℕ with deg_pos : degeneracy > 0. Temperature is later defined as the inverse of the Lagrange multiplier β that enforces the cost constraint.
proof idea
This is a structure definition with an empty proof body. It directly assembles the System type from the EnergyLevel structure and the single field nonempty : levels.length > 0.
why it matters
The structure feeds 36 downstream uses, including GeometricStrain and resonant_minimization in CoherenceTechnology, postural_minimization and SystemStability in PosturalAlignment, and tidalLockingFromPhiResonanceCert in Astrophysics. It supplies the basic object for the partition function and probability normalization that realize the paper proposition on statistical mechanics from J-cost. It anchors the cost-weighted selection step that recovers P_i = exp(-β E_i)/Z and connects to the Recognition Composition Law and phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.