radialPoissonStub
plain-language theorem explainer
This definition supplies a stub instance for radial Poisson facts in the relativity fixtures module. It would be referenced by developers isolating placeholder code from verified theorems to preserve a clean trust boundary. The construction applies two tactic blocks that simplify the spherical Laplacian identity and construct a trivial zero solution for the Poisson equation.
Claim. A noncomputable definition supplying an instance of radial Poisson facts where the spherical Laplacian applied to a test function $f$ at radius $r$ reduces to itself by simplification, and for any source density function and weight there exists a solution given by the zero function satisfying the equation after simplification.
background
The module supplies stub instances for hypothesis classes introduced to replace sorries, with all such fixtures kept outside production namespaces to maintain a clear trust boundary. Radial Poisson facts encode the spherical Laplacian operator together with existence of solutions to the associated Poisson equation, the latter verified against a phi-related term. No upstream lemmas are referenced, consistent with the stub's role among sibling placeholders for gauge, curvature, and field-theory facts.
proof idea
The definition is assembled from two by-tactic blocks. The first block introduces the function and radius arguments then applies simp to obtain the Laplacian identity. The second block introduces the source density and weight, then uses exact to supply the constant zero function paired with a simp tactic that discharges the verification condition.
why it matters
The stub supports the module's explicit goal of replacing sorries with named instances while isolating them from production code. It participates in the scaffolding for relativity modeling that includes parallel stubs for modified Poisson and linearized PDE facts. No direct link to the T0-T8 forcing chain or Recognition Composition Law is present, leaving open the question of replacing this placeholder with a verified solution existence theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.