Pith. sign in
module module moderate

IndisputableMonolith.Verification.LedgerHum

show as:
view Lean formalization →

Module packaging the fundamental recognition tick τ₀, the eight-tick period τ₈, and pulsar-timing residual signatures that would expose discrete ledger updates. Verification and observational groups cite it for the nanosecond-scale stacked-residual prediction and the PulsarTimingFalsifier interface. Content is definitions, positivity facts, and falsifier scaffolding rather than a deep proof chain.

claimThe module defines the fundamental ledger tick $\tau_0$ and eight-tick $\tau_8=8\tau_0$ (both positive), metric aliasing of residual signatures, a pulsar residual signature at nanosecond scale, stacked residuals after $10^8$-fold averaging, and a pulsar-timing falsifier for discrete spacetime updates.

background

Recognition Science updates spacetime in discrete steps fixed by the eight-tick octave. The module doc identifies $\tau_0$ as the atomic ledger time unit, with derived SI scale $\tau_0\approx 7.30\times 10^{-15},\mathrm{s}$ (not a fit). In RS-native units the Constants import sets the time quantum so that one tick is $1$; Patterns supplies the combinatorial octave structure behind the factor of eight.

When a continuous timing model is fit to a discrete update process, a residual "ledger hum" remains. This module names that imprint: metric aliasing maps the tick structure into the timing metric; pulsar residual signatures and stacked residuals turn it into an observable after folding many pulses. The target scale is nanoseconds once $\sim 10^8$ residuals are stacked.

proof idea

Definition-and-interface module, not a single theorem proof. It introduces $\tau_0$ and $\tau_8$ as constants, records positivity, then packages MetricAliasing / rsMetricAliasing, pulsarResidualSignature, stackedResidual (via $\sqrt{10^8}$ scaling), and the observability lemmas that pin the nanosecond band. PulsarTimingFalsifier stands as the hypothesis-style object an empirical test would discharge or refute. No deep tactic chain; structure is declarations plus short positivity and scale facts.

why it matters in Recognition Science

Anchors the eight-tick octave (forcing-chain landmark, module text T6 / primer T7) in a concrete observational channel: pulsar timing residuals. Gives verification a named falsifier rather than a purely formal tick. The graph currently lists no downstream used_by edges, so this module is a leaf verification surface: parent status is "feeds empirical closure of discrete ledger time" rather than a named Lean consumer. Ties the abstract $\tau_0=1$ tick from Constants to an SI-scale, stackable residual prediction without touching mass-ladder or $\alpha$ results.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (27)