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