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)
44def configDim : ℕ := 3
proof body
Definition body.
45
46/-- Total coalition types: 2^D - 1. -/
used by (23)
From the project-wide theorem graph. These declarations reference this one in their body.
-
etaB_pos
in IndisputableMonolith.Cosmology.BaryogenesisTrajectoryFromPhiLadder
decl_use
-
CMBCert
in IndisputableMonolith.Cosmology.CosmicMicrowaveBackgroundFromRS
decl_use
-
configDim
in IndisputableMonolith.Cosmology.CosmicMicrowaveBackgroundFromRS
decl_use
-
firstPeak
in IndisputableMonolith.Cosmology.CosmicMicrowaveBackgroundFromRS
decl_use
-
D1_counterfactual_rung
in IndisputableMonolith.Cosmology.EtaBExactRungDerivation
decl_use
-
D2_counterfactual_rung
in IndisputableMonolith.Cosmology.EtaBExactRungDerivation
decl_use
-
D5_counterfactual_rung
in IndisputableMonolith.Cosmology.EtaBExactRungDerivation
decl_use
-
twelve_is_D_4
in IndisputableMonolith.CrossDomain.CardinalitySpectrum
decl_use
-
cube_sq_plus_cube
in IndisputableMonolith.CrossDomain.CrossPatternMatrix
decl_use
-
G5
in IndisputableMonolith.CrossDomain.RecognitionGenerators
decl_use
-
guildCount
in IndisputableMonolith.Ecology.BiodiversityIndexFromConfigDim
decl_use
-
configDim
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
configDim_at_D3
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
integrationGap
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
IntegrationGapCert
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
amplitude_pos_off_threshold
in IndisputableMonolith.Foundation.QRFT.GaugeTreeAmplitudesCert
decl_use
-
mwcSize
in IndisputableMonolith.GameTheory.CoalitionSizeFromConfigDim
decl_use
-
mwcSize_eq
in IndisputableMonolith.GameTheory.CoalitionSizeFromConfigDim
decl_use
-
totalCoalitionTypes
in IndisputableMonolith.GameTheory.CoalitionSizeFromConfigDim
decl_use
-
totalCoalitionTypes_eq
in IndisputableMonolith.GameTheory.CoalitionSizeFromConfigDim
decl_use
-
surfaceEnergyFactor_pos
in IndisputableMonolith.Materials.FractureMechanicsFromJCost
decl_use
-
religiousExperienceCount
in IndisputableMonolith.Philosophy.ReligiousExperienceFromJCost
decl_use
-
quantumFieldTypeCount
in IndisputableMonolith.Physics.QuantumFieldOperatorsFromRS
decl_use
depends on (2)
Lean names referenced from this declaration's body.
-
configDim
in IndisputableMonolith.Cosmology.CosmicMicrowaveBackgroundFromRS
decl_use
-
configDim
in IndisputableMonolith.Foundation.IntegrationGap
decl_use