self_feasible
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove existence of any configuration besides the current state inside the feasible set.
- Does not establish uniqueness of the defect minimizer.
- Does not compute the explicit entries of the successor configuration.
- Does not address higher-tick reachability beyond one step.
Lean usage
theorem feasible_nonempty {N : ℕ} (c : Configuration N) : Set.Nonempty (Feasible c) := ⟨c, self_feasible c⟩formal statement (Lean)
94theorem self_feasible {N : ℕ} (c : Configuration N) :
95 c ∈ Feasible c := rfl
proof body
Term-mode proof.
96
97/-- The feasible set is nonempty (contains the current state). -/