add4
plain-language theorem explainer
add4 supplies modular addition on the cyclic group of order 4 that models ququart displacements inside the coupled recognition cores. Researchers building Weyl monomials or coupled-core configurations cite it when composing shifts or recovering labels from summed indices. The definition is a direct construction that adds the underlying integer values and reduces modulo 4, with membership in Fin 4 discharged by omega.
Claim. For $a, b$ in the cyclic group of order 4, add4$(a,b) := (a + b) mod 4$.
background
The CoupledRecognitionCores module works with ququart states whose basis kets are indexed by Fin 4. add4 furnishes the group law for index shifts that appear in displacement maps and in the phase factors of local Weyl monomials. The upstream alias simply re-exports the identical definition from the OperatorCore submodule, keeping the arithmetic inside the finite setting required by the rest of the module.
proof idea
This is a one-line definition that forms the pair consisting of the sum of the two valuations reduced modulo 4 together with the membership proof generated by omega.
why it matters
add4 is the primitive group operation that enables the recovery theorem add4_eq_add4_iff_left_core, the cancellation add4_sub4_cancel_core, and the action localWeylMonomial_basisKet. It supplies the additive structure for the canonical ququart shift operator X and for addedConfig, thereby closing the discrete model needed by the Recognition Composition Law and the eight-tick octave in the parent framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.