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)
103def faceCount (D : ℕ) : ℕ := 2 * D
proof body
Definition body.
104
105/-- Vertex count of a (D-1)-hypercube (the face of a D-cube). -/
used by (9)
From the project-wide theorem graph. These declarations reference this one in their body.
-
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
-
faceCount_D3
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
-
faceVertexRatio_D3
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
-
muTauContribution
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
-
muTauContribution_eq
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
depends on (5)
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