fittedContinuousParameterCount
plain-language theorem explainer
The T−2 through T5 forcing layer fits zero continuous parameters to empirical data. Auditors of Recognition Science parameter counts cite this constant as the honest remnant of the old “zero knobs” slogan. Discrete structural inputs remain real and are ledgered separately. The declaration is the literal natural-number assignment 0.
Claim. The number of continuous parameters fitted to empirical data in the $T_{-2}$ through $T_5$ proof layer equals $0$.
background
The module replaces the former vacuous zero_knobs_policy certificate (a reflexivity proof of $0=0$) with an explicit input ledger. The 2026 honesty pass and internal audit (Thapa, T−2..T5 forcing report, §11) required naming every discrete modeling input, convention, and calibration the forcing layer consumes.
“Zero adjustable parameters” survives only in a narrow sense: no continuous parameter is fit to data. Discrete structural choices (ledger entries, conventions, calibrations) are real inputs and are enumerated as such. This constant isolates that continuous-parameter count.
The surrounding ledger siblings record the discrete inputs and their cardinality; this definition is the continuous half of the split claim.
proof idea
Definitional assignment: the natural number is set equal to $0$ by :=. No lemmas, tactics, or proof obligations. The companion theorem is then a one-line rfl simp fact.
why it matters
Feeds the simp theorem that the fitted continuous-parameter count equals zero, which is the auditable survivor of the old zero-knobs language. In the Recognition framework this sits at the verification boundary of the forcing chain (T0–T8 landmarks: J-uniqueness, $\varphi$ fixed point, eight-tick octave, $D=3$): those steps are structural, not continuous fits to data.
The declaration exists so referees can separate “no continuous free parameters in T−2..T5” from “no inputs at all.” Discrete ledger entries remain named inputs; only the continuous fit count is zero. That split is the point of the 2026 honesty pass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.