InsideSchwarzschild
plain-language theorem explainer
InsideSchwarzschild defines the region inside the event horizon for mass M at coordinate r, with ledger constraint density flagged as extreme. Researchers deriving black-hole interiors or horizon crossings in the Recognition Science ledger model of gravity would reference this structure. It is realized as a direct structure definition that encodes the strict radial inequality against the Schwarzschild radius together with a trivial density proposition.
Claim. For mass $M$ and radial coordinate $r$, the structure holds when $r < r_s(M)$ where $r_s(M) = 2GM$ in RS-native units, and the ledger constraint density is extreme.
background
The module treats gravity as the geometric manifestation of ledger constraint density, identifying mass with the number of transactions per volume and curvature with the resulting pressure. Gravity is therefore the collective strain that arises when particles balance their ledgers simultaneously. Upstream, schwarzschildRadius supplies the horizon scale $r_s = 2GM$ for a black hole of mass $M$.
proof idea
This is a structure definition with no computational content. It directly packages the inequality $r <$ schwarzschildRadius $M$ and sets the extreme_density field to the trivial proposition True.
why it matters
The structure marks the interior domain in which ledger constraints become maximal, supporting the gravity-ledger correspondence developed in the same module. It aligns with the Recognition Science identification of curvature as constraint pressure and is consistent with the forcing-chain derivation of three spatial dimensions. No downstream uses are recorded in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.