HasFreeRealKnob
plain-language theorem explainer
A physics framework has a free real knob when the reals inject into its parameter-record type: there is a continuum of distinct configurations. Exclusivity and dimensionless-forcing arguments cite this predicate to separate zero-parameter frameworks from those with adjustable couplings. The body is a one-line existential definition, not a derived theorem.
Claim. Let $F$ be a physics framework equipped with a parameter record (a type of adjustable configurations acting injectively on the state space). Then $F$ has a free real knob if there exists an injective map $\mathbb{R} \hookrightarrow \mathrm{ParameterRecord}(F)$.
background
The Parameter Surface module replaces the older "zero parameters means countable state space" gloss with a record of adjustable numerical knobs. A parameter record is a type ParameterRecord together with an injective configure map into state-space endomorphisms: different parameters must induce different evolution.
Under that interface, strong zero parameters means the record is definitionally unique (PUnit). The complementary notion is a free continuum of knobs. The module doc states the key insight: a truly parameter-free framework has exactly one configuration, while a framework with free parameters has record type $\mathbb{R}$, $\mathbb{R}\times\mathbb{R}$, etc.
PhysicsFramework is the ambient exclusivity carrier (state space and evolution). This definition only makes sense once a parameter-record instance is supplied; it does not itself construct that instance.
proof idea
Pure definitional unpacking: the predicate is the proposition that there exists a function $\mathbb{R}\to\mathrm{ParameterRecord}(F)$ that is injective. No lemmas are applied; the body is the standard Mathlib Function.Injective existential. Downstream proofs discharge it by exhibiting a concrete embedding (e.g. id on a one-parameter toy) or derive False from it together with a PUnit equivalence.
why it matters
This is the positive half of the non-vacuous zero-parameter formalization. The sibling theorem zero_params_excludes_real_knob shows mutual exclusion with strong zero parameters: if the record is equivalent to PUnit and $\mathbb{R}$ embeds into the record, one obtains an injection $\mathbb{R}\hookrightarrow\mathrm{PUnit}$, which is impossible.
Dimensionless forcing uses it as the bridge hypothesis: zero_params_forces_dimensionless and bridge_B3_single_channel_forces_ratio assume that any dimensionful observable would induce a free real knob, then contradict strong zero parameters. The toy oneParam_has_knob witnesses the predicate on a one-parameter framework, showing the definition is inhabited and not vacuous.
In the exclusivity program this pins "no adjustable couplings" in the physics sense, not merely countable state space, which is required before claiming forced dimensionless ratios and single-channel interfaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.