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)
107structure WeakFieldBridge where
108 potential : (Fin 4 → ℝ) → ℝ
109 density : (Fin 4 → ℝ) → ℝ
110 poisson : ∀ x, laplacian potential x = (1/2 : ℝ) * 8 * phi ^ 5 * density x
111
112/-! ## §4 Coupling Constant Chain -/
113
114/-- The Einstein coupling κ = 8πG/c⁴ = 8φ⁵ in RS-native units.
115 This is derived in `Constants.lean` and `ZeroParameterGravity.lean`. -/
depends on (16)
Lean names referenced from this declaration's body.
-
Chain
in IndisputableMonolith.Chain
decl_use
-
G
in IndisputableMonolith.Constants
decl_use
-
G
in IndisputableMonolith.Constants.Codata
decl_use
-
G
in IndisputableMonolith.Cost.FunctionalEquation
decl_use
-
Constants
in IndisputableMonolith.CPM.LawOfExistence
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
G
in IndisputableMonolith.Gravity.JCostInflaton
decl_use
-
Coupling
in IndisputableMonolith.Information.FEPBridgeFromJCost
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
-
density
in IndisputableMonolith.Physics.NeutronStarCrustalRegimesFromRS
decl_use
-
Chain
in IndisputableMonolith.Recognition
decl_use
-
laplacian
in IndisputableMonolith.Relativity.Calculus.Derivatives
decl_use
-
Chain
in IndisputableMonolith.RRF.Core.Recognition
decl_use