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)
94theorem comma_small : pythagoreanComma < 1.02 := by
proof body
Tactic-mode proof.
95 simp only [pythagoreanComma]
96 have h1 : (3 / 2 : ℝ) ^ 12 = 531441 / 4096 := by norm_num
97 have h2 : (2 : ℝ) ^ 7 = 128 := by norm_num
98 rw [h1, h2]
99 norm_num
100
101/-! ## Interval Quality Theorems -/
102
103/-- The fifth in 12-TET is within 0.2% of just (less than 2 cents). -/
depends on (14)
Lean names referenced from this declaration's body.
-
pythagoreanComma
in IndisputableMonolith.Aesthetics.MusicalScale
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
fifth
in IndisputableMonolith.MusicTheory.CircleOfFifths
decl_use
-
fifth
in IndisputableMonolith.MusicTheory.HarmonicModes
decl_use
-
Interval
in IndisputableMonolith.Numerics.Interval.Basic
decl_use
-
Interval
in IndisputableMonolith.Recognition.Certification
decl_use