modularInterpret_zero
This theorem shows that the periodic interpretation of the identity element in the free orbit maps to the zero residue in the cyclic carrier of size k+2. Researchers building finite realizations of the forcing would cite it as the base case for the zero element. The proof is a term-mode reduction that applies Fin extensionality and invokes the arithmetic fact that zero modulo any positive integer is zero.
claimFor any natural number $k$, the periodic interpretation of the identity element of the forced natural numbers equals the zero element of the finite cyclic set of cardinality $k+2$.
background
The module constructs periodic finite-cyclic realizations for Universal Forcing. The internal orbit remains the free forced natural numbers while the carrier interpretation is made periodic. This demonstrates that Universal Forcing does not require every realization to embed arithmetic faithfully into the carrier.
proof idea
The proof applies the extensionality lemma for finite sets to reduce the equality to an equality of representatives. It then rewrites the goal to $0$ modulo the modulus value and applies the standard lemma that zero modulo any positive integer vanishes.
why it matters in Recognition Science
This base case supplies the zero element inside the modularRealization definition, which constructs the finite cyclic Law-of-Logic realization with periodic interpretation. It completes the zero-cost carrier element required for the foundation, consistent with the allowance for non-faithful arithmetic embeddings in the forcing framework.
scope and limits
- Does not specify the interpretation of any non-identity element obtained by the step constructor.
- Does not establish invariance of the cost function under the modular reduction.
- Does not compare this periodic carrier to the discrete realization in terms of embedding properties.
- Does not address dependence of physical predictions on the choice of modulus size.
formal statement (Lean)
50@[simp] theorem modularInterpret_zero (k : ℕ) :
51 modularInterpret k ArithmeticFromLogic.LogicNat.zero = ⟨0, modulus_pos k⟩ := by
proof body
Term-mode proof.
52 apply Fin.ext
53 change 0 % modulus k = 0
54 exact Nat.zero_mod (modulus k)
55