# 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.