HasZeroParameters
plain-language theorem explainer
A physics framework has zero parameters exactly when its state space admits an algorithmic specification, with no adjustable real knobs. Exclusivity and parameter-surface arguments cite this as the zero-parameter predicate. The body is a one-line definitional alias of algorithmic-spec on the carrier type.
Claim. For a physics framework $F$, $\mathrm{HasZeroParameters}(F)$ holds if and only if the state space of $F$ admits an algorithmic specification (no free real parameters in the framework definition).
background
This module supplies shared physics-framework definitions used by both NoAlternatives and the necessity proofs, isolating the core interface so those developments do not import each other.
A PhysicsFramework is the minimal abstract interface for "doing physics": a state space, an evolution map, an observable type, a measurement map from states to observables, and existence of initial conditions. Zero-parameter status is not a count of reals in the structure fields; it is the claim that the state space can be specified algorithmically.
The sibling note on parameter count records the modeling choice: the count is 0 when the framework is algorithmic, and otherwise left undefined in this simplified formalization. A fuller treatment would enumerate adjustable real parameters in the framework definition.
proof idea
Definitional, not a proved theorem. The predicate on $F$ is identified with algorithmic specification of $F$'s state space: one unfolding step, no tactics or lemmas.
why it matters
Exclusivity needs a crisp zero-parameter gate so Recognition Science can be compared with frameworks that carry free knobs. Downstream, ParameterCount is literally this predicate (true means zero parameters in the simplified model). The parameter-surface development uses the related strong form to prove that a one-parameter framework does not have zero parameters, via exclusion of a real knob.
In the broader RS forcing picture, the claim is that the unique framework forced by the chain (J-uniqueness, $\phi$, eight-tick octave, $D=3$) has no adjustable reals; this definition is the shared Prop that makes "zero parameters" checkable inside Lean exclusivity arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.