Redesign boundary analysis + prove boundary_doors_odd for Sperner grid

[rjwalters]

Problem

The current boundary analysis in SpernerGrid.lean is built on an incorrect lemma:

boundary_verts_on_face is mathematically wrong. It claims that when gridAdj s k = none and k < d, all vertices j ≠ k have (s.verts j).onFace k (k-th barycentric coordinate = 0). This is false — cell face position does NOT correspond to barycentric coordinate.

no_boundary_doors_face_lt depends on this incorrect lemma.

Correct Architecture

Step 1: Remove incorrect lemmas

Delete boundary_verts_on_face and no_boundary_doors_face_lt.

Step 2: Prove boundary doors only occur at face d

After fixing boundaryFlip0 (#9043):

• Face k for 0 < k < d: gridAdj dispatches to interiorFlip which always returns some. No boundary faces.
• Face 0: boundaryFlip0 returns some for all valid simplices (d=0 excluded, d=1 returns none only on geometric boundary, d≥2 always returns some after fix). So boundary doors at face 0 only for d=1.
• Face d: boundaryFlipLast returns none iff v₀.coords(incDir(d-1)) = 0. This correctly identifies geometric face incDir(d-1).

Step 3: Characterize boundary doors at face d

When boundaryFlipLast returns none:

• All vertices v₀, ..., v_{d-1} have incDir(d-1) coordinate = 0 (on geometric face incDir(d-1))
• Sperner condition on this face: color incDir(d-1) is forbidden
• A door at face d requires colors {0, ..., d-1} on the face {v₀, ..., v_{d-1}}
• If incDir(d-1).val < d, color incDir(d-1) is in {0,...,d-1} but forbidden → NOT a door
• If incDir(d-1).val = d, then miss must be some value < d (since miss ≠ incDir(d-1) = d)
  • The face vertices use colors from {0,...,d-1} \ {miss} ∪ (possibly miss if not on that face)
  • This is the only case where boundary doors at face d can exist

Step 4: Prove boundary_doors_odd by induction on d

Base case (d = 0): Single vertex, no doors, count = 0... hmm, but we need ODD count. Actually for d=0, the standard simplex has a single vertex colored 0, and the panchromatic condition is trivially satisfied. The boundary door count setup needs to be verified for d=0.

Inductive step: Boundary doors at face d of the d-simplex grid correspond to doors in the (d-1)-dimensional boundary triangulation. By induction, this count is odd.

This is the hardest proof in the file and requires constructing the (d-1)-dimensional boundary complex from the face d simplices.

Acceptance Criteria

• boundary_verts_on_face removed (incorrect)
• no_boundary_doors_face_lt removed or replaced with correct version
• boundary_doors_odd proved (0 sorry)
• sperner_grid end-to-end theorem works

Affected Files

• proofs/Proofs/SpernerGrid.lean — boundary analysis redesign

Test Plan

• Docker build: ./proofs/scripts/docker-build.sh Proofs.SpernerGrid with 0 errors
• sperner_grid theorem compiles with only the CellComplex.sperner sorry (proved in SpernerMathlib4.lean)

Dependencies

• Fix Mathlib compatibility issues in SpernerGrid.lean #9042: Fix Mathlib compatibility issues
• Fix boundaryFlip0 miss-change case + complete grid adjacency proofs #9043: Fix boundaryFlip0 + complete adjacency proofs

References

• Analysis: research/sperner-grid-analysis.md (PR Analysis: Sperner grid boundary flip bug and architecture for Part 2 #9040)
• Parent: Sperner Part 2: SimplicialComplex → CellComplex bridge for mathlib4#25231 #8998

[rjwalters]

Curating this issue per user request.

Curator Assessment

The issue is well-formed with a clear problem statement, acceptance criteria, affected files, test plan, and dependencies. This enhancement adds implementation depth: specific line references, a fuller test plan, and clarifies the approach options for boundary_doors_odd.

---

Implementation Guidance

Structural overview

SpernerGrid.lean has three sections relevant to this issue:

• Lines 596–644 (boundaryFlip0): Returns none for face 0 when last_v.coords(miss) = 0. Correct for d = 1, incorrect for d >= 2 (see analysis doc). Issue Fix boundaryFlip0 miss-change case + complete grid adjacency proofs #9043 covers the fix.
• Lines 653–699 (boundaryFlipLast): Returns none for face d when v₀.coords(incDir(d-1)) = 0. Correct — this is a genuine geometric boundary identification.
• Lines 704–730 (gridAdj): For 0 < k < d, dispatches to interiorFlip, which always returns some. So gridAdj s k = none for 0 < k < d is vacuously false.

This vacuous truth means no_boundary_doors_face_lt (lines 795–821) holds formally even though its supporting lemma boundary_verts_on_face (line 781) is mathematically wrong. The only genuinely needed proof is for boundary doors at face d (the boundaryFlipLast case).

Step 1: Remove incorrect lemmas (lines 781–821)

Delete boundary_verts_on_face (lines 781–787) and no_boundary_doors_face_lt (lines 795–821). Their logical content is not needed: for 0 < k < d vacuous truth covers it; for k = 0 the boundary analysis must rest on different foundations after #9043.

Step 2: Boundary door characterization after fixes

After #9043 repairs boundaryFlip0:

• Face k for 0 < k < d: gridAdj dispatches to interiorFlip, always returns some. No boundary.
• Face 0 (k = 0): Fixed boundaryFlip0 returns some for all d >= 2. For d = 1, returns none only on the geometric boundary (miss coordinate depleted). Sperner still prevents a door there via the 1D base case.
• Face d (k = d): boundaryFlipLast returns none iff v₀.coords(incDir(d-1)) = 0, i.e., the simplex lies on geometric face incDir(d-1). This is the only source of boundary doors.

Step 3: Prove boundary_doors_odd (line 824)

The most likely proof strategy:

Option A — Induction on d (recommended by the issue)

1. Base case d = 0: Boundary door set is empty (no faces, count = 0, which is even, not odd). Note: the standard convention may need adjustment — in dimension 0 Sperner's Lemma is trivial (a single colored vertex). Verify what boundary_doors_odd should claim at d = 0 before proceeding.
2. Inductive step: The boundary simplices at face d of the d-dim grid form a grid triangulation of the (d-1)-simplex. A door at face d of a d-simplex corresponds (via boundaryFlipLast) to a panchromatic (d-1)-simplex in the boundary triangulation. By induction the count is odd.
3. Key construction needed: an explicit bijection or correspondence between boundary doors of d-dim grid and boundary doors of (d-1)-dim boundary triangulation.

Option B — Direct parity argument via the incDir(d-1) face (simpler if induction is too hard)

Show directly that the set of boundary doors is in bijection with a set whose parity follows from an explicit combinatorial counting argument (e.g., grouping pairs of boundary simplices by their miss direction).

Option C — Punt with a localized sorry

If the boundary induction construction is blocking the larger #8998 effort, keep boundary_doors_odd as sorry and note it is the one remaining mathematical obligation.

Key definitions to understand

Symbol	Location	Meaning
IsSperner c	Line 184	v.onFace k → c v ≠ k — Sperner labeling condition
IsDoor c K s k	Line 101	Facet k of s is a rainbow door
BaryPoint.onFace	Line 173	Barycentric coordinate k = 0
boundaryFlipLast	Line 653	Adjacency at face d; none = geometric boundary
incDir(d-1)	Accessed via s.incDir ⟨d-1, _⟩	Direction for last flip step

Affected Files

• proofs/Proofs/SpernerGrid.lean lines 781–834 — remove boundary_verts_on_face + no_boundary_doors_face_lt, replace with correct boundary_doors_odd proof
• research/sperner-grid-analysis.md — reference doc with counterexample and correct architecture

Test Plan

• Manual verification: boundary_verts_on_face and no_boundary_doors_face_lt are deleted with no downstream breaks (only no_boundary_doors_face_lt calls boundary_verts_on_face; verify nothing else calls either)
• Manual verification: boundary_doors_odd at line 824 has no sorry
• Docker build: ./proofs/scripts/docker-build.sh Proofs.SpernerGrid exits with 0 errors
• Compile check: sperner_grid theorem (line 851) compiles; only permitted sorry is CellComplex.sperner (line 127, covered by SpernerMathlib4.lean)
• Edge case: verify d = 0 behavior — confirm boundary_doors_odd holds (count 0 = even, but check if the theorem's Odd claim needs d >= 1 hypothesis)
• Edge case: verify d = 1 boundary door count = 1 (or odd) with a concrete coloring

Dependencies

• Fix Mathlib compatibility issues in SpernerGrid.lean #9042: Fix Mathlib compatibility issues in SpernerGrid.lean — required for the file to build at all
• Fix boundaryFlip0 miss-change case + complete grid adjacency proofs #9043: Fix boundaryFlip0 + complete grid adjacency proofs — required so face-0 boundary characterization is correct

Note: Both dependencies are currently open (loom:curating). This issue is blocked until both complete.