WeakFieldBridge
plain-language theorem explainer
The WeakFieldBridge structure packages the weak-field limit of linearized gravity in RS units, with a potential and density satisfying the Poisson equation whose source term carries the coupling 4 φ^5. Researchers deriving Newtonian gravity from lattice J-cost or checking the discrete-to-continuum map would cite it when moving from curvature to mass density. The declaration is a direct structure definition that records the relation without invoking further lemmas.
Claim. A structure consisting of functions Φ, ρ : (Fin 4 → ℝ) → ℝ such that ∇²Φ(x) = 4 φ^5 ρ(x) for all x, where the factor 4 φ^5 is the RS-native value of κ/2 with κ = 8 φ^5.
background
The module builds the discrete-to-continuum bridge from J-cost lattice through quadratic defect and lattice Laplacian to the continuum Einstein equations. Tier 1 results already establish the flat limit, spatial metric from J-cost, Laplacian convergence, and the coupling κ = 8 φ^5 with D = 3. The WeakFieldBridge records the linearized reduction g_μν = η_μν + h_μν (|h| ≪ 1) to the Poisson equation ∇²Φ = (κ/2) ρ with Φ = -h_{00}/2.
proof idea
Structure definition that directly encodes the Poisson relation with the RS coupling factor 4 φ^5; no lemmas or tactics are applied.
why it matters
It supplies the explicit weak-field bridge from curvature to Newtonian gravity, filling the Tier 1 step listed in the module doc-comment. The factor 4 φ^5 traces to the forcing chain T5–T8 and the derived coupling κ = 8 φ^5. No downstream theorems yet reference it, but it supports the larger DiscreteContinuumBridge certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.