LedgeredInput
plain-language theorem explainer
A three-field record for one discrete modeling input in the T−2..T5 audit ledger: a human-readable name, a kind tag (structural choice, convention/normalization, or bridge hypothesis), and a locus of use. Downstream code builds the explicit input list from these records. There is no proof body; it is a plain data structure with decidable equality.
Claim. A ledgered input is a triple $(n,k,w)$ where $n$ is a name string, $k$ is a kind string drawn from structural choice, convention/normalization, or bridge hypothesis, and $w$ records where in the T−2..T5 layer the input is consumed.
background
The Verification.KnobsCount module replaces a former vacuous 0 = 0 certificate with an explicit input ledger. The module doc states the honesty goal: "Zero adjustable parameters" holds only in the narrow sense that no continuous parameter is fit to data; discrete structural choices, conventions, and bridge hypotheses remain real inputs and must be named.
This structure is the row type for that ledger. Each row carries a name, a kind tag (the comment lists the three allowed labels), and a where_used locus tying the input to a step in the forcing chain (T−1 floor through T5 characterization). The T−2..T5 layer is the early forcing segment that ends at J-uniqueness (T5: $J(x)=(x+x^{-1})/2-1$).
Upstream edges touch foundation and cosmology modules only as ambient context for the ledger entries; the structure itself does not depend on their theorems.
proof idea
No proof. The declaration is a structure with three String fields and automatic Repr and DecidableEq instances. Kind values are documented by comment as the three audit categories rather than enforced by a sum type.
why it matters
This is the atomic type behind inputLedger, the enumerated list that implements audit §11 for the T−2..T5 layer. Parent use builds five concrete rows (observational distinguishability at the T−1 floor, marked pair/orientation for the Boolean projection, unit-cost Bool indicator at T0, positive-ratio continuum carrier as a T4→T5 bridge hypothesis, and finite polynomial closure/composition law at T5).
In the Recognition framework it makes the "no fitted continuous knobs" claim auditable instead of rhetorical: continuous free parameters are claimed absent, while discrete structural inputs are listed in the open. It sits upstream of any count or emptiness claim about fitted continuous parameters in the same module, and anchors honesty about what the forcing chain still consumes before J-uniqueness and the later phi, eight-tick, and $D=3$ steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.