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)
151theorem universalCost_smul_single (n : ℕ) (p : P) :
152 universalCost (n • Finsupp.single p 1) = (n : ℝ) * primeJcost p := by
proof body
Term-mode proof.
153 rw [show n • Finsupp.single p (1 : ℕ) = Finsupp.single p n by
154 ext q; by_cases hpq : q = p
155 · subst hpq; simp
156 · simp [Finsupp.single_apply, hpq]]
157 exact universalCost_single p n
158
159/-! ## Universal certificate -/
160
161/-- Master certificate: the elementary properties of the universal
162 cost spectrum. -/
depends on (10)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
primeJcost
in IndisputableMonolith.NumberTheory.UniversalCostSpectrum
decl_use
-
universalCost
in IndisputableMonolith.NumberTheory.UniversalCostSpectrum
decl_use
-
universalCost_single
in IndisputableMonolith.NumberTheory.UniversalCostSpectrum
decl_use