Paper II: Refinement Towers, Weighted Transfer, and Integral Separation of Operator Packets

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

Read this chapter with formatted equations

1 \section{Worked realizations in the common operator language}
2 
3 \subsection{Signal polyphase coordinates}
4 
5 Let $x=(x_n)_{n\in\Z}\in c_{00}(\Z;R)$ and let the seed be $\delta_0$
6 under the bilateral shifts $(S^r\delta_0)_n=\delta_{n,r}$. This makes the
7 algebraic span and every displayed sum finite. The $N$ packets are
8 \[
9 x_j[m]=x[Nm+j].
10 \]
11 Synthesis interleaves these sequences. A linear filter with a finite impulse
12 response that is invariant under shifts becomes an $N\times N$ matrix of
13 transfer blocks. Refining from $N$ to $M$ with $N\mid M$ splits each coarse
14 phase into its descendants without changing the reconstructed signal. The
15 same formulas extend to standard sequence completions when the synthesis
16 series converges. This is the usual polyphase viewpoint from multirate filter
17 banks \cite{Vaidyanathan1993}.
18 
19 \subsection{Sparsity of transfer blocks}
20 
21 A banded operator need not remain banded after residue reordering, but its
22 nonzero couplings become a structured packet graph. With the convention
23 $(S_rx)_n=x_{n-r}$, the only active transfer is
24 \[
25 P_{N,j+r}S_rP_{N,j},
26 \]
27 with indices taken modulo $N$. More general finite stencils produce a finite set of active phase differences.
28 
29 \begin{figure}[htbp]
30 \centering
31 \includegraphics[width=0.96\textwidth]{10_transfer_block_sparsity.pdf}
32 \caption{Norms of packet blocks for a finite stencil. The original operator is exactly reconstructed from a sparse transfer pattern.}
33 \label{fig:block-sparsity}
34 \end{figure}
35 
36 \subsection{A short realization in Smith chart coordinates}\label{sec:smith-realization}
37 
38 \begin{interpretation}
39 The Smith chart used here is a coordinate diagram for impedance and reflection. It is different from the Smith normal form used earlier to study integral congruences. The connection within this paper is the way a change of coordinates makes an action easier to describe. Here a rotation in reflection coordinates becomes a fractional linear map in impedance coordinates. The sampled phase orbit is a geometric example and does not supply another linear projector decomposition.
40 \end{interpretation}
41 
42 Let $Z$ and $Z_0\ne0$ be complex impedances, put $z=Z/Z_0$, and assume $z\ne-1$. Write
43 \[
44 \Gamma=\frac{z-1}{z+1}.
45 \]
46 On the open reflection disk $|\Gamma|<1$, multiplication by any phase $\omega_N^k$ stays in the disk and has a finite inverse-chart image. The phase action is
47 \[
48 \Gamma\mapsto\omega_N^k\Gamma.
49 \]
50 Outside the open disk, the same chart formula requires $1-\omega_N^k\Gamma\ne0$. Pulling the phase action back on this domain gives
51 \[
52 T_{N,k}(z)
53 =
54 \frac{(1+\omega_N^k)z+(1-\omega_N^k)}
55 {(1-\omega_N^k)z+(1+\omega_N^k)}.
56 \]
57 For $N=2$ and $k=1$,
58 \phantomsection
59 \[
60 T_{2,1}(z)=\frac1z,
61 \qquad z\ne0,-1.
62 \label{eq:smith-inversion}
63 \]
64 Thus the nontrivial action at the first phase level exchanges normalized
65 impedance and admittance. Calling these values ``packets'' is geometric
66 terminology for the sampled orbit. It does not assert that the two values
67 form linear idempotent ranges. Higher refinements at powers of $2$ sample the
68 same reflection circle at progressively finer electrical phases. Compare the
69 standard Smith chart conventions in \cite{pozar2012}.
70 
71 \begin{figure}[htbp]
72 \centering
73 \includegraphics[width=0.96\textwidth]{11_smith_polyphase_orbit.pdf}
74 \caption{Nested phase orbits at powers of $2$ on the Smith reflection disk. The full treatment of the Smith chart is deferred to the signal paper.}
75 \label{fig:smith-orbit}
76 \end{figure}
77 
78 The symmetric weight
79 \[
80 w_{\mathrm{Smith}}(\Gamma)
81 =
82 \frac1{|1-\Gamma|^2}
83 +
84 \frac1{|1+\Gamma|^2}
85 \]
86 indicates where small errors in reflection coordinates produce large impedance or admittance errors.
87 
88 \begin{figure}[htbp]
89 \centering
90 \includegraphics[width=0.96\textwidth]{12_smith_adaptive_weight.pdf}
91 \caption{A symmetric refinement weight concentrated near the boundary points for open and short circuits.}
92 \label{fig:smith-weight}
93 \end{figure}
94 
95 
96 \section{Finite computational certificates}
97 The following results and tables are the recorded v1.2.1 finite implementation evidence.  They do not certify the expanded lattice or analytic statements in Lean.  Current reproduction outcomes are reported in the verification files accompanying this edition.
98 
99 
100 All numerical work in this paper is finite and reproducible. It tests the
101 Python implementation of identities proved above or checked against
102 certificates. It does not replace those arguments or the Lean kernel checks.
103 Release 1.2.1 runs 48 tests, including contracts for invalid input, refinement
104 transitivity, aggregation of transfer blocks, Fourier/DFT agreement, Smith
105 fibre counts by exhaustive enumeration, and consistency of the stored JSON
106 and CSV records.
107 
108 \begin{table}[htbp]
109 \centering
110 \caption{Representative numerical and symbolic checks.}
111 \begin{tabularx}{\textwidth}{L{0.54\textwidth}Y}
112 \toprule
113 Check & Result \\
114 \midrule
115 Packet synthesis residuals for moduli $2,3,4,6,8,12$ & $0$ \\
116 Nested refinement residuals for $2\to4$, $2\to8$, $3\to6$, $3\to12$, $4\to8$, $4\to12$, $6\to12$ & $0$ \\
117 CRT residuals for dyadic and odd moduli for $4\times3$, $8\times3$, $4\times5$, $8\times5$ & $0$ \\
118 Maximum finite Fourier projector residual & $6.60\times10^{-15}$ \\
119 Weighted inverse residual modulo $2^{10}$ & $0$ \\
120 Weighted inverse residual modulo $3^8$ & $0$ \\
121 Weighted inverse residual modulo $5^7$ & $0$ \\
122 Difference between filtered and direct modular inverses & $0$ \\
123 Transfer zeta coefficients versus direct walk enumeration through weight $30$ & exact match \\
124 Dyadic sign projector resultant weight & $v_2(2)=1$ \\
125 Sign projector resultant weight at the odd prime $3$ & $v_3(2)=0$ \\
126 Power defect telescoping identity residual & at most $6.94\times10^{-18}$ \\
127 Resolvent defect identity residual & $1.09\times10^{-17}$ \\
128 Smith $N=2$ phase versus $z\mapsto1/z$ & residual below $1.4\times10^{-16}$ \\
129 \bottomrule
130 \end{tabularx}
131 \end{table}
132 
Statement: Weighted inverse133 \begin{certificate}[Weighted inverse]
134 For the tested diagonal-plus-transfer matrices, the filtered inverse agrees exactly with direct modular inversion at all tested precisions:
135 \[
136 2^{10},\qquad3^8,\qquad5^7.
137 \]
138 The maximum modular residual is zero in every case.
139 \end{certificate}
140 
Statement: Transfer zeta141 \begin{certificate}[Transfer zeta]
142 The rational function
143 \[
144 \frac{-t^3}{t^9-t^7-t^6-t^5+2t^4+t^3+t^2-1}
145 \]
146 was expanded through degree $30$. Every coefficient agrees with direct weighted-walk enumeration.
147 \end{certificate}
148 
Statement: Dyadic separation149 \begin{certificate}[Dyadic separation]
150 The code verifies exactly that the two rational sign projectors are idempotent, orthogonal, and complementary, that scaling by $2$ makes both integral, and that the same projectors are already integral modulo every tested odd prime.
151 \end{certificate}
152 
153 
154 \section{Scope and limits}\label{sec:limits}
155 
156 The exact statements above have several deliberate boundaries.
157 
158 First, refinement changes coordinates while preserving reconstruction. If a numerical method discards fine packets, the resulting error must be estimated separately.
159 
160 Second, the weighted inverse is linear.  A nonlinear map creates higher order interactions among packet coordinates.  Those interactions are not contained in the path formula of \cref{thm:weighted_inverse}.
161 
162 Third, a resultant is only a denominator bound.  The exact weight depends on the lattice and is given by \cref{thm:gluing_weight}.  The two examples in \cref{ex:loose_resultant,ex:lattice_dependence} show that the same eigenvalue separation can give different integral packet weights.
163 
164 Fourth, the dyadic sign example is a model rather than a classification of all phenomena at the prime two.  Character averages, trace splittings, quadratic refinements, and deformation projectors must each be checked on their own lattices.
165 
166 Finally, the defect formulas do not prove that a chosen coarse operator is a good approximation.  They say exactly how a known one step defect propagates.  A useful approximation theorem must also bound that defect in the problem under study.
167 
168 
169 
170 \appendix
171 \section{Notation table}
172 
173 \begin{longtable}{L{0.28\textwidth}L{0.64\textwidth}}
174 \toprule
175 Symbol & Meaning \\
176 \midrule
177 \endhead
178 $P_{\ell,\alpha}$ & packet projector at refinement level $\ell$ \\
179 $I_\ell$ & packet address set at level $\ell$ \\
180 $\beta\succ\alpha$ & fine packet $\beta$ is a child of coarse packet $\alpha$ \\
181 $\cA_\ell,\cS_\ell$ & packet analysis and synthesis maps \\
182 $J_{\ell+1,\ell}$ & exact coordinate refinement map \\
183 $C_{\ell,\ell+1}$ & exact coordinate regrouping from fine to coarse \\
184 $T^{(\ell)}_{\beta\alpha}$ & transfer block $P_{\ell,\beta}TP_{\ell,\alpha}$ \\
185 $P_{N,j}$ & residue or phase selector for address $j\pmod N$ \\
186 $w(e)$ & positive filtration weight of a transfer edge \\
187 $W(\gamma)$ & cumulative weight of a transfer word or graph walk \\
188 $A(t)$ & polynomial weighted adjacency matrix \\
189 $Z_{s,t}(t)$ & weighted transfer-zeta function from vertex $s$ to vertex $t$ \\
190 $s_{\pi,\Lambda}(E)$ & separation weight of a rational projector on the chosen lattice, when a clearing exponent exists \\
191 $\Delta$ & linear refinement defect for one step $CT_f-T_cC$ \\
192 \bottomrule
193 \end{longtable}
194 
195 \section{Algorithmic forms}\label{sec:algorithms}
196 
197 \subsection{Residue analysis and synthesis}\label{alg:residue}
198 
199 \begin{lstlisting}
200 def analyze_residues(x, N):
201     require N > 0
202     return [x[j::N] for j in range(N)]
203 
204 def synthesize_residues(packets):
205     N = len(packets)
206     require packet lengths fit one N-way interleaving
207     y = empty(sum(len(p) for p in packets))
208     for j, packet in enumerate(packets):
209         y[j::N] = packet
210     return y
211 \end{lstlisting}
212 
213 The verified contract is
214 $\operatorname{synthesize}(\operatorname{analyze}(x,N))=x$. The Lean
215 counterpart uses packet coordinates restricted to projector ranges and proves
216 both inverse laws. The finite Python routine checks the concrete array
217 realization.
218 
219 \subsection{Weighted inverse at finite precision}\label{alg:weighted-inverse}
220 
221 \begin{lstlisting}
222 Dinv = inverse(D)                       # certified on both sides
223 edge[e] = Dinv @ H_edge[e]
224 require Dinv @ H == sum(edge[e] for e in edges)
225 require edge[e] lies in filtration[weight[e]]
226 m = certified_lower_bound(weight)       # 1 <= m <= weight[e]
227 N = (L + m - 1) // m                    # so L <= m*N
228 S = 0
229 for n in range(N):
230     for word in edge_tuples(edges, n):
231         if sum(weight[e] for e in word) < L:
232             S += (-1)**n * ordered_product(edge[e] for e in word)
233 return q_L(S @ Dinv)
234 \end{lstlisting}
235 
236 Lean proves that the mapped pruned sum is exactly the mapped finite geometric
237 inverse. The lower bound $m$ gives $m|\gamma|\le W(\gamma)$, so
238 $L\le mN$ derives $q_L(A^N)=0$ from the filtration certificate and makes the
239 returned value an inverse on both sides of $q_L(D+H)$. The Lean lemma
240 $L\le m\lceil L/m\rceil$ justifies the displayed executable cutoff for
241 $m>0$. Taking $m=1$ and $N=L$ gives
242 the unconditional cutoff for positive weights. The Python implementation checks the
243 DVR matrix specialization against direct modular inversion.
244 
245 \subsection{Walk construction for transfer zeta}\label{alg:path-zeta}
246 
247 \begin{lstlisting}
248 def coefficient(G, start, target, n):
249     total = 0
250     for length in range(n + 1):
251         for word in edge_tuples(G, length):
252             if is_walk(word, start, target) and weight(word) == n:
253                 total += 1
254     return total
255 
256 A[i,j] = sum(t**weight(e) for distinct edges e from i to j)
257 T = I - A
258 Q = det(T)
259 H = adjugate(T)
260 P = H[start, target]
261 assert Q.coeff(0) == 1
262 Z = coefficient_series(G, start, target)
263 prove Q * Z == P
264 \end{lstlisting}
265 
266 Positive weights make the coefficient loop finite because every contributing
267 word has length at most $n$. Lean proves the enumeration correct, derives its
268 recurrence from the first edge, proves $(I-A)Z=I$, constructs the
269 determinant/adjugate inverse, and identifies the two matrices by inverse
270 uniqueness. Thus the normalized $QZ=P$ identity and its induced recurrence
271 follow from finite graph data. The Python companion repeats the exact symbolic
272 construction as an executable check. The Lean proof does not use it as an
273 oracle.
274 
275 \section{Proof dependency map}
276 
277 \begin{figure}[htbp]
278 \centering
279 \includegraphics[width=0.96\textwidth]{13_theorem_dependency.pdf}
280 \caption{The dependency structure of Paper II. Coordinate coherence, residue/CRT, weighted inversion, automatic finite-graph transfer rationality, and integral separation are distinct branches with explicit inputs.}
281 \label{fig:dependency}
282 \end{figure}
283 
284 The proof order is:
285 \[
286 \begin{aligned}
287 &\text{complete packet axioms}
288   \Rightarrow\text{finite-packet uniqueness and coordinate coherence}\\
289 &\qquad\Rightarrow\text{coordinate naturality and refined transfer blocks},\\
290 &\text{residue selectors and a finite Fourier table}
291   \Rightarrow\text{Fourier formulas},\\
292 &\text{coprime moduli}\Rightarrow\text{dyadic--odd formulas},\\
293 &\text{quotient, filtration, and edge-weight certificates}
294   \Rightarrow\text{explicit pruned inverse},\\
295 &\text{finite positive-weight graph}
296   \Rightarrow\text{semantic enumeration and first-edge recurrence}\\
297 &\qquad\Rightarrow\det/\operatorname{adj}\text{ rationality and recurrence},\\
298 &\text{minimal evaluated B\'ezout data and inverse-unit lattice action}\\
299 &\qquad\Rightarrow\text{separation bound, upward closure, and precision delay},\\
300 &\text{concrete }\mathbb Z/p^L\mathbb Z\text{ coordinate fibres}
301   \Rightarrow\text{finite Smith product count},\\
302 &\text{one-step typed defect}
303   \Rightarrow\text{powers, polynomial actions, and witnessed resolvents}.
304 \end{aligned}
305 \]
306 
307 The walk branch for transfer zeta is logically independent of operator
308 inversion. Its rationality conclusion follows from finite graph data without
309 a supplied $QZ=P$ premise. Likewise, CRT factorization follows directly from
310 residue selectors and coprimality. It does not require the abstract refinement
311 theorem, although it supplies a concrete refinement family. General Smith
312 diagonalization and the construction of polynomial B\'ezout/resultant data
313 remain inputs to the formalized branches that use those certificates.
314 

Back to source controls

Back to Paper II: Refinement Towers, Weighted Transfer, and Integral Separation of Operator Packets