theorem proved term proof

`inflation_cert`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 119theorem inflation_cert : InflationCert where
 120  alpha_derived := alpha_attractor_eq_phi_plus_one

proof body

Term-mode proof.

 121  alpha_positive := alpha_attractor_pos
 122  spectral_ok := n_s_at_55
 123  modulation_positive := Omega_0_pos
 124  curvature_bounded := curvature_bounded_at_R0
 125
 126end
 127
 128end RSInflation
 129end Gravity
 130end IndisputableMonolith

depends on (8)

Lean names referenced from this declaration's body.

alpha_attractor_eq_phi_plus_one in IndisputableMonolith.Gravity.Inflation decl_use
alpha_attractor_pos in IndisputableMonolith.Gravity.Inflation decl_use
curvature_bounded_at_R0 in IndisputableMonolith.Gravity.Inflation decl_use
InflationCert in IndisputableMonolith.Gravity.Inflation decl_use
n_s_at_55 in IndisputableMonolith.Gravity.Inflation decl_use
Omega_0_pos in IndisputableMonolith.Gravity.Inflation decl_use
n_s_at_55 in IndisputableMonolith.Gravity.RSBaryogenesis decl_use
alpha_positive in IndisputableMonolith.Unification.ConstantsPredictionsProved decl_use