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)
89theorem Q3_simplex_vertices_eq : Q3_simplex_vertices = 4 := by
proof body
Term-mode proof.
90 unfold Q3_simplex_vertices Q3_degree; omega
91
92/-! ## Spectral Ratios
93
94The ratios of consecutive eigenvalues determine the correction-to-scaling
95structure. The key ratio λ₂/λ₁ = 4/2 = 2 governs the subleading RG eigenvalue.
96-/
97
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
q3Cert
in IndisputableMonolith.Physics.CubeSpectrum
decl_use
depends on (8)
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
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
correction
in IndisputableMonolith.Information.QuantumChannelCapacityFromPhi
decl_use
-
Q3_degree
in IndisputableMonolith.Physics.CubeSpectrum
decl_use
-
Q3_simplex_vertices
in IndisputableMonolith.Physics.CubeSpectrum
decl_use