residualOverHalf_eq_one
plain-language theorem explainer
At equal census (4,2,0), the residual of the uniform π-weighted class-mass ratio over the directed Aut prediction 1/2 is exactly 1. Anyone citing the Poisson coarea ratio test or the silent residual family uses this identity. The proof is a one-line algebraic reduction from the already-proved fibre ratio equaling 1/2.
Claim. The residual of the uniform class-mass ratio at equal census $(4,2,0)$ relative to the directed prediction $1/2$ equals $1$. Writing $R$ for the $\pi$-weighted class-mass ratio of the two Aut-distinct complexes (fibres 24 and 48), one has $R/(1/2)=1$.
background
Gap 2 / A20 studies a LIFO Poissonized post/unpost process on tet-free bounded complexes. Legal moves have unit rate; the rate matrix is symmetric, so the unique stationary law on each finite cap is uniform. Flag 8 is unmoved and FullTheoryLedger is not imported.
At equal census $(4,2,0)$ the two Aut-distinct witnesses twoEdgeComplex and pathPlusIsolated have fibre cardinalities 24 and 48. Under uniform $\pi$ their class-mass ratio is therefore exactly $1/2$ (directed Aut correction). The residual is defined as that ratio divided by the directed prediction $1/2$; the upstream theorem already records the ratio as the rational $1/2$.
Process symbols name neither Aut nor orbit nor stabilizer; those words appear only in conclusions and the pre-registered ratio comparison.
proof idea
One-line term-mode reduction. Unfold the residual definition (class-mass ratio over $1/2$), substitute the upstream equality that the $(4,2,0)$ class-mass ratio equals $1/2$, then finish by norm_num on the rational arithmetic $(1/2)/(1/2)=1$.
why it matters
Closes the residual side of the Poisson coarea ratio test under the uniformity premise. Downstream, residual_family_silent packages this identity with the class-mass ratio equaling $1/2$, equal vertex counts, and $\Delta\mathrm{SJ}=2$, showing that C6 and the C27 $q^{\mathrm{SJ}}$ trigger stay silent on the unit-rate process: the SJ-tilted decoy responds as $\mathrm{ratio}(q)=\mathrm{fibre_ratio}\cdot q^{\Delta\mathrm{SJ}}$, so the $q=1$ measurement excludes a nonunit tilt at these witnesses. Also feeds the index flag that C4+C16 does not claim C23 fully satisfied. Sits inside lane C16 of the seven-gap gravity ledger; no claim beyond the named witnesses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.