feasible_nonempty
plain-language theorem explainer
The theorem shows that for any configuration of N ledger entries the feasible set of one-tick successors is nonempty because the current state itself satisfies the log-charge conservation constraint. Researchers building the variational update rule for the Recognition Science ledger cite this to guarantee that the constrained J-cost minimization is always defined. The proof is a direct term that pairs the input configuration with the reflexivity fact that every state is feasible from itself.
Claim. Let $N$ be a natural number and let $c$ be a configuration of $N$ positive real ledger entries. The set of all configurations $c'$ such that the total log-charge of $c'$ equals the total log-charge of $c$ is nonempty.
background
The Variational Dynamics module supplies the missing update rule for the Recognition Science ledger: the next state is the configuration that minimizes total defect subject to conservation of log-charge. A configuration is a structure whose entries are a function from Fin N to positive reals. The feasible set from c is defined as the collection of all configurations c' whose total log-charge (sum of log entries) equals that of c; this encodes the conservation law that follows from J-symmetry.
proof idea
The proof is a term-mode construction that directly exhibits the current configuration as an element of its own feasible set by pairing c with the reflexivity lemma self_feasible c.
why it matters
This result ensures the argmin that defines the ledger's equation of motion is taken over a nonempty set, closing the gap between the existence of a defect landscape and the existence of a well-defined successor state. It sits inside the F-008 update principle and rests on the conservation law derived from LawOfExistence together with the Configuration structure from InitialCondition. The declaration supports the global, simultaneous character of the update across all entries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.