oneParam_not_zero
plain-language theorem explainer
The one-parameter toy framework fails the strong zero-parameter test: its parameter record is not equivalent to the unit type. Anyone auditing that the exclusivity formalization is non-vacuous cites this negative instance. The proof is a one-line application of mutual exclusion between zero parameters and a free real knob, using the already-proved knob fact for that framework.
Claim. The toy physics framework whose parameter record is $\mathbb{R}$ does not satisfy the strong zero-parameter condition: there is no equivalence between its parameter record and the unit type $PUnit$.
background
This module tightens the "zero free parameters" claim used in exclusivity arguments. The older predicate equated zero parameters with mere algorithmic enumerability of the state space, which a framework can satisfy while still carrying adjustable numerical knobs (coupling constants, scales, and so on).
The fix introduces a parameter-record typeclass: each framework exposes a type of configurations together with an injective configure map into state-space evolutions. Strong zero parameters means that record is equivalent to $PUnit$ (exactly one configuration). A free real knob means $\mathbb{R}$ embeds into the record. The module builds two toys: one with record $PUnit$, and oneParamFramework with record $\mathbb{R}$.
Upstream, the exclusivity framework already supplies algorithmic-spec language; the parameter-record layer sits on top so that "no free knobs" is a separate, checkable property rather than a synonym for countability.
proof idea
Term-mode by contradiction. Assume the strong zero-parameter predicate for the one-parameter toy. Discharge immediately with the mutual-exclusion lemma: zero parameters and a free real knob cannot hold together. The second hypothesis is the sibling fact that the one-parameter toy has a free real knob (its record is $\mathbb{R}$ with injective configure). No further case analysis.
why it matters
Recognition Science claims a unique, zero-parameter derivation of physics (forcing chain T0–T8, RCL, $\phi$-ladder constants). Exclusivity arguments need a Lean predicate that actually means "no adjustable knobs," not merely "countable states." This theorem is the negative half of the non-vacuity check: the one-parameter toy is provably outside the strong zero-parameter class, while the zero-parameter toy sits inside it, and the two predicates are mutually exclusive.
No downstream consumers are wired yet (used_by is empty). The declaration still closes the documented vacuity hole in the old HasZeroParameters := HasAlgorithmicSpec definition, so later uniqueness or "only RS" theorems can cite a predicate that rejects free $\mathbb{R}$ knobs rather than accepting them by accident.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.