M
plain-language theorem explainer
The definition M constructs the cyclic recognition structure on the three-element set with the successor relation modulo three. Researchers deriving defect-distance bounds and quasi-triangle inequalities in the Recognition framework cite this as the base three-state model. The construction directly populates the RecognitionStructure record by setting the universe to Fin 3 and defining the relation via modular successor, with the range proof discharged by Nat.mod_lt.
Claim. Let $M$ be the recognition structure whose universe is the set $U = {0,1,2}$ equipped with the binary relation $R(i,j)$ holding precisely when $j ≡ i + 1 mod 3$.
background
A RecognitionStructure consists of a type $U$ serving as the universe of recognizers together with a binary relation $R : U → U → Prop$. The upstream minimal stub from Chain supplies exactly this record for standalone compilation, while the core Recognition module supplies a general instance using structural equality on its own $U$. RS-native units fix the gauge by setting $τ_0 = 1$ tick, $ℓ_0 = 1$ voxel and $c = 1$ (quoted: “RS-native gauge: τ₀ = 1 tick, ℓ₀ = 1 voxel, c = 1”).
proof idea
The definition directly constructs the record: the universe field is set to Fin 3 and the relation field is defined by the successor map $j = (i.val + 1) % 3$, with the proof that the result lies in Fin 3 supplied by Nat.mod_lt together with the decide tactic.
why it matters
This supplies the concrete three-cycle instance required by downstream results in CostAlgebra, including defectDist_le_J_of_ratio_bounds, defectDist_quasi_triangle_local and quasiTriangleConstant_eq. It feeds the constant derivations in MassToLight. In the framework it realizes the three-dimensional case (T8: D = 3) and provides a minimal periodic structure compatible with the eight-tick octave and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.