strainAtScale
plain-language theorem explainer
The definition strainAtScale computes the recognition strain Q at wavenumber k relative to the 8-tick scale k8. Cosmologists modeling the σ8 tension cite it to quantify scale-dependent suppression of structure growth in the Recognition Science framework. It is implemented as a piecewise function that returns zero below k8 and applies the J-cost to the ratio k/k8 above that threshold.
Claim. The recognition strain at wavenumber $k$ relative to the 8-tick wavenumber $k_8$ is $Q(k,k_8)=0$ if $k≤k_8$ and $J(k/k_8)$ otherwise, where $J$ is the J-cost function measuring recognition cost of a ratio.
background
In Recognition Science the 8-tick octave (T7) fixes a neutrality scale λ8 = 2π/k8 below which structure growth is suppressed by cumulative recognition strain. The J-cost function satisfies the Recognition Composition Law and is evaluated at the golden-ratio fixed point φ for the maximum per-cycle strain Q_max. The module addresses the σ8 tension between Planck CMB values (≈0.811) and weak-lensing measurements (≈0.76) by introducing scale-dependent suppression via the recognition operator. Upstream results establish the tick as the fundamental time quantum τ0=1 and confirm that Q_max equals J(φ).
proof idea
This is a direct definition that encodes the piecewise rule stated in the doc-comment. It applies the conditional expression with the Jcost function imported from the Cost module, returning zero on the large-scale side of k8 and the normalized J-cost on the small-scale side.
why it matters
strainAtScale supplies the core strain function required by the growth_suppression_scale_separation theorem and the Sigma8SuppressionCert structure. It implements the strain-accumulation step in the Recognition Science account of the σ8 tension, linking the eight-tick constraint to the predicted suppression factor (1−Q/Q_max) that matches weak-lensing data to within 2σ. The definition closes the interface between the phi-ladder and observable cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.