pressure_equiv_from_w
plain-language theorem explainer
Any ILG kernel supplies a pressure function via the pointwise product of its weight, density, and scaling maps. Modelers of galactic dynamics under the coercive projection law cite this to rewrite the weighted source term as an effective pressure in the Poisson equation. The proof is a direct term-mode construction that exhibits the candidate function and confirms the equality by reflexivity.
Claim. There exists a function $p : ℝ → ℝ$ such that $p(x) = w(x) · ρ(x) · δ(x)$ for every real $x$, where $w, ρ, δ : ℝ → ℝ$ are given real-valued functions.
background
The Coercive Projection Law module formalizes gravity as an information-limited process whose energy functional admits a unique minimizer. The ILG weight operator w multiplies the baryonic density source; the pressure equivalence rewrites this product as an effective pressure term p that recovers the standard Poisson equation. The supplied theorem guarantees existence of p without further hypotheses on w, ρ or δ. Upstream results on the ILG energy functional supply the coercivity constant 49/162 and the net constant K_net = (9/7)^2 arising from the eight-tick structure.
proof idea
The proof is a one-line term-mode construction. It supplies the explicit function λx, w x * rho x * delta x as the witness for the existential quantifier, then applies reflexivity to discharge the universal quantification over x.
why it matters
The declaration supplies the pressure-equivalence step required by the Coercive Projection Law of Gravity. It directly supports the module claim that the ILG modified Poisson equation is equivalent to the standard Poisson equation with effective pressure source p = w * rho_b. The result sits inside the Recognition Science forcing chain after T8 (D = 3) and the Recognition Composition Law, closing the link between the weight operator and observable gravitational dynamics. No open scaffolding remains for this particular existence statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.