LocalStrain
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not compute numerical J from explicit transaction counts.
- Does not evolve strain under time-dependent ledger updates.
- Does not tie J to the phi-ladder or specific mass rungs.
- Does not incorporate quantum or higher-dimensional corrections.
formal statement (Lean)
66structure LocalStrain where
67 /-- Strain value. -/
68 J : ℝ
69 /-- Strain is non-negative. -/
70 J_nonneg : 0 ≤ J
71
72/-- Strain from ledger density. -/