LocalStrain
plain-language theorem explainer
LocalStrain defines a non-negative real number J as the local tightness of ledger constraints at a point. Physicists deriving gravity from ledger density in the Recognition framework cite this when mapping mass to geometric strain. The declaration is a direct structure with a field for J and an attached non-negativity proof.
Claim. A local strain is a pair consisting of a real number $J$ and a proof that $0 ≤ J$.
background
The RRF module treats gravity as the geometric manifestation of ledger constraint density. Mass equals the number of transactions per volume while curvature equals the resulting constraint pressure. LocalStrain supplies the pointwise object that carries this pressure as a non-negative real.
proof idea
The declaration is a structure definition that introduces the type with two fields: the strain value J and the non-negativity witness J_nonneg. No lemmas or tactics are invoked.
why it matters
LocalStrain supplies the basic datum for the gravity-ledger correspondence. It is used in curvatureFromStrain to set scalar curvature equal to kappa times J and in gravity_is_ledger_curvature to prove monotonicity of curvature with strain. The definition thereby realizes the module claim that gravity is collective ledger strain rather than a force, feeding directly into GravityLedgerCorrespondence and LedgerDeadlock.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.