self_feasible
plain-language theorem explainer
Any ledger configuration belongs to its own feasible set under the log-charge conservation constraint. Researchers formalizing the variational update rule in Recognition Science ledger dynamics cite this result to anchor nonempty feasible sets and defect-nonincreasing steps. The proof is a direct reflexivity application on the set-membership predicate from the Feasible definition.
Claim. For any natural number $N$ and configuration $c$ with $N$ positive real entries, $c$ lies in the feasible set of $c$, where the feasible set comprises all configurations $c'$ satisfying total log-charge of $c'$ equal to that of $c$.
background
The VariationalDynamics module supplies the missing update rule for the Recognition ledger: the next state is the global minimizer of total defect over the feasible set reachable in one tick. Configuration is the structure of $N$ positive real entries whose total log-charge is conserved under evolution. Feasible is the set of all such configurations sharing the same total log-charge as the input.
proof idea
One-line term proof that applies reflexivity directly to the membership predicate in the definition of Feasible.
why it matters
This reflexivity step feeds the feasible_nonempty theorem and the variational_step_reduces_defect theorem, which together establish that each variational successor has total defect at most that of the current state. It supplies the base case for the constrained J-cost minimization principle that defines ledger evolution in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.