energyFromJCost
The definition identifies the energy of a ledger configuration directly with its J-cost value. Researchers constructing partition functions or deriving thermodynamic relations from Recognition Science ledger sums cite this mapping to equate low J-cost states with low energy. The implementation is a one-line alias to the Jcost function.
claimThe energy $E(x)$ of a configuration with ratio $x$ is defined by $E(x) = J(x)$, where $J$ denotes the J-cost of the ledger entry.
background
The PartitionFunction module derives the statistical mechanics partition function as a sum over ledger configurations weighted by J-cost. J-cost quantifies the recognition defect of a multiplicative ratio, with low values corresponding to favored states. The module doc states that Z encodes free energy, average energy, and entropy through the standard relations, now realized via ledger sums. Upstream entropy in InitialCondition is proportional to total defect, providing the minimum-entropy reference state.
proof idea
This is a one-line definition that directly aliases the Jcost function to energyFromJCost.
why it matters in Recognition Science
This supplies the energy mapping used by the JCostThermoBridge theorems energy_min_at_unity, energy_nonneg, and jcost_thermo_fundamentals. The latter states that energy is proportional to J-cost, Boltzmann weights minimize expected J-cost, and free energy follows from the partition function. It realizes the core E_state ↔ J_cost connection in the T5 J-uniqueness step of the forcing chain and supports the eight-tick octave structure for phase statistics.
scope and limits
- Does not introduce temperature or Boltzmann factors.
- Does not prove non-negativity or minimization of energy.
- Does not specify the explicit algebraic form of Jcost.
- Does not address multi-particle statistics or phase factors.
formal statement (Lean)
133noncomputable def energyFromJCost (x : ℝ) : ℝ := Jcost x
proof body
Definition body.
134
135/-- The temperature sets the scale for J-cost fluctuations.
136
137 - Low T: Only lowest J-cost states occupied
138 - High T: All states approximately equally occupied
139 - T → ∞: Maximum entropy (all states equally likely) -/