vacuumLedger
plain-language theorem explainer
The vacuum ledger supplies the zero-density baseline for the RRF gravity model. Researchers deriving curvature from ledger strain cite it to fix the flat-space reference. The definition constructs the spatial ledger by direct assignment of zero density and charge, with reflexivity supplying the non-negativity witness.
Claim. The vacuum ledger is the spatial ledger $L$ with density $L.ρ = 0$, charge $L.q = 0$, satisfying $0 ≤ L.ρ$ and $L.q = 0$.
background
In the RRF module, gravity is the geometric manifestation of ledger constraint density, with mass identified as transaction density per volume. The spatial ledger structure records a local point with real-valued density, a non-negativity witness, integer charge, and a balance condition that charge equals zero. Upstream, le_refl establishes reflexivity of the order on LogicNat, while the balanced predicate requires the event list of a ledger to be balanced.
proof idea
The definition is a direct structure construction. It sets density to 0, applies le_refl 0 for density_nonneg, sets charge to 0, and uses rfl for the balanced field.
why it matters
This definition anchors the vacuum case inside GravityLedgerCorrespondence and supplies the zero inputs for vacuum_has_zero_mass and vacuum_has_zero_strain. It completes the baseline step in the ledger-to-curvature mapping before non-vacuum ledgers are introduced. The construction touches the open question of how density gradients on the phi-ladder produce observed gravitational strain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.