sub4
plain-language theorem explainer
Modular subtraction on Fin 4 supplies the inverse operation to modular addition in this module. It is referenced by researchers building discrete ququart models and Weyl operators for coupled cores. The definition reduces directly to integer arithmetic inside the Fin constructor, with omega discharging the range check.
Claim. For $a, b$ in the cyclic group of order 4, define $a - b := (a.val + (4 - b.val)) mod 4$, with the result packaged as an element of Fin 4.
background
The CoupledRecognitionCores module assembles finite algebraic tools for ququart states in the Recognition Science foundation. QuquartState is the type of functions from Fin 4 to ℂ, while CoupledCoreIndex N tracks configurations across multiple cores with values in Fin 4. The module imports Mathlib to access Fin types and complex arithmetic.
proof idea
The declaration is a direct term-mode definition. It builds the Fin 4 value from the integer expression (a.val + (4 - b.val)) % 4. The omega tactic certifies that the computed value lies between 0 and 3 inclusive.
why it matters
This definition is invoked by add4_sub4_cancel, add4_sub4_cancel_core, localWeylMonomial, localWeylMonomial_basisKet, shiftedConfig, and shiftedConfig_zero. It supplies the displacement operation that lets Weyl monomials act on basis kets and lets configurations be shifted componentwise. The mod-4 structure supplies the discrete symmetry layer required by the coupled-core constructions that sit beneath the forcing chain steps T5-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.