augPath
plain-language theorem explainer
Encodes the augmented two-edge-path seed row as the rational 4-tuple (3, 2, 0, 2), standing for the linear relation 3 C_V + 2 C_E = 2. Cited by the C15 rank test that shows the three augmented seed rows are linearly independent over Q. Pure data definition: no proof content.
Claim. The augmented seed row for the two-edge path (direct order) is the rational 4-tuple $(3,2,0,2)$, encoding the affine relation $3 C_V + 2 C_E = 2$ with a zero coefficient on the unused third left-hand direction.
background
Gap 2 / C15 studies the J-diamond rank lattice after the census-inversion route was ruled out. A J-diamond is a pair of proper subcomplexes of a posting graph whose union is the whole complex; the diamond defect is the four-term inclusion-exclusion failure $D(A,B;I)=SJ(A)+SJ(B)-SJ(I)-SJ(K)$ of the integer squared-imbalance total $SJ=2\kappa J$. The localization theorem factors that defect through interface imbalance products.
To test whether per-kind rates can still be recovered from diamond data, the module builds a small linear system of seed rows. Each augmented row packages left-hand coefficients on the cost unknowns together with a right-hand side. The path row is the contribution of the two-edge path configuration in direct evaluation order.
proof idea
Definitional constant: the 4-tuple is written out literally as (3, 2, 0, 2). No lemmas, tactics, or computation. Downstream independence proofs project componentwise and simplify against this literal value.
why it matters
Feeds seed_augmented_independent, which proves that the three augmented seed rows (point, edge, path) are linearly independent over $\mathbb{Q}$, so the right-hand sides carry one extra degree of freedom beyond the three left-hand directions. That rank fact is packaged into JDiamondRankVerdict, the C15 lattice verdict collecting localization, evenness, kernel diamonds, count conflict, and seed-row inconsistency. A hostile-probe mirror (probe_aug_independent) reuses the same constant. Within the Seven Gaps gravity program this is the concrete path datum that makes the augmented system overshoot left-hand rank by one, blocking a consistent recovery of the three per-kind rates from J-diamond data alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.