IndisputableMonolith.Verification.Exclusivity.ParameterSurface
Defines the parameter surface of a physics framework: the type of adjustable numerical knobs it carries. Zero-parameter frameworks use a singleton type; frameworks with free constants use products of reals. Supplies typeclass interfaces for zero-parameter strength and free real knobs, plus exclusion lemmas and toy models. Downstream dimensionless-forcing arguments import this surface to state that Recognition Science has no free knobs.
claimA parameter record $P$ is the type of adjustable numerical knobs of a physics framework $F$. For a zero-parameter framework, $P \simeq \mathbf{1}$ (unique inhabitant). For $n$ free real parameters, $P \simeq \mathbb{R}^n$. Interfaces assert strong zero-parameter status and the presence of a free real knob; a lemma states that strong zero-parameter status excludes any free real knob.
background
In the exclusivity verification layer, a physics framework is an abstract carrier of dynamical and kinematic structure (imported from the shared Framework module, which breaks circular dependencies between NoAlternatives and necessity proofs). Beyond that structure one must record which numerical constants are free inputs rather than derived outputs.
A parameter record is exactly that type of knobs. The empty (singleton) record means every constant is forced; a copy of $\mathbb{R}$ or a finite product means the framework still has adjustable real parameters. Typeclasses package the claims "has a parameter record," "has strongly zero parameters," and "has a free real knob," so later modules can quantify over frameworks without hard-coding a particular parameter type.
Toy frameworks (one with empty record, one with a single real knob) witness that the interfaces are inhabited and that the exclusion relation is sharp.
proof idea
This is largely a definition and interface module. Parameter-record and zero-parameter typeclasses are Prop-carrying structures; free-real-knob is a similar interface. The main lemma is an elementary incompatibility: strong zero-parameter status and existence of a free real knob cannot hold simultaneously. Toy models are concrete instances (singleton vs $\mathbb{R}$) that discharge the interfaces and illustrate the exclusion. No deep analytic argument lives here; the content is type-level bookkeeping for exclusivity.
why it matters in Recognition Science
Exclusivity claims in Recognition Science require a precise notion of "no free parameters." This module supplies that surface so DimensionlessForcing (and related necessity arguments) can state that the RS framework has empty parameter record while competitor frameworks retain real knobs. It sits under the shared Framework definitions and feeds the forcing chain that aims to show dimensionless constants (including the fine-structure band) are fixed rather than fitted. Without a clean parameter surface, zero-parameter claims would be informal.
scope and limits
- Does not derive any physical constant or force a numerical value.
- Does not prove that Recognition Science itself has zero parameters; only supplies the interface.
- Does not classify continuous families of theories beyond finite real products.
- Does not address discrete or categorical parameters outside the real-knob interface.
- Toy models are illustrative only; they are not physical frameworks.