HasParameterRecord
plain-language theorem explainer
A typeclass that equips any abstract physics framework with an explicit parameter surface: a type of configurations and an injective map from those configurations into evolution operators on the state space. Zero free parameters means the record is unique (unit type); free knobs mean a real line embeds into it. Downstream exclusivity and dimensionless-forcing arguments cite this interface rather than the older countable-state proxy. The declaration is pure structure, no proof body.
Claim. For a physics framework $F$ (state space, evolution, observables), a parameter record is a type $P$ together with a map $\mathrm{configure}: P \to (S_F \to S_F)$ that is injective: distinct parameter values induce distinct evolution operators on the state space $S_F$.
background
The module replaces a weak proxy for "zero free parameters" (algorithmic/countable state space) with a physics-facing notion of adjustable numerical knobs. A framework can be countable yet still carry a free coupling that ranges over $\mathbb{R}$.
The ambient object is PhysicsFramework: carrier state space, evolution map, observables, and a nonempty initial-state witness. The parameter surface sits on top of that interface. The record type is the space of configurations; configure says how each configuration rewrites the evolution law; injectivity ensures the knobs are not dummy labels.
Sibling notions built on this class: strong zero parameters means the record is equivalent to the unit type (exactly one configuration); a free real knob means $\mathbb{R}$ injects into the record.
proof idea
No proof: this is a typeclass declaration. It packages three fields (record type, configuration map into endomorphisms of the state space, and injectivity of that map). Instances are supplied later for toy zero-parameter and one-parameter frameworks; consumers assume the class and reason about the induced propositions.
why it matters
This is the non-vacuous backbone of the exclusivity verification stack's "zero free parameters" claim. HasZeroParameters_Strong and HasFreeRealKnob are defined directly from it, and zero_params_excludes_real_knob makes those postures mutually exclusive.
Downstream, zero_params_forces_dimensionless and bridge_B3_single_channel_forces_ratio take a [HasParameterRecord F] instance plus strong zero parameters: if a dimensionful observable existed it would induce a real knob, contradicting zero parameters, so observables must be dimensionless and (with single-channel conservation) factor through a positive ratio interface. That is the formal bridge from "no free knobs" toward RS-style dimensionless forcing, complementary to the T0–T8 chain that fixes $J$, $\varphi$, the eight-tick period, and $D=3$.
Toy instances (toyZeroParamFramework, oneParamFramework) witness that the interface is inhabited on both sides of the dichotomy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.