gravity_ledger_consistent
plain-language theorem explainer
The definition supplies an explicit instance of the gravity-ledger correspondence by equating mass to spatial ledger density, setting curvature proportional to local strain J, and confirming zero curvature for the vacuum ledger. Researchers modeling gravity via ledger constraint density cite it to verify that the proposed mapping satisfies its internal consistency requirements. Construction proceeds by direct field assignment for the mass and curvature properties together with a single simplification step on the vacuum case.
Claim. The structure is realized by the assignments $mass(L) = density(L)$ for every spatial ledger $L$, $R(curvatureFromStrain(S, κ)) = κ · J(S)$ for every local strain $S$ and $κ > 0$, and $R(curvatureFromStrain(strainFromLedger(vacuumLedger), 1)) = 0$.
background
In the RRF module gravity is defined as the geometric manifestation of ledger constraint density, with mass identified as the number of transactions per volume and curvature identified as the resulting constraint pressure. The referenced structure GravityLedgerCorrespondence encodes exactly three properties: mass-density equality, curvature-strain proportionality via the linear map curvatureFromStrain, and vacuum flatness. Upstream definitions supply curvatureFromStrain (which sets scalar curvature R := κ · S.J) and strainFromLedger (which extracts the strain field from a given ledger); vacuumLedger is the zero-density reference ledger.
proof idea
The definition populates the three fields of GravityLedgerCorrespondence by reflexivity for mass_is_density and curvature_is_strain. The remaining vacuum_is_flat field is discharged by a single simp tactic that unfolds curvatureFromStrain, strainFromLedger, and vacuumLedger to obtain the required zero equality.
why it matters
This definition supplies the concrete witness used by the downstream theorem gravity_interpretation_valid, which asserts Nonempty GravityLedgerCorrespondence. It thereby closes the internal-consistency step for the module claim that gravity is ledger curvature rather than an independent force. The construction directly supports the RRF mapping of mass to density and curvature to strain without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.