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)
105noncomputable def vacuumJCost : ℝ := Jcost phi
proof body
Definition body.
106
107/-! ## J-Cost Cancellation Mechanism -/
108
109/-- Key insight: In RS, the cosmological constant arises from
110 the DIFFERENCE between positive and negative J-cost contributions.
111
112 1. Positive contributions: Each field mode adds ~E_P
113 2. Negative contributions: φ-structure provides cancellation
114 3. Residual: The tiny observed Λ
115
116 Λ_eff = Λ_bare - Λ_φ-cancel + Λ_residual
117
118 The residual is ~10⁻¹²² of the bare value! -/
depends on (16)
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
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
Cost
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
-
value
in IndisputableMonolith.QFT.SpinStatistics
decl_use
-
constant
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use