IndisputableMonolith.Verification.Exclusivity.ParameterSurface
Defines the parameter surface of a physics framework: the type of adjustable numerical knobs. Zero-parameter theories use the unit type; theories with free constants use reals or products of reals. Supplies typeclass predicates for zero-parameter and free-real-knob structure, plus toy examples that separate the two. Downstream exclusivity and dimensionless-forcing arguments cite these predicates to rule out alternative frameworks that smuggle in free constants.
claimA parameter record is a type $P$ standing for the adjustable numerical knobs of a framework: $P = \mathbf{1}$ (unit) when there are no free parameters, and $P = \mathbb{R}$, $\mathbb{R}\times\mathbb{R}$, etc., otherwise. Predicates assert strong zero-parameter structure and the existence of a free real knob; a lemma shows these are incompatible. Toy frameworks illustrate both extremes.
background
In the exclusivity layer of Recognition Science, competing physics frameworks are compared by structural properties rather than by fitting data. One such property is the parameter surface: which real numbers can still be dialed after the framework's axioms are fixed.
The parent Framework module supplies only the shared skeleton used by NoAlternatives and the necessity proofs, deliberately thin so that circular imports are avoided. ParameterSurface sits on that skeleton and introduces the concrete typeclass language for knobs.
A zero-parameter framework is one whose parameter record is definitionally unique (the unit type). A free real knob is a continuous real degree of freedom that is not fixed by the axioms. The module also records the elementary incompatibility: strong zero-parameter structure excludes any free real knob.
proof idea
This is primarily a definition and typeclass module. It introduces the parameter-record interface, the strong zero-parameter predicate, and the free-real-knob predicate, then proves the short exclusion lemma that zero parameters rule out a real knob. Toy frameworks (a zero-parameter example and a one-parameter example) discharge the predicates by construction and witness the exclusion. No deep analytic argument is required; the content is structural bookkeeping for later forcing theorems.
why it matters in Recognition Science
Exclusivity arguments in Recognition Science claim that the RS framework is forced and that alternatives either fail structural constraints or reintroduce free parameters. This module supplies the precise language for that claim: HasZeroParameters_Strong versus HasFreeRealKnob, and the lemma that they cannot hold together.
It is imported by DimensionlessForcing, which uses the parameter-surface predicates when forcing dimensionless constants (including the fine-structure band) without residual knobs. In the broader chain, zero free parameters is part of what distinguishes a fully forced theory (T5–T8 landmarks, RCL, phi-ladder masses) from a phenomenological model that still fits by dialing reals.
scope and limits
- Does not prove that Recognition Science itself has zero free parameters.
- Does not enumerate or classify all possible parameter types beyond unit and real products.
- Does not force numerical values of constants; only tracks whether knobs exist.
- Does not address discrete or non-real parameter spaces.
- Toy frameworks are illustrative only; they are not physical models.