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 (d : ℕ) : ℕ := d + 2
proof body
Definition body.
45
46/-- The parity count (number of independent ledger parities): `D²`.
47 At `D = 3`, this equals `9`. -/
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_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
-
configDim
in IndisputableMonolith.GameTheory.CoalitionSizeFromConfigDim
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 (10)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
independent
in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics
decl_use
-
configDim
in IndisputableMonolith.Cosmology.CosmicMicrowaveBackgroundFromRS
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
independent
in IndisputableMonolith.Foundation.RSCoupledAxis
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
configDim
in IndisputableMonolith.GameTheory.CoalitionSizeFromConfigDim
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
parity
in IndisputableMonolith.LedgerPostingAdjacency
decl_use