toyZeroParamFramework
plain-language theorem explainer
A minimal PhysicsFramework with singleton state space, identity evolution and measurement, and a unique initial state. It is the canonical witness that a framework can have ParameterRecord equal to the unit type, i.e. genuinely zero free knobs. Downstream exclusivity lemmas cite it to prove HasZeroParameters_Strong and to contrast against one-parameter frameworks. The body is a pure structure instance: every field is id or the unit value.
Claim. Define a toy physics framework whose state space is the singleton type, whose evolution and measurement maps are the identity, whose observable type is the singleton, and which admits a unique initial state. Equipped with parameter record $PUnit$, it is the standard example of a framework with no adjustable real parameters.
background
The ParameterSurface module replaces an older "zero parameters means countable state space" criterion with a parameter-record interface. A ParameterRecord is the type of adjustable configurations of a framework. HasZeroParameters_Strong holds when that record is definitionally (or equivalently) the unit type $PUnit$: there is exactly one way to configure the theory. HasFreeRealKnob holds when the record contains at least one $\mathbb{R}$ factor.
PhysicsFramework (from the Exclusivity.Framework import) packages a state space, an evolve map, an Observable type, a measure map, and a nonempty initial-state witness. The toy fills every slot with Unit or id, so dynamics and observation carry no numerical freedom.
This is deliberately non-physical: it exists only to pin the boundary case of the exclusivity argument, not to model Recognition Science dynamics (J-cost, phi-ladder, eight-tick octave).
proof idea
Definitional construction, not a proof. StateSpace and Observable are set to Unit; evolve and measure are the identity function; hasInitialState is the unique inhabitant of Unit. A companion instance sets ParameterRecord to PUnit.{1}, configure to ignore the unit parameter and return id, and configure_injective by Subsingleton.elim. No lemmas are invoked beyond structure field filling.
why it matters
Supplies the positive witness for the module's refined "zero free parameters" claim. toy_has_zero_params immediately concludes HasZeroParameters_Strong via Equiv.refl on PUnit. The sibling oneParamFramework (ParameterRecord = $\mathbb{R}$) is then shown not zero-parameter by zero_params_excludes_real_knob, yielding oneParam_not_zero.
In the broader exclusivity story this separates "algorithmically specified / countable" from "no adjustable coupling." Recognition Science's forcing chain (T5 J-uniqueness through T8 dimension) aims at a unique law with no free knobs; the toy is the formal null model against which any claimed free $\mathbb{R}$ parameter is excluded. It does not itself derive constants ($c$, $\hbar$, $G$, $\alpha$) or close any forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.