measuredCap3_pi
plain-language theorem explainer
The cap-3 measured tally records a uniform stationary law with numerator 1 and denominator 910. Anyone citing the Gap-2 Poisson coarea receipt (lane C16) uses this as the exact rational π for the 910-state tet-free LIFO chain. The proof is pure definitional equality: both components are the fields written into the measuredCap3 record.
Claim. For the measured cap-3 tet-free tally, the stationary distribution is the exact rational $\pi = 1/910$: its numerator equals $1$ and its denominator equals $910$.
background
Gap 2 / A20 studies a raw LIFO Poissonized post/unpost process on serially named tet-free bounded complexes. Every legal move (append vertex, unpost max unused vertex, append edge, unpost max edge) has rate 1. The module headline is that symmetric legal rates force a uniform stationary law on each finite cap; Flag 8 is left unmoved and FullTheoryLedger is not imported.
The upstream definition measuredCap3 is the MEASURED mirror of the cap-3 receipt: 910 named states, all reachable from empty, off-diagonal rate matrix symmetric, chain irreducible, and stationary numerator fixed at 1. The module doc states the unique stochastic stationary law is uniform $1/910$ (exact rational solve; B=0/1/2 by Gaussian elimination, B=3 by exact solve).
Process symbols deliberately avoid Aut, orbit, stabilizer, and gibbsWeight; those appear only in conclusions and the pre-registered ratio comparison.
proof idea
One-line wrapper by reflexivity. The conjunction is proved as $\langle \mathrm{rfl}, \mathrm{rfl} \rangle$: both equalities hold definitionally because the measured cap-3 record sets stationaryPiNum := 1 and (by the Cap3Tally layout and the stated 910-state census) stationaryPiDen := 910. No tactic search or external lemma is required.
why it matters
This pins the exact rational stationary mass used as premise c16_cap3_uniform_measured inside measureDerivationPremises_inhabited, which asserts every measure-derivation premise field is inhabited by a cited theorem (or the named cap-4 uniformity premise tagged DERIVED-UNFORMALIZED).
In the Recognition Gravity SevenGaps chain it is the measured half of lane C16: rate symmetry plus irreducibility yield uniform $\pi$ on the 910-state cap-3 slice. Cap-4 uniformity (host of the equal-census $(4,2,0)$ witnesses whose class-mass ratio is $1/2$) remains DERIVED-UNFORMALIZED by the same argument, not a separate solve. The factorial $nV!,nE!,nT!$ emerges as the cardinality of sort-respecting arrival orders, not a hypothesis. No claim is made beyond the measured witnesses and the pre-registered ratio test under the uniformity premise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.