module module high

`IndisputableMonolith.Verification.FalsifierRegisterDatasets`

Shared dataset-attachment record for every §7 falsifier-register row. Each attachment packages a named survey with dimensionless sensitivity, RS target scale, units, and a flag for whether the data already reach the φ-suppressed target. Downstream likelihood modules import these records as the structural base for Cassini, EHT, GRAVITY, PTA, ringdown, and dark-energy certificates. Pure definitions; no proofs.

claimA dataset attachment is a record packing a dataset name, dimensionless sensitivity $s$, RS target scale $\sigma_{\mathrm{RS}}$, optional units, and a boolean $\mathrm{currentlySensitive}$ recording whether $s$ already reaches $\sigma_{\mathrm{RS}}$. Concrete attachments (echo, QNM, PTA, $\Omega_\Lambda$, dark-energy $w$, strong-field probes, etc.) instantiate this record for named observational programs.

background

In Recognition Science verification, §7 of the falsifier register lists observational tests that could defeat RS predictions: strong-field GR deviations, stochastic GW backgrounds, dark-energy equation of state, black-hole thermodynamics and echoes. Each row needs a uniform handle for the dataset that would perform the test.

This module introduces that handle. Sensitivity and RS target scale are dimensionless unless the units field says otherwise. The currentlySensitive flag is honest: several future rows name a survey that cannot yet reach the φ-suppressed target, so the flag is false.

Predicates require positive sensitivity and positive target scale for well-formed rows. Named constants fix the concrete catalogue (BMV, Hawking temperature, leading-log entropy, Page curve, echoes, $\Omega_\Lambda$, dark-energy $w$, QNMs, PTA) used by later likelihood upgrades.

proof idea

This is a definition module, no proofs. It declares the dataset-attachment structure, positivity predicates on sensitivity and target scale, and a catalogue of concrete attachment values for the named §7 falsifier rows.

why it matters in Recognition Science

Feeds every §7 likelihood certificate that upgrades a bare attachment into a dataset-specific structural theorem. Downstream importers include Cassini strong-field, EHT M87*, GRAVITY S2, EPTA DR2 PTA, NANOGrav PTA, Planck/BAO/SNe dark-energy $w$, Planck $\Omega_\Lambda$, and GWTC-3 ringdown/echo/QNM status modules. Those modules treat this catalogue as the shared substrate so sensitivity flags and target scales stay consistent across the falsifier register. Without a single attachment type, each likelihood module would reinvent dataset metadata.

scope and limits

Does not compute likelihoods, posteriors, or χ² statistics.
Does not claim that currentlySensitive datasets confirm or falsify RS.
Does not derive φ-suppressed target scales from first principles.
Does not ship raw observational data tables or covariances.
Does not prove physical reach beyond the recorded boolean flag.

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