PressureEquivalence
plain-language theorem explainer
The PressureEquivalence structure assembles the ILG weight map, baryon density, density contrast, and effective pressure together with their pointwise product identity. Cosmologists comparing information-limited gravity to Newtonian limits would cite it to record that the modified Poisson equation differs from the standard form only on the source side. The declaration is a direct bundling of the four functions with the algebraic relation that equates effective pressure to the weighted product.
Claim. A structure consisting of maps $w : ℝ → ℝ$, $ρ_b : ℝ → ℝ$, $δ_b : ℝ → ℝ$, and $p_{eff} : ℝ → ℝ$ satisfying $p_{eff}(x) = w(x) ⋅ ρ_b(x) ⋅ δ_b(x)$ for every real $x$.
background
The Coercive Projection Law module formalizes results from two papers on unique energy minimizers in ILG and on gravity as pressure. The ILG kernel supplies the weight $w(k,a) = 1 + C (a/(k τ₀))^α$ (with a floor at 0.01 to avoid division by zero), while the pressure form is defined as the product ρ ⋅ w ⋅ δ. This structure records that the effective source $p = w ρ_b δ_b$ renders the ILG Poisson equation identical to the standard Newtonian form with pressure density on the right-hand side.
proof idea
This declaration is a structure definition that directly assembles the four component functions and asserts the equivalence identity. No lemmas are applied; the construction is the definition itself.
why it matters
The definition supplies the precise interface for the pressure equivalence result stated in the module documentation: the ILG modified Poisson equation is equivalent to the standard Poisson equation with an effective pressure source. It supports the claim that ILG modifies only the source term rather than the gravitational operator. Within the Recognition Science framework it aligns with the eight-tick octave and the forcing chain by preserving the left-hand side of the field equation while adjusting only the matter source.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.