strainAtScale
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not integrate strain over cosmic time or multiple cycles.
- Does not include baryonic or astrophysical feedback terms.
- Does not derive the numerical value of k8 from first principles.
- Does not address the Hubble tension or other cosmological discrepancies.
Lean usage
example (k k8 : ℝ) (hk8_pos : 0 < k8) (h : k ≤ k8) : strainAtScale k k8 = 0 := by simp [strainAtScale, h]formal statement (Lean)
74noncomputable def strainAtScale (k k8 : ℝ) : ℝ :=
proof body
Definition body.
75 if k ≤ k8 then 0 else Jcost (k / k8)
76
77/-- The maximum strain from a single 8-tick cycle.
78
79 Q_max = J(φ) since the maximum stable ratio in a cycle is φ. -/