NonStatic
plain-language theorem explainer
A physics framework counts as non-static when its evolution map moves at least one state. Exclusivity and necessity arguments that discard frozen dynamics cite this Prop class as a structural filter. It is a one-field typeclass packaging an existential, not a proved theorem.
Claim. A physics framework $F$ is non-static if there exists a state $s$ in the state space of $F$ such that $\mathrm{evolve}_F(s) \neq s$.
background
This module holds shared framework definitions used by both NoAlternatives and the necessity proofs, so those developments do not import each other. The central object is PhysicsFramework: a minimal interface with a state space, an evolution map, an observable type, a measurement map, and existence of initial conditions.
Non-static is one of several structural predicates on that interface (alongside zero-parameter, algorithmic-spec, and observable-derivation markers). It only constrains dynamics: at least one state is not a fixed point of evolve. Upstream names that appear in the dependency graph (active-edge count $A$, gap display $F$, discrete J-descent iteration) are ambient RS infrastructure; they are not hypotheses of this class.
proof idea
Definitional Prop class with no proof body. The single field is the existential statement that some state is moved by the framework's evolution operator. Instantiating the class means exhibiting such a state (or deriving the existential from a stronger dynamical assumption).
why it matters
In the Verification/Exclusivity stack this predicate screens out trivial frozen frameworks before parameter counting and observable-derivation arguments run. Recognition Science forces nontrivial discrete dynamics (eight-tick octave, J-cost descent, phi-ladder mass steps); a static evolve map would sit outside that forcing chain. No downstream theorems currently list this class as a direct dependency in the supplied graph, so it functions as shared scaffolding for exclusivity filters rather than a leaf in a finished proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.