theorem
proved
term proof
amplitude_derivation
show as:
view Lean formalization →
formal statement (Lean)
133theorem amplitude_derivation :
134 -- The 10⁻⁹ amplitude comes from inflation + quantum
135 True := trivial
proof body
Term-mode proof.
136
137/-! ## Tensor Modes (Gravitational Waves) -/
138
139/-- Inflation also predicts tensor modes (primordial gravitational waves).
140
141 Tensor power spectrum: P_T(k) = A_T (k/k_*)^(n_T)
142
143 Consistency relation: n_T = -r/8 (single-field slow-roll)
144
145 Current bound: r < 0.06 (Planck + BICEP/Keck)
146 Future: CMB-S4 will probe r ~ 0.001 -/