no_fitted_continuous_parameters
plain-language theorem explainer
The T−2..T5 layer of Recognition Science fits no continuous parameters to empirical data. Cite this when defending the narrow “zero knobs” claim: continuous free parameters are absent, while discrete structural inputs remain named elsewhere. The proof is reflexivity against a definition fixed at the natural number zero.
Claim. The number of continuous parameters fit to empirical data in the $T_{-2}\ldots T_5$ proof layer equals $0$.
background
The module is an explicit input ledger for the Recognition Science forcing layer from $T_{-2}$ through $T_5$. It replaced a former vacuous certificate (0 = 0) that the 2026 internal audit flagged as carrying no information about framework inputs. The honest restatement separates continuous fitted parameters from discrete modeling choices, conventions, and calibrations.
Upstream, fittedContinuousParameterCount is defined as the natural number $0$, with the doc-comment: “Number of CONTINUOUS parameters fit to empirical data in the T−2..T5 proof layer: zero. This narrow claim is the honest survivor of the former ‘zero knobs’ language; the discrete inputs above remain real inputs.” Sibling ledger entries enumerate those discrete inputs; this theorem only closes the continuous count.
proof idea
One-line term proof by rfl. The count is definitionally the literal natural number $0$, so equality to $0$ is definitional. Marked @[simp] so downstream rewrites can discharge the continuous-parameter claim without unfolding.
why it matters
Closes the honesty pass on the old “zero knobs” slogan for the $T_{-2}\ldots T_5$ forcing chain (J-uniqueness and related landmarks live in that layer). The framework may still claim no continuous data-fit parameters; it may not claim a parameter-free theory in the broader sense, because the ledger’s discrete structural choices are real inputs. No downstream consumers are recorded yet; the declaration is a verification anchor rather than a lemma in a longer derivation. It does not touch mass ladders, $\alpha$, or later physics outputs—only the continuous-parameter count at the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.