rsMetricAliasing
plain-language theorem explainer
Packages the Recognition Science metric-aliasing parameters fixed by the eight-tick octave: sampling period τ₈, Nyquist frequency 1/(2τ₈), and dimensionless noise amplitude φ⁻¹. Anyone citing discrete spacetime sampling or pulsar residual noise floors would use this record. The body is a structure instance: field assignments plus two positivity proofs.
Claim. The RS metric-aliasing datum with sampling period $\tau_8$ (one eight-tick cycle), Nyquist frequency $1/(2\tau_8)$, and aliasing noise amplitude $\varphi^{-1}$, together with proofs that $\tau_8>0$ and $\varphi^{-1}\ge 0$.
background
In the LedgerHum verification module, continuous signals on a discretely updating spacetime are treated as sampled at a finite rate. The structure MetricAliasing records that sampling period, the associated Nyquist frequency $1/(2\cdot\mathrm{period})$, a dimensionless aliasing-noise amplitude, and the positivity side-conditions.
The fundamental RS time quantum is one tick $\tau_0=1$ (RS-native). One octave is eight ticks: the forced evolution period from the T7 step of the forcing chain. Here $\tau_8$ is that eight-tick duration, and $\varphi$ is the unique self-similar fixed point forced at T6. The noise floor is set to the Berry-scale amplitude $\varphi^{-1}$.
Upstream positivity for powers of $\varphi$ (e.g. period positivity in the pulsar-emission regimes) and the tick/octave constants supply the arithmetic background; this definition specializes them to the eight-tick sampling channel.
proof idea
Definitional instance of MetricAliasing. Sampling period is set to $\tau_8$; Nyquist frequency is the literal reciprocal $1/(2\tau_8)$; noise amplitude is $\varphi^{-1}$. Period positivity is the sibling lemma $\tau_8>0$. Nonnegativity of noise is one inequality step: $\varphi>0$ implies $\varphi^{-1}>0$, hence $\varphi^{-1}\ge 0$ via le_of_lt.
why it matters
Gives the concrete RS sampling channel used by the stacked-residual and pulsar-timing falsifier story in the same module: if spacetime updates on the eight-tick octave, continuous metric signals alias above the Nyquist cut and leave a $\varphi^{-1}$-scaled noise floor at the $\tau_8$ scale. That feeds the module's $\sim 10,\mathrm{ns}$ stacked-residual prediction (geometric stacking of many pulse arrivals times path-length factors).
Framework landmarks: T7 (eight-tick octave, period $2^3$) fixes the sampling period; T6 ($\varphi$) fixes the noise amplitude at the Berry threshold $\varphi^{-1}$. No downstream theorems yet list this definition as a dependency, so it is presently a named parameter pack for the verification layer rather than a proved bridge theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.