module module

`IndisputableMonolith.Verification.LedgerHum`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Patterns module_import

declarations in this module (27)

def tau_0 L34
def tau_8 L42
theorem tau_0_pos L45
theorem tau_8_pos L50
structure MetricAliasing L66
def rsMetricAliasing L79
def pulsarResidualSignature L104
theorem signature_is_nanosecond_scale L107
def stackedResidual L115
lemma sqrt_10_pow_8 L119
theorem stacked_residual_observable L125
structure PulsarTimingFalsifier L154
def detectionThreshold L167
def falsifiesEightTick L171
def strongDetection L175
structure LIGONoiseFloor L189
def rsSpectralSlope L198
def ligoConsistentWithAliasing L201
structure LedgerHumFalsifier L213
def crossCorrelationPredicted L222
def ledgerHumFalsified L226
def ledgerHumConfirmed L232
structure MeasurementProtocol L256
def minimalProtocol L267
def protocolValid L274
theorem minimalProtocol_valid L281
def ledgerHumStatus L297