poissonCoareaIndex
plain-language theorem explainer
Boolean status ledger for Gap 2 (A20/C16) Poisson recognition coarea: which process, stationarity, ratio, residual, and coarea clauses are asserted, and which flags stay false. Gravity auditors and FullTheoryLedger consumers cite it as the single claim surface for this lane. The body is a pure structure instance with seven hard-coded Booleans.
Claim. The Poisson coarea status index records: process firewall on (LIFO serial names only), cap-3 stationary uniformity on, equal-census $(4,2,0)$ class-mass ratio exactly $1/2$ on, residual family silent on, scoped coarea at the witnesses on; measure flag unmoved (false); and C23 not fully satisfied (false).
background
Gap 2 / A20 studies a raw LIFO Poissonized post/unpost process on serially named tet-free bounded complexes. Legal moves (append vertex, unpost unused max vertex, append edge, unpost max edge) each have rate 1. Cap-3 has 910 named states; symmetric off-diagonal rates plus irreducibility from empty force the unique stationary law to be uniform $1/910$. Cap-4 uniformity (host of the $(4,2,0)$ witnesses) is derived from the same rate-symmetry argument, not a separate solve.
At equal census $(4,2,0)$, the $\pi$-weighted class-mass ratio of two Aut-distinct complexes (twoEdgeComplex vs pathPlusIsolated) is exactly $1/2$ under uniform $\pi$ (fibres 24 and 48). The factorial $nV!,nE!,nT!$ is the cardinality of sort-respecting arrival orders; fibre size equals that count divided by directed Aut order (orbit-stabilizer on the conclusion side only). C35 firewall: process symbols name neither Aut, orbit, canonicalization, nor Gibbs weight.
PoissonCoareaIndex is the structure packing seven Boolean claim flags for this scoped coarea story. Flag 8 (measure moved) stays false; FullTheoryLedger is not imported.
proof idea
Definitional structure instance, not a proof. Each field of PoissonCoareaIndex is assigned a literal true or false matching the module's measured/theorem surface: firewall, cap-3 uniformity, ratio-half, residual silence, and coarea witnesses asserted; measure-flag-moved and c23-fully-satisfied left false. Downstream index_* lemmas are one-line rfl readers of these fields.
why it matters
Single machine-checkable claim surface for the A20/C16 Poisson coarea lane inside Gravity.SevenGaps. Downstream parents are the seven index_* audit theorems (index_firewall, index_cap3, index_ratio, index_coarea, index_residual, index_flag_unmoved, index_c23_not_claimed), each a reflexivity check that the ledger matches the intended status.
The module headline is exact: symmetric legal rates imply uniform stationary law on each finite cap; at $(4,2,0)$ the directed-Aut-corrected class-mass ratio is $1/2$; factorial arrival counts are cardinalities, not hypotheses; flag 8 is not moved. This index freezes that headline so later ledger composition cannot silently upgrade C23 or move the measure flag. It does not itself touch T0–T8 or the RCL; it is gravity-side scaffolding for recognition coarea at named witnesses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.