one_val
plain-language theorem explainer
At any distinction-orbit modulus N, the multiplicative identity of the unit-residue carrier projects to the native one-step orbit. Character-theory and factorization arguments on residues cite this projection lemma. The equality is definitional: a one-line reflexivity proof.
Claim. For every distinction-orbit modulus $N$, if $1_N$ denotes the multiplicative identity in the unit-residue carrier at $N$, then the underlying value of $1_N$ equals the native one-step orbit.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, used as the native arithmetic of the recognition register. Residues are formed by the native remainder against a nonzero orbit modulus N.
A residue is a unit residue when it satisfies the native unit predicate. In the finite δ-orbit that predicate collapses to equality with the one-step orbit: the only multiplicative unit is one. The structure UnitResidue packages a value together with a proof that it is a unit residue; its doc-comment states that unit residues form the carrier for finite multiplicative character theory.
The local module builds the multiplicative monoid (and certificate) on that carrier. The identity element one N is the UnitResidue whose value is the native one and whose unit proof is the corresponding unitResidue witness.
proof idea
Term-mode reflexivity. The identity constructor of the unit-residue carrier is defined to store DistinctionNat.one in the value field, so projecting .val is definitionally equal to the native one-step orbit. No lemmas are applied; rfl closes the goal.
why it matters
This is a projection lemma in the unit-residue monoid infrastructure under PrimitiveRecognitionCalculus.Factorization. It anchors the multiplicative identity so later lemmas (multiplication closure, powers, the UnitGroupCertificate) can rewrite values without unpacking constructors by hand.
In the broader Recognition stack, unit residues supply the finite multiplicative character surface on the distinction orbit. That surface sits under factorization and orbit-divisibility arguments that feed the forcing chain's discrete register structure (eight-tick octave, finite-dimensional recognition calculus). No downstream theorems currently list this declaration as a direct dependency; it is local scaffolding for the unit-group certificate in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.