LedgerDeadlock
plain-language theorem explainer
LedgerDeadlock encodes a region whose local strain J diverges without bound, forcing a wait state that the framework reads as time dilation. Gravity modelers in Recognition Science cite it when treating constraint singularities as ledger closure failures. The declaration is a bare structure with three fields and no computational content.
Claim. A region $R$ is a ledger deadlock when its strain diverges: for every real bound $B$ there exists a local strain $S$ with $J(S) > B$, and the only admissible move is to wait.
background
The RRF module treats gravity as the geometric expression of ledger constraint density, with mass identified as transaction density per volume and curvature as the resulting pressure. LocalStrain is the sibling structure that records the tightness of constraints at a point via a non-negative real $J$ satisfying $0 ≤ J$. The supplied module doc states that gravity is not a force but the collective strain of particles balancing ledgers simultaneously.
proof idea
The declaration is a structure definition whose three fields are introduced directly; no lemmas are applied and no tactics are executed.
why it matters
The structure supplies the formal object for strain divergence inside the ledger-curvature account of gravity. It sits downstream of LocalStrain and upstream of any future treatment of horizons or singularities, consistent with the module's claim that curvature equals constraint pressure. No used-by edges exist yet, leaving open how the divergence condition will be discharged by concrete ledger rules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.