def
definition
def or abbrev
observedSpectrum
show as:
view Lean formalization →
formal statement (Lean)
74noncomputable def observedSpectrum : PowerSpectrum := {
proof body
Definition body.
75 amplitude := scalar_amplitude_observed,
76 spectral_index := spectral_index_observed,
77 pivot_scale := 0.05, -- Mpc⁻¹
78 amplitude_pos := by unfold scalar_amplitude_observed; norm_num,
79 pivot_pos := by norm_num
80}
81
82/-! ## φ-Connection Analysis -/
83
84/-- Analysis of n_s - 1 ≈ -0.035:
85
86 Possible φ-connections:
87 1. |n_s - 1| = (φ - 1)² = 0.382² = 0.146 (too large)
88 2. |n_s - 1| = (φ - 1)³ = 0.236 × 0.382 = 0.090 (still large)
89 3. |n_s - 1| = 1/(2φ³) = 1/(2 × 4.236) = 0.118 (too large)
90 4. |n_s - 1| = 1/(8φ³) = 0.030 (close!)
91 5. |n_s - 1| = 1/(φ⁸) = 1/46.98 = 0.021 (too small)
92
93 Best fit: |n_s - 1| ≈ 1/(8φ³) ≈ 0.030 (vs observed 0.035) -/