DatasetAttachment
plain-language theorem explainer
A six-field record that binds one quantum-gravity falsifier-register row to a named observational channel, units, numerical sensitivity, RS target scale, and an honest flag for whether current data already reach that scale. Verification and phenomenology authors cite it when wiring concrete datasets (Planck, GWTC-3, DESI, MAQRO-class, etc.) into the register. It is a plain structure definition with no proof obligations.
Claim. A dataset attachment is a record $(s, d, u, \sigma, \tau, c)$ where $s$ is the physics sector label, $d$ the named dataset or channel, $u$ the unit string, $\sigma \in \mathbb{R}$ the reported sensitivity, $\tau \in \mathbb{R}$ the Recognition Science target scale (dimensionless unless $u$ says otherwise), and $c \in \{\mathrm{true},\mathrm{false}\}$ whether present data already reach $\tau$.
background
This module implements the quantum-gravity master-plan §7 falsifier register as Lean data. Status is structural: zero sorry and no new RS-internal axioms. The point is falsifiability accounting, not empirical confirmation of Recognition Science.
Each register row needs four pieces of bookkeeping: a named observational channel, a numerical sensitivity, an RS target scale or band, and an honest flag saying whether current instruments already probe that target. Several future channels (MAQRO-class BMV, analog Hawking temperature) are attached with the flag set false.
Anchor examples in the module header include Planck 2018 $\Omega_\Lambda$, DESI/Planck $w_0$, Cassini Shapiro delay, EHT M87* shadow size, GRAVITY S2 precession, NANOGrav/EPTA PTA spectra, and GWTC-3 ringdown/echo bounds. Sensitivity and target scale are treated as dimensionless reals unless the units field overrides that convention.
proof idea
No proof. The declaration is a Lean structure with six fields (three strings, two reals, one Bool). Downstream named rows are ordinary structure instances that fill those fields; positivity of sensitivity and target scale is expressed separately by the predicates HasPositiveSensitivity and HasPositiveTargetScale.
why it matters
This is the common carrier type for every concrete falsifier-register attachment in the module: BMV phase-rate, Hawking temperature, leading-log entropy, page-curve, echo amplitude, $\Omega_\Lambda$, dark-energy $w(z)$, QNM, and PTA rows all inhabit it. Downstream predicates require positive sensitivity and positive RS target scale on any such record.
In the Recognition framework the structure turns abstract $\varphi$-ladder targets (for example echo damping near $\varphi^{-1}$, or the tiny $\varphi^{-44}z$ dark-energy scale) into auditable dataset comparisons. It does not claim confirmation; it only makes explicit which experiment tests which prediction and at what reported precision, which is the verification layer sitting above the forcing chain and mass/ladder formulae.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.