mass_nonneg
plain-language theorem explainer
Mass extracted from any spatial ledger equals its transaction density and is therefore non-negative. Cosmologists populating gauge sectors cite the result when assigning boson masses to SU(2) and SU(3) sectors. The argument is a direct field projection from the ledger structure definition.
Claim. For any spatial ledger $L$ with transaction density $d$, the derived mass $m(L) := d$ satisfies $m(L) ≥ 0$.
background
In the RRF setting gravity is ledger curvature, with mass defined as local transaction density. A SpatialLedger is a structure carrying a real density field (transactions per unit volume), a non-negativity witness for that density, an integer charge, and a balance constraint forcing charge zero. The auxiliary definition massFromSpatialLedger simply returns the density field, turning the non-negativity witness into a mass statement.
proof idea
The proof is the one-line term L.density_nonneg, which directly supplies the inequality from the structure field of SpatialLedger.
why it matters
The theorem supplies the mass_nonneg field required by GaugeSector in NonAbelianSuppression. It is invoked (via norm_num or le_refl) when constructing the U(1), SU(2), and SU(3) sectors that carry explicit boson masses. Within the Recognition framework it anchors the ledger-to-mass identification that precedes curvature and strain definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.