MetricAliasing
plain-language theorem explainer
Packages a sampling period, Nyquist frequency, and nonnegative aliasing-noise amplitude with positivity witnesses. Verification and pulsar-timing work cite it as the data shape for discrete-update metric noise. It is a pure structure definition: no proof obligations beyond the two inequality fields.
Claim. A metric-aliasing record is a 5-tuple $(T, f_N, A, h_T, h_A)$ with sampling period $T \in \mathbb{R}$, Nyquist frequency $f_N \in \mathbb{R}$, noise amplitude $A \in \mathbb{R}$, proof $h_T : 0 < T$, and proof $h_A : 0 \leq A$. Intended reading: $f_N = 1/(2T)$ and $A$ is the dimensionless floor from discrete metric updates.
background
Recognition Science treats time as discrete at the fundamental tick $\tau_0$ (Constants.tick $= 1$ in RS-native units). The eight-tick octave $\tau_8 = 8\tau_0$ is the forced evolution period from the T7 step of the forcing chain. Continuous signals sampled on that lattice fold above the Nyquist limit $1/(2T)$ and leave a staircase residual in the metric.
This module (Verification.LedgerHum) packages that residual as an observable floor for LIGO and pulsar timing arrays. Upstream, period k := $\phi^k$ and period_pos supply positive $\phi$-ladder timescales used elsewhere in the pulsar stack; here the sampling period is the octave tick rather than a rung period.
The structure itself only records $T$, $f_N$, $A$ and the two sign constraints. Concrete RS values are filled by the sibling constructor that sets $T = \tau_8$, $f_N = 1/(2\tau_8)$, and $A = \phi^{-1}$.
proof idea
No proof body: this is a structure declaration. The two Prop fields period_pos and noise_nonneg are ordinary inequality hypotheses that any inhabitant must supply. Downstream rsMetricAliasing discharges them via tau_8_pos and a short nonnegativity argument for $\phi^{-1}$.
why it matters
Gives the typed carrier for the ledger-hum metric-noise claim. Parent rsMetricAliasing instantiates it from the 8-tick structure (T7 octave), with noise amplitude $\phi^{-1}$ (Berry-scale decay). ledgerHumStatus reports the structure as one of the checklist lines in the minimal verification protocol.
In the broader framework this is the interface between discrete recognition updates and continuous gravitational-wave observables: aliasing at the $\tau_0$ (or $\tau_8$) scale is the predicted noise floor that PTA/LIGO campaigns are approaching. It does not itself compute a residual in seconds; siblings pulsarResidualSignature and stackedResidual turn the amplitude into nanosecond-scale forecasts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.