sameUnordered
plain-language theorem explainer
Boolean test that two ordered pairs of N=5 torus vertices represent the same unordered edge endpoints. Gravity stencil coefficient audits cite it whenever residual terms are grouped by unordered monomials ξ(u)ξ(v). The body is a one-line decidable disjunction of the two orderings.
Claim. For vertices $a,b,u,v$ on the $5\times5\times5$ periodic lattice, $\mathrm{sameUnordered}(a,b,u,v)$ is true precisely when $\{a,b\}=\{u,v\}$ as sets, i.e. either $(a,b)=(u,v)$ or $(a,b)=(v,u)$.
background
The module certifies the corrected Freudenthal axis-stencil residual on the $N=5$ periodic cubic lattice by exact rational arithmetic. It audits the coefficient of every unordered monomial $\xi(u)\xi(v)$ in the mixed explicit-fiber three-axis stencil, matching the Python audit script without floating point.
Vertex5 is the abbreviation for lattice points of the $5\times5\times5$ torus (Vertex 5 5 5). Stencil residuals sum local contributions over bases, axis directions, and Freudenthal local pairs; those contributions must be collected by unordered endpoint pairs so diagonal and off-diagonal monomials are not double-counted under the canonical order vertex5CanonLE.
This predicate is the Boolean gate used throughout those expansions: it asks whether the ordered pair $(a,b)$ is the same unordered pair as $(u,v)$.
proof idea
Definition, not a proof. The body is decide applied to the Prop ((a = u ∧ b = v) ∨ (a = v ∧ b = u)), so Lean reduces equality of Vertex5 components and returns a Bool. No lemmas are invoked at the definition site; downstream results such as sameUnordered_translate prove translation invariance via injectivity of translateVertex5.
why it matters
Unordered pairing is the bookkeeping primitive for the entire coefficient certificate. It is used by axisStencilResidualCoeff (the residual coefficient sum), by the local expansions pairAxisCoeffExpansionAtN5, scaledPairLocalVertexCoeff, scaledPairLocalVertexCoeffExpansionAtN5, and by the monomial expansions unorderedCrossMonomialExpansionAtN5 and unorderedSameUnorderedMonomialExpansionAtN5.
Those pieces feed axisStencilCoeffSoundnessAtN5, which states that the corrected three-axis stencil is sound with respect to the unordered coefficient expansion and closes the RHS half of ExplicitFiberAxisStencilCoeffSoundnessAtN5. In the Recognition gravity stack this is lattice-level support for the discrete Dirichlet/Freudenthal stencil that underlies continuum limits, not a forcing-chain (T0–T8) step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.