growth_suppression_scale_separation
plain-language theorem explainer
The theorem establishes that recognition strain vanishes for all wavenumbers at or below the 8-tick scale. Cosmologists addressing the σ8 tension cite it to justify why large-scale structure growth matches ΛCDM while small scales experience suppression. The proof is a direct simplification that unfolds the piecewise definition of strainAtScale once the inequality hypothesis is supplied.
Claim. Let $k, k_8$ be real numbers with $k_8 > 0$. If $k ≤ k_8$, then the recognition strain at wavenumber $k$ relative to the 8-tick scale equals zero.
background
Recognition Science models structure growth via the recognition operator whose strain accumulates from 8-tick cycles. The auxiliary definition strainAtScale implements this as a piecewise function: zero when the input wavenumber lies at or below the 8-tick wavenumber k8, and equal to Jcost(k/k8) otherwise. This implements the scale separation stated in the module, where the 8-tick neutrality constraint introduces a characteristic wavenumber below which growth proceeds unsuppressed.
proof idea
The proof is a one-line wrapper. It introduces the hypothesis k ≤ k8 and then applies simp to the definition of strainAtScale together with the inequality, reducing the conditional expression to the zero branch.
why it matters
The result supplies the large_scale_unsuppressed field inside the σ8 Suppression Certificate sigma8Suppression_verified. It thereby closes the scale-separation step that links the eight-tick octave (T7) to the predicted suppression factor (1 - Q/Q_max) used to reconcile Planck CMB and weak-lensing values of σ8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.