PhaseVector
plain-language theorem explainer
Integer 3-vectors index discrete phase (Bloch) displacements on the Regge TT lattice. Anyone assembling bucket keys for the stencil audit cites this type. It is a one-line abbreviation: maps from a 3-element index set into the integers.
Claim. A phase vector is a map $u \colon \{0,1,2\} \to \mathbb{Z}$, equivalently an ordered triple of integers $(u_0,u_1,u_2)$ used as a discrete displacement key for phase buckets.
background
This module is the panel-locked C11 Regge TT Bloch interface audit (attempt 2). It keeps the first gate narrow: a literal $6\times 6\times 6$ raw cell stencil over tetrahedra and ordered slot pairs, with A2 reduced second variation matched by distributing a finite inner sum. Full rational bucket aggregation and hinge-aware zero-mode cancellation remain open.
Phase vectors supply the integer displacement keys that label those buckets. In the local convention a bucket is a triple (left face index, right face index, phase), and the only intended external identification is $(f,g,u)\sim(g,f,-u)$. The three coordinates match the three spatial directions of the lattice (consistent with the forced $D=3$ landmark).
Downstream, componentwise negation of a phase vector implements the reversal half of that identification.
proof idea
Pure abbreviation: PhaseVector is definitionally Fin 3 → Int. No proof obligations, lemmas, or tactics.
why it matters
Gives the phase field type inside Bucket and the domain of negPhase (and thus Bucket.swap). Without a shared integer 3-key, the stencil cannot be partitioned into rational buckets for the still-open gate A2-full (aggregate_raw_weight_eq_rational) or the hinge-aware zero-mode gate A3. The three-component shape is the discrete counterpart of spatial dimension three in the forcing chain (T8). The module explicitly does not yet quotient or aggregate all fibers, so this type is scaffolding for the non-tautological audit rather than a continuum or spike certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.