EnergyDistribution
plain-language theorem explainer
EnergyDistribution structures a non-negative density function on positions as the J-cost density that sources the processing field. Workers on the energy-processing-gravity bridge cite it to encode the T^{00} = J-cost density identity from EFE emergence. The declaration is a direct structure definition with a non-negativity field and no computational reduction.
Claim. An energy distribution consists of a map $ρ : Position → ℝ$ together with a proof that $ρ(h) ≥ 0$ for every position $h$, where $ρ$ is the J-cost density sourcing the processing potential.
background
In the EnergyProcessingBridge module the structure packages the density that links energy to processing fields. J-cost is the cost induced by a multiplicative recognizer (derivedCost of its comparator) and equals the cost of any recognition event. The constant G is the RS-native form $λ_{rec}^2 c^3 / (π ħ)$. Upstream the CPM2D.model builds a Model from a Hypothesis bundle that supplies defectMass, orthoMass and energyGap for fluid-like systems.
proof idea
The declaration is a structure definition that directly introduces the type with fields density and density_nonneg. No lemmas or tactics are invoked.
why it matters
The definition supplies the type for energy_creates_processing_gradient and energy_distribution_creates_gravity_modifier, which establish that energy gradients produce opposing processing gradients. It formalizes the T^{00} = J-cost density identity from EFE emergence, connecting the J-uniqueness step (T5) to gravitational modification in the forcing chain. It closes scaffolding between classical fluid models and the processing-field bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.