Block34 — Canonical residual realization and global linear minimality
Status is determined by RESULTS.json and the final execution receipts.
Main result
The observable quotient constructed in Block33 is now identified with the intrinsic R-module generated by the prefix residuals of its all-word behavior. For f : List A -> R define f_u(w)=f(u ++ w) and H_f=span_R{f_u}. The state x of any realization is sent to its complete future-output function. The kernel is exactly Block33's unobservable submodule; the image of the reachable span is H_f.
Reachable-observable realizations of the same f are related by a UNIQUE R-linear isomorphism preserving seed, every digit transition, and output on every state. Any other reachable realization surjects onto them. From an arbitrary competitor, first restrict to its reachable submodule, then take that surjection. Consequently the canonical machine has minimum cardinality among ALL finite R-linear realizations of f, not merely among quotients of its predecessor.
The ring and alphabet are fixed. The theorem uses all words, including the empty word and noncanonical integer digit encodings. It does not assume a field or a free state module. Minimum module cardinality is not minimum DFA size or generator rank.
Actual masks
The source is Block33's actual quotient of the correlated reachable mask module. For prime p, positive r, integer A,B, p not dividing B(0), and A(0)=B(0) modulo p^r, its all-word output equals coefficient cartierWordValue(p,ds) of the canonical Mahler solution constructed in Block24. The new theorem applies to that very system. No alternative matrix model or supplied-series oracle is substituted.
The principal mask theorems are minimalMask_comparison, minimalMask_cardinality, minimalMask_unique_equiv, and minimalMaskEquivResidual_simulation. The theorem-level compileCanonicalMask returns a certificate containing the entire Block33 certificate, the residual equivalence and its simulation laws, all-word behavior, and the universal finite-cardinality lower bound.
This closes Goal I's MATHEMATICAL canonical/minimum-cardinality realization milestone. The earlier roadmap also requested a verified efficient executable compiler. That implementation-refinement obligation is not discharged by these noncomputable Lean definitions and remains explicitly open.
A finite behavioral comparison certificate
For two systems with state cardinalities p^b and p^c, the product difference system has cardinality p^(b+c). The inherited finite observation theorem gives
behavior M = behavior N
iff outputs agree on every word with length < b+c.
If behaviors differ, such a short distinguishing word exists. For finite alphabets this is a finite test. The horizon is sufficient, not asserted optimal. Enumerating all words up to it need not be efficient.
Restriction witnesses
The constant-one system on ZMod5 has a singleton initial orbit yet requires at least five elements in any linear realization with that behavior. This prevents calling the result minimum DFA cardinality. Scaling its seed by 2 and output by 3 changes coordinates but preserves its behavior; the intertwiner is uniquely forced. A zero-output system on the same underlying module has different behavior, so a module signature alone is not a complete machine invariant. The ZMod4 twice-identity example has a two-element canonical behavior module and satisfies the same cross-realization lower bound, without field-dimension arguments. A binary system emits zero on the empty word and every word ending in 1, but emits one at [0]. Full all-word comparison cannot be replaced silently by canonical-digit comparison. Those are universally quantified production examples where indicated.
Independent exact finite evidence
Ninety pairs of different realizations are checked by enumerating their small reachable spans and joint future-observation partitions. One side is enlarged with a driven silent coordinate, then conjugated by a unimodular change. The image of each span agrees with the span of residual vectors; the two intrinsic images agree. Output, additive/scalar laws, and every digit transition agree on class representatives.
Sixteen actual mask cases additionally use finite Hankel matrices with entries H(u,w)=a_(value(u)+p^length(u)*value(w)). Entries come from an independent direct Mahler coefficient recurrence. The image signatures computed by exact Smith normal form agree with the predecessor observable-quotient signatures. This is bounded reference evidence, not a formal Python-to-Lean executable refinement.
For A=1 the larger examples are:
| p | r | B | Hankel dimensions | Residual cyclic exponents | Cardinality |
|---|---|---|---|---|---|
| 2 | 4 | 1+4z | 7 x 1 | 4 | 2^4 |
| 2 | 8 | 1-z | 31 x 15 | 2,5,7,8,8 | 2^30 |
| 2 | 8 | 1+16z | 7 x 1 | 8 | 2^8 |
| 3 | 6 | 1+81z | 4 x 1 | 6 | 3^6 |
There is no additional state reduction relative to Block33. The new result changes the guarantee: the quotient is compared with every finite linear realization of its behavior. Concrete table counts are exact finite audit results, not separate kernel reductions of each complete noncomputable mask construction.
Verification and preservation
Five new production modules add 66 declared theorems to 1,054 inherited declarations. Every inherited mathematical source is byte-identical; the root receives one import. A fresh predecessor build passed first. The authoritative final run deleted only project-local build output and recompiled all 92 project modules under warning-as-error: 2618 Lake jobs completed. All 17 final phases passed with unchanged before/after execution-input hashes. All 1120 declared theorem axiom closures and 2510 project-owned environment theorem constants were audited; 19 declared theorems are axiom-free. Only propext, Quot.sound and Classical.choice occur. The final suite passed 58 new concrete examples, eight universal applications, 28 immediate-predecessor examples, five negative controls with the expected diagnostics, and a positive control. leanchecker replay and 3512 exact-integer assertions passed. Historical finite suites are not relabeled as fresh. See RESULTS.json and the per-command receipts.
All failed development drafts are retained. An accidental duplicated record field in a late certificate edit caused one syntax error; downstream probe passes that used older objects were not accepted as final evidence. The corrected source is subject to the authoritative empty-project-build-directory replay.
The exact toolchain remains Lean4.34.0-rc2 with pinned mathlib. Dependency caches are not independently rebuilt; leanchecker is another use of Lean's own kernel. Stable4.34.0 compatibility, independent human/kernel review, new state reduction across precisions, general compiler abstraction, and efficient runtime refinement remain separate obligations. No novelty or priority claim is made.