oneParamFramework
plain-language theorem explainer
Toy physics framework whose state space is the reals and whose only free datum is a real coupling constant. Used as the positive control that a framework can be countable-looking yet still carry an adjustable numerical knob. The definition is a direct structure instance: identity evolution, identity measurement, initial state zero, with configuration acting by scalar multiplication.
Claim. Define a physics framework with state space $\mathbb{R}$, trivial (identity) evolution, observables valued in $\mathbb{R}$ measured by the identity map, and initial state $0$. Equip it with parameter record $\mathbb{R}$, where a coupling $c$ configures evolution by $x \mapsto c\cdot x$, and distinct couplings yield distinct configured dynamics.
background
The Parameter Surface module replaces an older "zero free parameters" proxy (algorithmic/countable state space) with an explicit parameter-record interface. A parameter record is the type of adjustable numerical knobs of a framework. Strong zero-parameter means that record is PUnit (one configuration only). A free real knob means the record contains at least one $\mathbb{R}$ factor, so infinitely many configurations exist.
PhysicsFramework packages state space, evolution, observables, measurement, and an inhabited initial state. The sibling notion HasParameterRecord adds a ParameterRecord type and an injective configure map from parameters into evolution laws. Injectivity is the physics content: different knob settings must produce different dynamics.
This definition is the one-parameter counterexample in that taxonomy: state space $\mathbb{R}$ with identity flow, and configuration by real scalar multiplication on the state.
proof idea
Pure structure definition, not a proof. Fields are filled by identity maps and the zero initial state. The accompanying HasParameterRecord instance sets the parameter record to $\mathbb{R}$ and `configure(c)(x) = c\cdot x$. Injectivity of configure is a short calculation: equal configured maps agree at $x=1$, so the couplings agree.
why it matters
This is the positive control for the exclusivity/parameter-surface story. Downstream, oneParam_has_knob exhibits an explicit free real knob (the identity embedding of $\mathbb{R}$), and oneParam_not_zero shows the strong zero-parameter property fails, via the general lemma that zero parameters exclude any free real knob.
In Recognition Science terms it sharpens the "zero free parameters" claim against a common loophole: a framework can look simple (even with trivial evolution) yet still smuggle a continuous coupling. The RS forcing chain aims at frameworks whose parameter record is unit, not $\mathbb{R}$. This toy object makes that distinction machine-checkable and feeds the exclusivity verification path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.