inputLedger
plain-language theorem explainer
An explicit nine-entry ledger of every discrete modeling input, convention, and bridge hypothesis consumed by the T−2..T5 forcing layer. Auditors and anyone citing the “zero knobs” claim use it: continuous fitted parameters are zero, but these named discrete inputs are real. The body is a literal list of structured triples (name, kind, where used).
Claim. The T−2..T5 input ledger is the finite list of nine named discrete inputs, each a triple (name, kind, locus of use), with kinds among structural choice, convention/normalization, and bridge hypothesis. Entries cover the distinguishability floor, Boolean orientation, unit recognition cost, the positive-ratio continuum carrier, finite polynomial closure of the composition law, bilinear coefficient $c=2$, diagonal normalization $P(1,1)=6$, log-curvature $\lambda=1$, and hyperbolic branch selection for $J$.
background
The module replaces a former vacuous 0 = 0 “zero knobs” certificate. The 2026 audit (Thapa, T−2..T5 forcing report, §11) required an honest enumeration: “zero adjustable parameters” holds only for continuous parameters fit to data; discrete structural choices remain genuine inputs.
A ledgered input is a triple of strings: a human name, a kind (structural choice, convention/normalization, or bridge hypothesis), and a short note on where it enters the chain. The list sits under the Recognition Composition Law and J-uniqueness (T5): $J(x)=\cosh(\log x)-1$, forced among the family $\cosh(\lambda\log x)-1$ once $\lambda=1$ and the hyperbolic branch are fixed, with combiner polynomial $P(u,v)=2uv+2u+2v$.
Upstream cost and recognizer machinery (J-cost on recognition events, multiplicative recognizer derived cost, rung-coarsen weighted sums) consume these choices; the ledger does not re-derive them, it names what was assumed before T5 characterization.
proof idea
Definition by literal list construction: nine structure values of type LedgeredInput, each an anonymous constructor with three string fields. No tactics, no lemmas, no computation beyond the list literal. Downstream length and non-emptiness proofs reduce by rfl / simp on this closed term.
why it matters
This is the honesty anchor for the Verification.KnobsCount story. It feeds inputLedger_nonempty (the framework has named inputs) and inputLedger_count (length equals 9), which in turn support the narrow claim that the number of continuous parameters fit to empirical data in the T−2..T5 layer is zero.
In the forcing chain it documents the discrete residue before and through T5 J-uniqueness and the RCL polynomial normalizations ($c=2$, $P(1,1)=6$, $\lambda=1$, hyperbolic branch). Without this ledger, “zero knobs” reads as a slogan; with it, referees can see exactly which structural choices and bridge hypotheses (including the positive-ratio continuum carrier toward T4→T5) remain outside pure logic.
It does not close open physics questions; it makes the input surface of the early forcing layer auditable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.