SJ_pathPlus
plain-language theorem explainer
Names the integer SJ score of the path-plus-isolated witness complex as the constant 2. Downstream ratio instruments subtract this from the two-edge score to obtain ΔSJ = 2, so the predicted q-tilt is (1/2) q^2. Citation target for anyone checking the (4,2,0) class-mass decoy or residual_family_silent. The body is a bare natural-number literal.
Claim. The SJ score attached to the path-plus-isolated complex at census $(4,2,0)$ is the natural number $2$.
background
Gap 2 (lane C16) studies a LIFO Poissonized post/unpost process on tet-free bounded complexes. Legal moves (append vertex, unpost max unused vertex, append edge, unpost max edge) each have rate 1. On each finite cap the off-diagonal rate matrix is symmetric, so the unique stationary law is uniform on named states.
At equal census $(4,2,0)$ two Aut-distinct witnesses appear: the two-edge complex and the path-plus-isolated complex. Their named fibres have sizes 24 and 48, so the uniform class-mass ratio is exactly $1/2$. An optional decoy reweights states by $q^{\mathrm{SJ}}$; the instrument then responds $\mathrm{ratio}(q)=\frac12 q^{\Delta\mathrm{SJ}}$.
This definition simply records the integer SJ value of the path-plus-isolated witness. The companion constant for the two-edge witness and the difference $\Delta\mathrm{SJ}=2$ are used only on the conclusion side of the ratio test; process symbols never mention Aut, orbit, or gauge class (C35 firewall).
proof idea
Bare definition: the natural-number literal 2 is assigned to the constant. No proof obligations, no lemmas, no tactics. The companion reflexivity theorem SJ_pathPlus_rfl is the one-line rfl wrapper that exposes the equality for simp.
why it matters
Feeds every predicted-ratio and residual statement in the module. predictedRatio_qSJ is defined as $\frac12 q^{\mathrm{SJ}{\mathrm{twoEdge}}-\mathrm{SJ}{\mathrm{pathPlus}}}$; the two evaluation theorems at $q=1$ and $q=2$ unfold this constant by simp. residual_family_silent packages the conjunction that the uniform class-mass ratio equals $1/2$ together with $\mathrm{SJ}{\mathrm{twoEdge}}-\mathrm{SJ}{\mathrm{pathPlus}}=2$, thereby showing that the unit-rate process keeps the C6/C27 $q^{\mathrm{SJ}}$ trigger silent at these witnesses.
Inside the Seven Gaps gravity ledger this is the numeric anchor that converts the measured fibre ratio into an exact rational decoy response, confirming that no non-unit SJ tilt is present once stationarity is uniform. Flag 8 and the full theory ledger remain untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.