toy_has_zero_params
plain-language theorem explainer
The toy zero-parameter physics framework has a unique parameter record, equivalent to the unit type, so it satisfies the strong zero-parameters predicate. Anyone checking the Parameter Surface formalization of "no free knobs" would cite this as the positive example. The proof is a one-line term: the reflexive equivalence on PUnit.
Claim. The toy zero-parameter framework satisfies the strong zero-parameters property: its parameter-record type is equivalent to the unit type $PUnit$ (exactly one configuration).
background
The Parameter Surface module replaces a weak "countable state space" reading of zero parameters with a physics-facing notion of adjustable numerical knobs. A PhysicsFramework may carry a HasParameterRecord: a type ParameterRecord of configurations, a map configure sending each record to a state-space evolution, and an injectivity axiom so distinct records give distinct evolutions.
Strong zero parameters means that record type is unique: Nonempty (ParameterRecord F ≃ PUnit). Equivalently, there is exactly one way to configure the framework. The companion notion embeds $\mathbb{R}$ into the record when a free real knob exists.
The toy framework is the canonical empty-record instance used as a positive witness opposite the one-parameter example later in the same module.
proof idea
Term-mode proof. HasZeroParameters_Strong asks for a nonempty equivalence ParameterRecord ≃ PUnit. For the toy framework the record is already PUnit, so Equiv.refl PUnit inhabits the equivalence type; wrapping it in an anonymous constructor discharges Nonempty.
why it matters
This is the positive calibration point for the exclusivity verification story: a framework can be shown, in Lean, to have literally one configuration. The module doc frames the old HasAlgorithmicSpec definition as insufficient because countable state space still allows free couplings; the strong predicate closes that gap.
Together with the sibling one-parameter counterexample (oneParam_not_zero and friends), it pins the dichotomy used when arguing Recognition Science has no free real knobs in the sense of T0–T8 forcing (J-uniqueness, $\varphi$, eight-tick octave, $D=3$) rather than fitted constants. No downstream theorems currently depend on it; it is an in-module sanity witness for the parameter-surface API.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.