stackedResidual
plain-language theorem explainer
The stacked residual after N independent samples equals the eight-tick period times √N. Pulsar-timing and ledger-hum verification cite this as the random-walk growth of the residual under discrete recognition ticks. The body is a one-line scaling definition: τ₈ multiplied by the square root of the stack size.
Claim. For $N \in \mathbb{N}$, the stacked residual is $\tau_8 \sqrt{N}$, where $\tau_8 = 8\tau_0$ is the eight-tick recognition period ($\tau_8 \approx 5.84 \times 10^{-14}\,\mathrm{s}$).
background
In the ledger-hum verification module, discrete recognition updates run on an eight-tick octave. The fundamental tick $\tau_0$ sets the base time unit; the complete cycle is $\tau_8 = 8\tau_0$, documented as the fundamental period of spacetime updates ($\approx 5.84 \times 10^{-14},\mathrm{s}$). That period is the T7 landmark in the forcing chain.
The stacking model treats successive residuals as a discrete-time random walk: uncorrelated increments add in quadrature, so the coherent residual amplitude grows as $\sqrt{N}$ rather than linearly in $N$. Multiplying the single-cycle scale $\tau_8$ by $\sqrt{N}$ converts stack size into a predicted residual time.
Sibling material in the same module (metric aliasing, pulsar residual signature at nanosecond scale, and the observability theorem for $N \sim 10^8$) uses this scale as the bridge from the eight-tick clock to a laboratory-facing timing residual.
proof idea
Pure definition, not a proved statement. The body multiplies the upstream constant $\tau_8$ by Real.sqrt N. No lemmas or tactics; noncomputable only because it lands in $\mathbb{R}$ via the real square root.
why it matters
Gives the $\sqrt{N}$ stacking law that the module status string reports as part of the minimal ledger-hum protocol, and that the observability theorem instantiates at $N = 10^8$ to show the residual exceeds $10^{-10},\mathrm{s}$. Downstream, that theorem records the arithmetic $8 \cdot 7.30\times 10^{-15} \cdot 10^4 \approx 5.84\times 10^{-10} > 10^{-10}$.
Framework-wise it sits on T7 (eight-tick octave): the residual yardstick is exactly one full recognition period, then random-walk stacked. It does not itself close a forcing step; it turns the eight-tick clock into a falsifiable pulsar-timing / ledger-hum prediction once $N$ is large enough.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.