negPhase
plain-language theorem explainer
Componentwise negation of an integer phase-displacement key on three lattice directions. Gravity auditors cite it when building the swap representative of a Bloch bucket under the external identification (f,g,u) ~ (g,f,-u). The body is a one-line pointwise map on Fin 3 → Int.
Claim. Given a phase key $u:\{0,1,2\}\to\mathbb{Z}$, define $(\mathrm{neg}\,u)(i)=-u(i)$ for each coordinate $i$.
background
This module is the panel-locked C11 Regge TT Bloch interface audit (attempt 2). It keeps the first gate narrow: a literal 6×6×6 raw cell stencil and a non-tautological A2 reduction, without claiming full rational bucket aggregation or zero-mode cancellation.
A phase key is an integer displacement vector on three directions (PhaseVector := Fin 3 → Int). Buckets are triples (left, right, phase) with face indices in Fin 6 and such a phase. The intended external convention only identifies (f,g,u) with (g,f,-u); this attempt does not yet quotient or aggregate all fibers.
Negation of the phase is the algebraic half of that swap. The continuum-limit and spike-certificate modules are deliberately not imported here.
proof idea
Definitional one-liner: return the function i ↦ -u i. No lemmas, no tactics. Downstream Bucket.swap applies it after swapping the two face indices.
why it matters
Supplies the phase half of Bucket.swap, the reversal representative for the external identification (f,g,u) ~ (g,f,-u). Without componentwise sign flip, bucket quarantine and any later rational-weight comparison against Jacobian data would break the intended symmetry of the Bloch phase lattice.
The parent structure is the in-module Bucket. Full gates remain open: A2-full aggregation over all buckets, A3 hinge-aware zero-mode, and Gate B spike convention. This def is pure scaffolding for those audits, not a physics claim about continuum gravity or RS forcing (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.