lemma
proved
term proof
phi_pow_residue_mu_bounds
No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
186lemma phi_pow_residue_mu_bounds :
187 (0.0097 : ℝ) < phi ^ predicted_residue_mu ∧ phi ^ predicted_residue_mu < (0.0098 : ℝ) :=
proof body
Term-mode proof.
188 ⟨phi_pow_residue_mu_lower, phi_pow_residue_mu_upper⟩
189
190/-! CORRECTED: φ^(predicted_residue_tau) where residue_tau ∈ (-3.77, -3.75)
191Previous claim of 0.346 < φ^residue < 0.348 was FALSE!
192Actual: φ^(-3.76) ≈ 0.164
193Correct bounds: φ^(-3.77) ≈ 0.163, φ^(-3.75) ≈ 0.165 -/
194
195/-- φ^(-3.77) > 0.163 (numeric). -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (15)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
was
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
predicted_residue_mu
in IndisputableMonolith.Physics.LeptonGenerations.Defs
decl_use
-
predicted_residue_tau
in IndisputableMonolith.Physics.LeptonGenerations.Defs
decl_use
-
phi_pow_residue_mu_bounds
in IndisputableMonolith.Physics.LeptonGenerations.Necessity
decl_use
-
phi_pow_residue_mu_lower
in IndisputableMonolith.Physics.LeptonGenerations.Necessity
decl_use
-
phi_pow_residue_mu_upper
in IndisputableMonolith.Physics.LeptonGenerations.Necessity
decl_use
-
predicted_residue_mu
in IndisputableMonolith.RRF.Physics.LeptonGenerations.Defs
decl_use
-
predicted_residue_tau
in IndisputableMonolith.RRF.Physics.LeptonGenerations.Defs
decl_use
-
phi_pow_residue_mu_lower
in IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity
decl_use
-
phi_pow_residue_mu_upper
in IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity
decl_use