IndisputableMonolith.Verification.FalsifierRegisterDatasets

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