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)
106def faceVertexCount (D : ℕ) : ℕ := 2^(D - 1)
proof body
Definition body.
107
108/-- In D=3, each face is a 2D square with 4 vertices. -/
used by (10)
From the project-wide theorem graph. These declarations reference this one in their body.
-
D3_has_2D_faces
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
-
delta_derived_not_calibrated
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
-
deltaStructural
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
-
deltaStructural_alt_D3
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
-
deltaStructural_D3
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
-
discrete_continuous_duality
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
-
discreteMeasure2DFace
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
-
faceVertexCount_D3
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
-
muTauContribution_eq
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
-
vertices_are_anchors
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
depends on (4)
Lean names referenced from this declaration's body.
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use