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)
95theorem mode_seven_lt_9 : harmonicFrequency ⟨7, by decide⟩ < 9 := by
proof body
Term-mode proof.
96 rw [mode_seven]
97 have := phi_lt_onePointSixTwo
98 -- 35φ/8 < 35 · 1.62 / 8 = 56.7/8 = 7.0875 < 9
99 linarith
100
101/-- Strict monotonicity of the comb. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (8)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
phi_lt_onePointSixTwo
in IndisputableMonolith.Constants
decl_use
-
harmonicFrequency
in IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum
decl_use
-
mode_seven
in IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use