ParameterCount
plain-language theorem explainer
Boolean property of a physics framework that holds exactly when the framework has zero free parameters. Exclusivity and no-alternatives arguments cite it to mark algorithmic, parameter-free theories. The body is a one-line alias of the zero-parameter predicate; the doc flags this as a simplified stand-in for a real parameter tally.
Claim. For a physics framework $F$ (state space, evolution, observables, and measurement), the parameter-count property holds if and only if $F$ has zero adjustable real parameters.
background
The shared exclusivity module defines a minimal PhysicsFramework: a state space, an evolution map, an observable type, a measurement map, and existence of initial data. That interface is the common substrate for NoAlternatives and necessity proofs, kept thin to break circular imports.
Parameter counting is deliberately coarse here. The declaration reduces to the sibling zero-parameter predicate: true when the framework is treated as algorithmic (no free reals), false otherwise. The doc-comment states that a full formalization would enumerate adjustable real parameters in the framework definition; this version only records the zero/nonzero cut.
Nearby siblings (HasAlgorithmicSpec, HasZeroParameters, DerivesObservables) supply the rest of the exclusivity checklist: algorithmic presentation, observable extraction, and structural derivation.
proof idea
Definition, not a proved theorem. The body is the single proposition HasZeroParameters F, with an inline note that the flag is true for zero parameters and false otherwise. No tactics, no lemmas, no arithmetic on a parameter list.
why it matters
Zero free parameters is the exclusivity filter that separates Recognition-style forced frameworks from empirically tuned ones. In the RS forcing chain, constants and structure (J-uniqueness, $\phi$, eight-tick period, $D=3$) are derived rather than fitted; a framework that still carries adjustable reals cannot claim the same necessity.
This definition sits in the shared verification layer used by NoAlternatives and necessity certificates. It does not itself prove uniqueness; it only names the zero-parameter cut those arguments need. The module keeps it for backward-compatible certificates while stronger observable-derivation predicates live elsewhere.
No downstream uses are recorded in the graph yet, so its role is infrastructural: a stable Prop hook for exclusivity statements rather than a leaf theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.