Pith. sign in
module module moderate

IndisputableMonolith.Foundation.GroundStateDynamics

show as:
view Lean formalization →

Equilibria of the recognition ledger sit exactly at the uniform configuration of each conserved charge sector. The module identifies ground states with the unique cost-minimizing flat assignment and treats zero-charge equilibria as the unit ratio configuration. Mass and generation work cites it when locking torsion and rung offsets to a stable vacuum. Arguments reduce sector equilibria to uniform minimizers via the variational update rule.

claimIn each conserved charge sector of the recognition ledger, every equilibrium configuration equals the uniform minimizer of the sector cost. In particular, a stable zero-charge equilibrium is the unit ratio configuration (all entries $1$), and the logarithmic charge of a ratio configuration vanishes precisely when that configuration is identically one.

background

Recognition Science treats the ledger as a discrete dynamical system whose one-step map is formalized in VariationalDynamics (F-008): the missing update rule $\mathrm{state}(t)\to\mathrm{state}(t+1)$. Cost is measured by the $J$-functional forced at T5, $J(x)=(x+x^{-1})/2-1$, subject to the Recognition Composition Law. Conserved sectors are level sets of total logarithmic charge; within a sector the variational problem asks for configurations that minimize total $J$.

This module studies those minimizers as ground states. Sibling material introduces ratio configurations (entries as positive reals encoding pairwise ratios), their per-entry and log-charge projections, and the claim that any equilibrium coincides with the uniform assignment on its sector. Zero total charge forces the uniform value to be unity, so the stable vacuum is the all-ones configuration.

proof idea

The module is theorem-bearing, not a pure definition dump. Core results identify equilibria with uniform sector minimizers, then specialize to zero charge. Typical steps: express equilibrium as a critical point of the sector cost inherited from VariationalDynamics; apply convexity or uniqueness of the $J$-minimizer on a fixed-charge slice to force all entries equal; for vanishing total log-charge, the common value must be $1$. Ratio-configuration lemmas package the same fact in multiplicative coordinates used downstream by mass and torsion bridges.

why it matters in Recognition Science

Ground-state uniqueness supplies the vacuum against which generation torsion and mass rungs are measured. GenerationTorsionBridge imports this module as part of the authoritative chain deriving charged-generation torsion ${0,11,17}$ from $Q_3$ cube geometry and matching every other codebase representation. Without a pinned uniform zero-charge equilibrium, rung offsets on the $\phi$-ladder and the eight-tick octave bookkeeping would float relative to an arbitrary background. The module therefore sits between the F-008 equation of motion and the mass/generation layer, closing the "what is the stable ledger vacuum" gap before torsion and $\phi$-ladder formulas are applied.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)