module module moderate

`IndisputableMonolith.Verification.LedgerHum`

Verification layer that packages the recognition ledger's atomic tick τ₀ and the eight-tick period τ₈, then builds pulsar-timing residual signatures that would expose metric aliasing if the discrete ledger is real. Observers of RS timing predictions cite it. The module is mostly definitions and positivity lemmas plus a named falsifier structure, not a deep proof chain.

claimThe module fixes the fundamental tick $\tau_0>0$ and the eight-tick interval $\tau_8=8\tau_0>0$, defines RS metric-aliasing residuals and a pulsar residual signature at nanosecond scale, and packages a stacked residual observable together with a pulsar-timing falsifier for discrete ledger updates.

background

Recognition Science updates spacetime in discrete ledger steps. From the eight-tick forcing step, the atomic time quantum is $\tau_0$ (one tick in RS-native units), with physical scale about $7.30\times 10^{-15},\mathrm{s}$, derived rather than fitted. The octave period is $\tau_8=8\tau_0$.

This verification module sits on Constants (which supplies the RS-native $\tau_0=1$ tick) and Patterns. It introduces metric aliasing: the mismatch between continuous metric time and the discrete recognition clock. Residuals of that mismatch, especially when stacked over many pulses, are the observable the module prepares.

Sibling objects include positivity of $\tau_0$ and $\tau_8$, an RS metric-aliasing predicate, a pulsar residual signature claimed to sit at nanosecond scale, a stacked residual, and an explicit PulsarTimingFalsifier bundle.

proof idea

Definition-and-interface module rather than a single theorem. It binds $\tau_0$ and $\tau_8$ from the constants layer, records positivity, then defines aliasing and residual signatures as structured Props or data. Scale claims (nanosecond signature, $\sqrt{10^8}$ stacking factor) are short algebraic or numerical lemmas. The falsifier is a packaged hypothesis interface for downstream timing tests, not a discharged proof.

why it matters in Recognition Science

Gives the verification domain a concrete timing hook for the discrete ledger: if recognition updates on $\tau_0$ with eight-tick structure (T6/T7 in the forcing chain), pulsar timing arrays should see a characteristic residual signature rather than pure noise. No downstream Lean consumers are wired yet (used_by empty), so the module is a source package for observational falsifiers and stacked-residual claims. It ties the abstract tick to a named pulsar-timing falsifier path without claiming a detection.

scope and limits

Does not prove that pulsars exhibit the residual; only defines the signature and falsifier interface.
Does not derive τ₀'s SI value inside this module; that sits in Constants or upstream forcing.
Does not claim a completed observational test or data reduction pipeline.
Does not feed named parent theorems yet; used_by is empty.
Does not address non-pulsar clocks or continuous-limit GR timing beyond aliasing residuals.

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