HasZeroParameters_Strong
plain-language theorem explainer
A physics framework has strongly zero free parameters when its parameter-record type is uniquely inhabited, i.e. equivalent to the unit type. Anyone arguing the RS exclusivity claim that no adjustable numerical knobs remain cites this predicate. It is a one-line definitional Prop: nonemptiness of an equivalence ParameterRecord ≃ PUnit.
Claim. Let $F$ be a physics framework equipped with a parameter record (a type of adjustable configurations together with an injective map from configurations into evolution operators on the state space). Then $F$ has strongly zero free parameters when that parameter-record type is equivalent to the unit type $1$, i.e. there is exactly one configuration up to unique isomorphism.
background
The Parameter Surface module replaces an older "zero parameters means countable state space" gloss with a physics-facing notion of adjustable numerical knobs. A PhysicsFramework supplies a state space, evolution, and observables. Over that, a parameter record is a type of configurations plus an injective configure map into endomorphisms of the state space, so distinct knobs really change the dynamics.
Strong zero-parameter posture means the record collapses to a singleton: there is exactly one way to configure the framework. By contrast, a free real knob is an injective embedding of $\mathbb{R}$ into the record (one continuous coupling, or a factor of one). The module's key insight is that $PUnit$ vs $\mathbb{R}$ (or products of $\mathbb{R}$) separates "unique configuration" from "infinitely many couplings."
Upstream, the exclusivity framework only needs the abstract PhysicsFramework interface; the circle-winding and mass-anchor symbols that appear in the dependency graph are ambient RS infrastructure, not ingredients of this Prop.
proof idea
Definitional, not a proved theorem. The body is the proposition that there exists an equivalence between the framework's parameter-record type and PUnit (the unit type in universe 1). Inhabiting that Prop is exactly exhibiting such an equivalence; the toy zero-parameter example later does so via Equiv.refl.
why it matters
This is the non-vacuous formalization of "zero free parameters" used throughout exclusivity verification. Downstream, zero_params_excludes_real_knob shows mutual exclusion with a free $\mathbb{R}$ embedding; zero_params_forces_dimensionless and Bridge B3 (bridge_B3_single_channel_forces_ratio) use the strong zero-parameter hypothesis to force dimensionless observables and a positive-ratio interface under single-channel conservation. Toy and one-parameter examples (toy_has_zero_params, oneParam_not_zero) certify that the predicate distinguishes genuine singleton records from coupling-constant frameworks.
In the broader RS story this is the verification-side stand-in for the claim that the forcing chain (T0–T8) and the Recognition Composition Law leave no adjustable constants once $\phi$, the eight-tick octave, and $D=3$ are fixed. It does not itself derive those landmarks; it packages the "no knobs left" posture so dimensionless-forcing theorems can cite it cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.