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)
115theorem vertex_deficit_eq : vertex_angular_deficit = Real.pi / 2 := by
proof body
Term-mode proof.
116 unfold vertex_angular_deficit faces_per_vertex cube_dihedral; ring
117
118/-- **Discrete Gauss-Bonnet on Q₃**: total curvature of ∂Q₃
119 (sum of vertex deficits over all 8 vertices) equals 4π.
120
121 8 × (π/2) = 4π = 2π · χ(S²). -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (16)
Lean names referenced from this declaration's body.
-
all
in IndisputableMonolith.Aesthetics.NarrativeGeodesic
decl_use
-
all
in IndisputableMonolith.Anthropology.KinshipGraphCohomology
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
cube_dihedral
in IndisputableMonolith.Constants.AlphaDerivation
decl_use
-
faces_per_vertex
in IndisputableMonolith.Constants.AlphaDerivation
decl_use
-
vertex_angular_deficit
in IndisputableMonolith.Constants.AlphaDerivation
decl_use
-
all
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
cube_dihedral
in IndisputableMonolith.Geometry.DihedralAngle
decl_use
-
cube_dihedral
in IndisputableMonolith.Gravity.DiscreteCurvature
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
all
in IndisputableMonolith.Musicology.ModalPreferenceFromPhi
decl_use
-
total
in IndisputableMonolith.NavierStokes.DiscreteVorticity
decl_use
-
total
in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget
decl_use