strainFromLedger
plain-language theorem explainer
This definition maps the density component of a SpatialLedger directly to the strain value J of the corresponding LocalStrain. Researchers modeling gravity as ledger curvature in the Recognition framework cite it to identify local mass with transaction density. The construction is a direct field assignment that reuses the non-negativity proof already present in the ledger.
Claim. Let $L$ be a spatial ledger with non-negative density $d$. The local strain associated to $L$ is the structure whose strain component equals $d$ and whose non-negativity certificate is inherited from $L$.
background
A SpatialLedger is a local record consisting of a real-valued transaction density $d$ together with the constraint that the net charge at that point is zero. LocalStrain is the structure whose single real component $J$ quantifies the tightness of constraints at the same point. The module states that gravity is the geometric manifestation of ledger constraint density, with mass identified with ledger density and curvature identified with the resulting strain pressure.
proof idea
The definition constructs a LocalStrain instance by setting its J field to the density field of the input SpatialLedger and copying the supplied non-negativity proof.
why it matters
This definition supplies the explicit map required by GravityLedgerCorrespondence to equate curvature with strain and by gravity_ledger_consistent to verify internal consistency. It realizes the module claim that gravity is the collective strain of particles balancing their ledgers simultaneously, closing the link between the ledger formalism and the geometric description of gravity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.