inputLedger_count
plain-language theorem explainer
The T−2..T5 input ledger contains exactly nine discrete modeling inputs. Auditors of the Recognition Science forcing layer cite this as the concrete count behind the honest “no continuous fitted parameters” claim. The proof is pure reflexivity: length of the explicitly written list equals nine by definition.
Claim. The enumerated input ledger for the $T_{-2}$ through $T_5$ layer has length exactly $9$.
background
This module replaces a former vacuous certificate (a reflexivity proof of $0=0$ marketed as “zero knobs”) with an explicit ledger of every discrete modeling input, convention, and calibration the $T_{-2}$..$T_5$ layer consumes. The 2026 internal audit (Thapa, forcing report §11) flagged the old statement as empty; the ledger is the opposite of empty.
Each ledger entry is a named triple: description, kind (structural choice or bridge hypothesis), and the layer it feeds. Entries include the observational distinguishability structure at the $T_{-1}$ floor, the marked-pair orientation for Boolean projection, the unit-cost Bool indicator at $T_0$, the positive-ratio continuum carrier bridging $T_4$ to $T_5$, and the finite polynomial closure (composition law) used in the $T_5$ characterization. “Zero adjustable parameters” is retained only in the narrow sense that no continuous parameter is fit to data; these discrete choices are real inputs and are counted as such.
proof idea
One-line term proof by reflexivity. The ledger is a closed nine-element list literal; List.length evaluates definitionally to $9$, so rfl closes the goal. No lemmas are invoked beyond that computation.
why it matters
This count is the quantitative half of the honesty pass that retired the vacuous zero-knobs policy. Paired with the sibling claim that the number of continuous parameters fit to empirical data is zero, it states precisely what the framework consumes at $T_{-2}$..$T_5$: nine named discrete inputs, zero fitted continuous knobs.
The forcing-chain landmarks above the ledger (T5 $J$-uniqueness via the Recognition Composition Law, T6 $\varphi$ as self-similar fixed point, T7 eight-tick octave, T8 $D=3$) rest on these structural choices; the ledger does not derive those theorems, it only inventories the inputs they presuppose. The dependency graph currently shows no downstream consumers of the count itself; its role is audit transparency rather than a proof stepping-stone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.