r_prediction
plain-language theorem explainer
Recognition Science predicts the tensor-to-scalar ratio satisfies 0.1 < r < 0.2 as a direct consequence of J-cost fluctuations on the phi-ladder. Cosmologists testing CMB polarization data against RS models would cite this interval as a falsifiable window. The proof unfolds the definition of rs_prediction_r then sandwiches (phi-1)^4 between explicit fourth powers of 0.61 and 0.62 using the supplied phi bounds and monotonicity of x^4.
Claim. $0.1 < r < 0.2$, where $r$ is the Recognition Science prediction for the tensor-to-scalar ratio given by $(phi-1)^4$.
background
Module COS-009 derives the primordial power spectrum from J-cost quantum fluctuations during inflation. The phi-ladder fixes the spectral tilt while the amplitude follows from the same cost function that governs mass ladders elsewhere in the framework. Upstream lemmas one_lt_phi, phi_gt_onePointSixOne and phi_lt_onePointSixTwo supply the concrete interval 1.61 < phi < 1.62 that drives the numerical bound.
proof idea
Unfold rs_prediction_r to (phi-1)^4. Apply phi_gt_onePointSixOne and phi_lt_onePointSixTwo to obtain 0.61 < phi-1 < 0.62. Verify 0.61^4 > 0.1 and 0.62^4 < 0.2 by norm_num. Use pow_lt_pow_left₀ twice, once for each side of the sandwich, together with linarith on positivity of phi-1.
why it matters
The result supplies an explicit numerical window for the tensor-to-scalar ratio inside the RS derivation of the primordial spectrum (COS-009). It rests on the phi fixed-point property (T6) and the eight-tick octave structure that forces D=3. No downstream theorems yet consume the bound, leaving open its insertion into a full power-spectrum pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.