module module high

`IndisputableMonolith.Verification.FalsifierRegisterDatasets`

Shared dataset-attachment records for the Recognition Science falsifier register. Each row names an observational handle, a dimensionless sensitivity, an RS target scale, and a flag for whether the data already reach that scale. Downstream likelihood modules import these attachments to upgrade §7 falsifier rows into dataset-specific certificates. The module is pure data structure: no theorems, only typed records and positivity predicates.

claimA dataset attachment is a record $(name, sensitivity, rsTargetScale, units, currentlySensitive)$ for one falsifier-register row. Sensitivity and RS target scale are dimensionless unless $units$ says otherwise. The flag $currentlySensitive$ is true precisely when the named dataset can already probe the $\varphi$-suppressed RS target; otherwise the row is named but not yet decisive.

background

Recognition Science states sharp, often $\varphi$-suppressed targets for strong-field gravity, dark energy $w(z)$, ringdown/echoes, and pulsar-timing stochastic GW backgrounds. The falsifier register (§7) lists those targets against named observational programs. Before a likelihood certificate can be written, each row needs a stable handle: which dataset, what sensitivity, what RS scale, and whether the data already reach that scale.

This module supplies that handle type and the concrete attachments (BMV, Hawking temperature, leading-log entropy, Page curve, echoes, $\Omega_\Lambda$, dark-energy $w$, QNMs, PTA, and related rows). Two small predicates record that sensitivity and target scale are positive. Units default to dimensionless; the field units overrides when a dimensionful convention is required.

The design is deliberately honest about reach: several future rows set currentlySensitive := false, so the register names the experiment without claiming a present-day test of the $\varphi$-ladder prediction.

proof idea

This is a definition module, no proofs. It introduces the DatasetAttachment structure, positivity predicates on sensitivity and RS target scale, and a family of concrete attachment values (one per falsifier-register row). Downstream modules import the records and build likelihood-style certificates on top of them.

why it matters in Recognition Science

Every §7 likelihood upgrade in the Verification layer imports this module. Downstream consumers include Cassini strong-field, GRAVITY S2, EHT M87*, Planck/BAO/SNe dark-energy $w$, $\Omega_\Lambda$, GWTC-3 ringdown/echo/QNM status, EPTA DR2 PTA, and NANOGrav PTA attachments. Those modules are marked structural theorems (0 sorry, 0 RS-internal axiom) that turn bare register rows into dataset-specific certificates.

Without a shared attachment type, each likelihood module would re-encode dataset metadata ad hoc. Centralizing the records keeps the falsifier register uniform: same fields, same honesty about current sensitivity, same path from $\varphi$-suppressed target to observational handle. The module therefore sits under the verification spine rather than under the forcing chain (T0–T8); it does not derive constants, but it makes the empirical claims of RS checkable against named data.

scope and limits

Does not prove any observational bound or likelihood inequality.
Does not claim currentlySensitive datasets already falsify or confirm RS targets.
Does not derive sensitivity or rsTargetScale from first principles.
Does not encode full instrument response, covariance, or selection functions.
Does not replace the §7 falsifier statements themselves; only their dataset handles.

used by (9)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Verification.CassiniStrongFieldLikelihood module_import
IndisputableMonolith.Verification.DarkEnergyWPlanckLikelihood module_import
IndisputableMonolith.Verification.EHTM87StrongFieldLikelihood module_import
IndisputableMonolith.Verification.EPTAPTALikelihood module_import
IndisputableMonolith.Verification.GravityS2StrongFieldLikelihood module_import
IndisputableMonolith.Verification.GWTC3RingdownStatus module_import
IndisputableMonolith.Verification.NANOGravPTALikelihood module_import
IndisputableMonolith.Verification.OmegaLambdaPlanckLikelihood module_import
IndisputableMonolith.Verification.Track6FalsifierSensitivity module_import

declarations in this module (37)

structure DatasetAttachment L61
def HasPositiveSensitivity L70
def HasPositiveTargetScale L74
def bmvAttachment L84
def hawkingTemperatureAttachment L96
def leadingLogEntropyAttachment L108
def pageCurveAttachment L120
def echoAttachment L132
def omegaLambdaAttachment L144
def darkEnergyWAttachment L158
def qnmAttachment L172
def ptaAttachment L187
def strongFieldAttachment L200
theorem bmv_sensitivity_pos L210
theorem hawking_sensitivity_pos L214
theorem leadingLog_sensitivity_pos L219
theorem pageCurve_sensitivity_pos L224
theorem echo_sensitivity_pos L229
theorem omegaLambda_sensitivity_pos L233
theorem darkEnergyW_sensitivity_pos L238
theorem qnm_sensitivity_pos L243
theorem pta_sensitivity_pos L247
theorem strongField_sensitivity_pos L251
theorem bmv_target_pos L258
theorem hawking_target_pos L262
theorem leadingLog_target_pos L267
theorem pageCurve_target_pos L272
theorem echo_target_pos L277
theorem omegaLambda_target_pos L281
theorem darkEnergyW_target_pos L286
theorem qnm_target_pos L291
theorem pta_target_pos L295
theorem strongField_target_pos L299
structure FalsifierDatasetRegisterCert L309
def falsifierDatasetRegisterCert L331
theorem falsifierDatasetRegisterCert_inhabited L353
theorem falsifier_dataset_register_one_statement L359