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)
130private theorem constant_config_total_defect {N : ℕ} (μ : ℝ) :
131 total_defect (constant_config μ : Configuration N) = (N : ℝ) * Jlog μ := by
proof body
Term-mode proof.
132 unfold total_defect constant_config
133 simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
134 rfl
135
136/-- Weighted average of the logs equals `log_charge / N`. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (13)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
Jlog
in IndisputableMonolith.Cost
decl_use
-
Jlog
in IndisputableMonolith.Cost.FlogEL
decl_use
-
Jlog
in IndisputableMonolith.Cost.Jlog
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
Configuration
in IndisputableMonolith.Foundation.InitialCondition
decl_use
-
total_defect
in IndisputableMonolith.Foundation.InitialCondition
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
Configuration
in IndisputableMonolith.Foundation.RecognitionForcing
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
constant_config
in IndisputableMonolith.Foundation.VariationalDynamics
decl_use
-
log_charge
in IndisputableMonolith.Foundation.VariationalDynamics
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use