IndisputableMonolith.Verification.KnobsCount
Module that enumerates every named input consumed by the Recognition Science derivation layer and records that the count of fitted continuous parameters is zero. A verification auditor cites it when checking the no-free-parameters claim. Structure is definitional: a ledger type, a finite list of inputs, cardinality lemmas, and a zero-count theorem.
claimThe derivation layer consumes a finite ledger of named inputs. That ledger is nonempty, has an explicit cardinality, and the number of fitted continuous parameters among them is $0$.
background
Recognition Science claims that the forcing chain (T0–T8) and the Recognition Composition Law fix the dynamics with no adjustable continuous knobs. Constants such as $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$, and the fine-structure band are derived rather than fit.
This module makes that claim checkable. It introduces a type of ledgered inputs (one named input consumed by the derivation layer), assembles them into a finite input ledger, and defines the fitted-continuous-parameter count on that ledger. Sibling declarations record non-emptiness and exact cardinality of the ledger.
The local setting is pure verification bookkeeping: Mathlib is the only import; no physics lemmas are proved here.
proof idea
This is a definition-and-count module, not a deep proof development. It declares the ledgered-input type, builds the concrete input ledger, and supplies cardinality facts (nonempty, exact count). The headline result is a one-line or short equational proof that the fitted continuous parameter count equals zero, by inspecting the ledger entries.
why it matters in Recognition Science
Zero fitted continuous parameters is a load-bearing verification claim for the whole RS stack: if the ledger ever acquires a free real knob, the uniqueness story from J-cost through $\varphi$, the eight-tick octave, and $D=3$ is compromised. Downstream verification and paper-facing summaries cite this module when asserting that the derivation layer is parameter-free. It does not itself derive masses or couplings; it only certifies the input tally those derivations rely on.
scope and limits
- Does not derive any physical constant or mass formula.
- Does not prove uniqueness of J or forcing of phi; only counts ledger inputs.
- Does not assert completeness of the ledger against future modules.
- Does not address discrete or integer-valued configuration choices.
- Does not connect to experimental fitting pipelines outside the RS ledger.