oneParam_has_knob
plain-language theorem explainer
The toy one-parameter physics framework admits an injective embedding of the reals into its parameter record, so it has a free real knob. Anyone checking the exclusivity/parameter-surface formalization cites this as the positive witness that the one-parameter example is not zero-parameter. The proof is a two-field term: identity embedding plus trivial injectivity.
Claim. The one-parameter physics framework has a free real knob: there exists an injective map $\mathbb{R}\hookrightarrow$ its parameter record.
background
This module tightens the old "zero free parameters" claim. Countable state space alone does not rule out adjustable numerical knobs (e.g. a coupling set to any real). The fix is a parameter record: a type of configurations, a configure map into state-space evolution, and injectivity of configure so distinct parameters give distinct dynamics.
A free real knob means $\mathbb{R}$ embeds injectively into that parameter record. Strong zero-parameters means the record is PUnit (one configuration). Those two properties are mutually exclusive by a sibling lemma.
The one-parameter framework is the canonical counterexample object in this file: its parameter record is essentially $\mathbb{R}$, so it should carry a free knob and fail the strong zero-parameter predicate.
proof idea
Term-mode existential witness for HasFreeRealKnob. Take the identity map $\mathrm{id}:\mathbb{R}\to$ parameter record (the record is $\mathbb{R}$ for this framework). Injectivity is immediate: equal images imply equal arguments via fun _ _ h => h. No further lemmas are needed.
why it matters
Feeds oneParam_not_zero, which concludes the one-parameter framework does not satisfy strong zero-parameters by applying mutual exclusion of zero-parameters and free knobs to this witness. Together the pair shows the new parameter-record API separates "has a real coupling" from "parameter-free" in the sense the exclusivity verification needs.
In the Recognition Science exclusivity story, RS claims zero free parameters (constants fixed by the forcing chain and RCL, not fitted). This lemma is scaffolding for that claim: it certifies that the positive control (a framework with one real knob) is detected correctly before arguing the RS framework has parameter record PUnit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.