Feasible
plain-language theorem explainer
The feasible set collects all ledger configurations that preserve the total log-ratio of the current state. Physicists modeling deterministic evolution of the recognition ledger cite this when deriving the update rule from constrained minimization. It is introduced as a direct set comprehension over configurations sharing the conserved charge quantity.
Claim. Let $c$ be a configuration of $N$ positive real entries. The feasible set consists of all configurations $c'$ satisfying $∑_{i=1}^N log(c'_i) = ∑_{i=1}^N log(c_i)$.
background
The Variational Dynamics module supplies the missing update rule for the Recognition Science ledger. A configuration is a structure whose entries are positive real ratios indexed by Fin N. The total log-charge is the sum of the logarithms of these entries and remains invariant because the J-cost function is symmetric under inversion, as established in the LawOfExistence module.
proof idea
This is a one-line definition that constructs the set of all configurations whose log-charge matches the input. It directly invokes the log-charge summation and the positivity condition built into the configuration structure.
why it matters
This supplies the constraint set for the variational successor definition and the equilibrium characterization theorem. It encodes the charge conservation that follows from J-symmetry and enables the deterministic evolution theorem. In the framework it realizes the constrained minimization step that turns the energy landscape into an explicit equation of motion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.