zero_params_excludes_real_knob
plain-language theorem explainer
A physics framework cannot simultaneously have a unique (PUnit) parameter record and an injective real-valued free knob. Anyone arguing the RS zero-parameter claim against adjustable couplings cites this mutual exclusion. The proof composes the PUnit equivalence with the real embedding and derives 0 = 1 from injectivity into a singleton.
Claim. Let $F$ be a physics framework equipped with a parameter record (a type of adjustable configurations acting injectively on the state-space evolution). If that record is equivalent to the unit type $PUnit$ (exactly one configuration) and there exists an injective map $\mathbb{R} \hookrightarrow$ ParameterRecord, then contradiction.
background
This module replaces a weak "countable state space" reading of zero free parameters with an explicit parameter-record surface. A ParameterRecord is the type of adjustable numerical configurations of a framework $F$, together with an injective configure map into state-space evolutions: different parameters must yield different dynamics.
Strong zero parameters means the record is equivalent to $PUnit$ (exactly one configuration). A free real knob means $\mathbb{R}$ embeds injectively into the record, so a continuous family of configurations exists. The module doc states the key insight: a truly parameter-free framework has ParameterRecord $= PUnit$; a framework with free parameters has record $\mathbb{R}$ or a product of reals.
The local setting is Verification/Exclusivity: non-vacuous formalization of the RS claim that the forced framework carries no adjustable numerical knobs in the physics sense.
proof idea
Tactic proof by unpacking both hypotheses. From strong zero parameters obtain an equivalence $eqv$ between the parameter record and $PUnit$. From the free-knob hypothesis obtain an injective embedding $\mathrm{embed}:\mathbb{R}\to$ ParameterRecord.
Because $PUnit$ is a subsingleton, $eqv(\mathrm{embed}, x)=eqv(\mathrm{embed}, y)$ for all reals $x,y$. Injectivity of $eqv$ forces $\mathrm{embed}, x=\mathrm{embed}, y$. Injectivity of embed then forces $x=y$ for all reals. Instantiating at $0$ and $1$ (with $0\neq 1$ by norm_num) yields the contradiction.
why it matters
This is the non-vacuous mutual-exclusion lemma for the RS zero-parameter posture. Downstream, zero_params_forces_dimensionless quotes it directly: if a dimensionful observable existed it would induce a genuine real-valued knob, contradicting this theorem, so strong zero parameters force all observables to be dimensionless.
The sibling oneParam_not_zero applies it to the toy one-parameter framework (record $\mathbb{R}$) to show that framework fails strong zero parameters. Together these pin the exclusivity surface: RS-style frameworks cannot hide a continuous coupling while claiming a unique configuration.
In the broader forcing chain this supports the verification claim that the T0–T8 forced structure (J-uniqueness, $\varphi$, eight-tick octave, $D=3$) leaves no free real dial once the parameter record is $PUnit$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.