Realization Calculus

Download original file

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

Read the typeset paper

1 \clearpage
2 \section{Whole finite extensions and dyadic marking criteria}\label{app:dyadic_markings}
3 
4 Evidence: direct reading of the original dyadic contract and ordinary
5 finite group proofs. This note does not prove a dyadic arithmetic field
6 construction, its simple-character existence, nontrivial stabilizer
7 attachment, H5, or a Lean closure. It identifies exactly what a supplied
8 actual host and sector must preserve, and proves the marked finite
9 attachment step for C=\{1\}.
10 
11 \hypertarget{dyadic_markings-the-original-datum-includes-more-than-the-alternating-form}{%
12 \subsection{1. The original datum includes more than the alternating
13 form}\label{dyadic_markings-the-original-datum-includes-more-than-the-alternating-form}}
14 
15 The original text
16 \path{closure_attempt162/inputs/original_reading.txt} states in
17 Definition~11.1, starting line 4911, that at p=2 a restricted bridge
18 additionally supplies compatible quadratic refinements and an
19 isomorphism of the resulting Heisenberg central extensions lifting the
20 given symplectic isometry. Sections~13.1--13.9 define the refinements and
21 their Arf/Gauss signs.
22 
23 The retained visual appendix is particularly explicit, at
24 lines 6892--6947: with center \{I,-I\} fixed, squares of lifts carry the
25 quadratic bit. Multiplying a lift by i changes the particular finite
26 central-extension realization. The appendix says that allowing complex
27 scalar rescaling \textbf{without recording this distinction} erases data
28 that the bridge is required to retain.
29 
30 The finite record must therefore retain at least:
31 
32 \begin{itemize}
33 \tightlist
34 \item
35   the labeled symplectic quotient and its pairing;
36 \item
37   the supplied quadratic refinement q;
38 \item
39   the specified finite central extension, its central
40   embedding/character, and any marked lifts or specified extension
41   isomorphism;
42 \item
43   the resulting normalized Gauss sign, and all declared phase operators;
44 \item
45   the complete original character values retained by the scalar pushout.
46 \end{itemize}
47 
48 The last item alone does not retain the preceding finite-subgroup/lift
49 marking unless that marking is explicitly carried along. The raw text
50 does not require literal embeddings of the old arithmetic matrix groups
51 into a new type. Nor does it define a unique quadratic refinement
52 extracted automatically from an unmarked C× scalar extension of every
53 arithmetic type.
54 
55 \hypertarget{dyadic_markings-general-finite-central-extension-criterion}{%
56 \subsection{2. General criterion for finite central extensions}\label{dyadic_markings-general-finite-central-extension-criterion}}
57 
58 Let V be an elementary abelian 2-group with ordered basis
59 v\_1,\ldots,v\_m. Let E\_s and E\_t be central extensions of V by the
60 same abelian group Z. Fix the identity on Z and a quotient isomorphism
61 f.~Choose lifts a\_i of v\_i in E\_s and b\_i of f(v\_i) in E\_t. Write
62 
63 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
64 a_i²=s_i,  b_i²=t_i,  [a_i,a_j]=c_ij, [b_i,b_j]=d_ij.
65 \end{Verbatim}
66 
67 Every element has a unique normal form
68 
69 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
70 z a_1^(epsilon_1) ... a_m^(epsilon_m), epsilon_i in {0,1},
71 \end{Verbatim}
72 
73 and analogously on the target. The multiplication is completely
74 determined by the displayed squares and commutators.
75 
76 \textbf{Criterion.} A center-fixing isomorphism lifting f exists
77 precisely when
78 
79 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
80 c_ij=d_ij for every i,j,
81 s_i/t_i belongs to Z² for every i.                     (1)
82 \end{Verbatim}
83 
84 Indeed, every such isomorphism must take a\_i to lambda\_i b\_i for some
85 lambda\_i in Z, forcing lambda\_i²=s\_i/t\_i. Conversely these equations
86 make the assignment a\_i -\textgreater{} lambda\_i b\_i preserve all
87 relations, and the normal forms prove it is bijective.
88 
89 If the \textbf{particular lifts} a\_i and b\_i must correspond exactly,
90 the condition is s\_i=t\_i, with lambda\_i=1. If a full chosen section
91 is marked, rather than only generating lifts, its multiplication
92 coefficients must also correspond:
93 
94 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
95 a(v)a(w)=c_s(v,w)a(v+w),
96 b(fv)b(fw)=c_t(fv,fw)b(f(v+w)),
97 \end{Verbatim}
98 
99 and exact section preservation requires c\_s(v,w)=c\_t(fv,fw) for every
100 pair. Transporting the complete section under an existing group
101 isomorphism retains these identities automatically. Preserving just its
102 squares need not retain an additional independently specified section.
103 
104 \hypertarget{dyadic_markings-fixed-two-element-center}{%
105 \subsubsection{2.1. Fixed two-element
106 center}\label{dyadic_markings-fixed-two-element-center}}
107 
108 For Z=\{+1,-1\}, Z²=\{1\}. The lift square is independent of the lift
109 within its fiber and defines
110 
111 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
112 a(v)²=(-1)^(q_s(v)).
113 \end{Verbatim}
114 
115 The identity (ab)²=a²b²{[}b,a{]} gives the quadratic refinement law.
116 Criterion (1) becomes the exact requirement
117 
118 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
119 q_t(f(v))=q_s(v) for every v.                          (2)
120 \end{Verbatim}
121 
122 For an unspecified symplectic isomorphism between equal-dimensional
123 nondegenerate spaces, such an f exists exactly when their Arf invariants
124 agree. For a preassigned f, equality of Arf invariants alone is
125 insufficient: (2) must hold for that f.
126 
127 \hypertarget{dyadic_markings-four-element-and-complex-centers}{%
128 \subsubsection{2.2. Four-element and complex
129 centers}\label{dyadic_markings-four-element-and-complex-centers}}
130 
131 For Z=mu\_4, multiplication of a lift by i changes its square by -1. The
132 unmarked extension criterion preserves square classes modulo Z²=mu\_2.
133 In particular, squares +1 and -1 do not distinguish unmarked mu\_4
134 extensions. A separately marked finite mu\_2-central extension subgroup
135 (such as the full D8 or Q8), or prescribed lifts, still distinguishes
136 them.
137 
138 For Z=C× every square ratio has a square root. Thus matching commutators
139 is sufficient for an unmarked center-fixing extension isomorphism. This
140 fact does not delete a marked finite subgroup from the objects being
141 compared.
142 
143 \hypertarget{dyadic_markings-exact-d8q8-check}{%
144 \subsection{3. Exact D8/Q8 check}\label{dyadic_markings-exact-d8q8-check}}
145 
146 In dimension two over C put
147 
148 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
149 X=[[0,1],[1,0]],       Z=[[1,0],[0,-1]].
150 \end{Verbatim}
151 
152 Then X²=Z²=I, XZ=-ZX, and {[}X,Z{]}=-I. The group generated by X and Z
153 has order 8 and is D8. Its refinement on V=F2² is
154 
155 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
156 q_D(x,y)=xy,       Arf(q_D)=0,
157 \end{Verbatim}
158 
159 with square table (+1,+1,+1,-1) at (0,e,f,e+f), and Gauss sum +2.
160 
161 The generators iX,iZ also anticommute, but each squares to -I and their
162 product also squares to -I. They generate Q8, with
163 
164 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
165 q_Q(x,y)=xy+x+y,   Arf(q_Q)=1,
166 \end{Verbatim}
167 
168 square table (+1,-1,-1,-1), and Gauss sum -2.
169 
170 Both C× pushouts identify with the same ambient matrix group
171 
172 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
173 P={z X^a Z^b : z in C×, a,b in {0,1}}.
174 \end{Verbatim}
175 
176 Nevertheless the marked subgroups
177 
178 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
179 H_D=<X,Z>,          H_Q=<iX,iZ>
180 \end{Verbatim}
181 
182 are different. No isomorphism fixing the two-element center can map H\_D
183 onto H\_Q: it would preserve q and hence the Arf invariant, which
184 differs. There is also no center-fixing automorphism of P carrying the
185 marked H\_D onto H\_Q. Their unmarked pushouts are isomorphic, but the
186 marked objects (P,H\_D) and (P,H\_Q) are not.
187 
188 Conversely a Q8 source embeds perfectly into the same P by sending its
189 generators to iX and iZ. This preserves every source square and its
190 negative Gauss sign. It does not identify those generators with the
191 independently marked D8 lifts X,Z. This is the distinction needed for
192 the arithmetic sector.
193 
194 \hypertarget{dyadic_markings-marked-scalar-pushout-attachment-with-c1}{%
195 \subsection{4. Marked scalar-pushout attachment with
196 C=\{1\}}\label{dyadic_markings-marked-scalar-pushout-attachment-with-c1}}
197 
198 Assume an actual type, its full character theta, and its Heisenberg
199 quotient W have already been constructed. Let P\_W be its actual C×
200 scalar pushout, acting on its actual Heisenberg representation eta\_W.
201 Let V\_src be a finite nondegenerate symplectic F2-space of dimension 2s,
202 with its complete supplied dyadic marked extension data. For several
203 breaks use their labeled orthogonal sum, balanced central product, and
204 supplied product refinement.
205 
206 Assume the following precise finite contract:
207 
208 \begin{enumerate}
209 \def\labelenumi{\arabic{enumi}.}
210 \tightlist
211 \item
212   The source full-character pushout P\_src has quotient V\_src and the
213   same represented scalar center as P\_W.
214 \item
215   The supplied finite central extensions and their marked lifts are
216   retained as subgroups/elements of P\_src, or as already specified maps
217   into P\_src. Any central character kernel already factored out must be recorded. A scalar pushout cannot recover invisible elements of that
218   kernel.
219 \item
220   The host has enough symplectic capacity, dim W\textgreater=2s, and the
221   new attachment into this host has no independently fixed conflicting
222   quadratic marking.
223 \item
224   The declared stabilizer is C=\{1\}, and the graph has one vertex.
225 \end{enumerate}
226 
227 Then a complete marked attachment exists in the \textbf{same actual
228 candidate}.
229 
230 \textbf{Proof.} Choose a symplectic embedding f:V\_src -\textgreater{} W
231 and let V be its image. The restriction P\_V of P\_W and P\_src have the
232 same commutator. Criterion (1) with center C× produces an isomorphism
233 
234 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
235 F:P_src -> P_V
236 \end{Verbatim}
237 
238 fixing every scalar and lifting f.~Carry every supplied finite subgroup
239 H\_src to the actual subgroup F(H\_src) of P\_V, and every marked lift a
240 to F(a). This operation does not erase square data:
241 
242 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
243 F(a)²=F(a²),        [F(a),F(b)]=F([a,b]).              (3)
244 \end{Verbatim}
245 
246 Since F fixes the scalar center, a²=(-1)\^{}q(v) implies
247 F(a)²=(-1)\^{}q(v). The transported refinement is therefore exactly q,
248 not a new choice with the same polar form. All marked section products,
249 specified extension maps, and finite group relations are preserved by
250 the same F. Consequently the Arf invariant and normalized Gauss sign are
251 unchanged.
252 
253 Every original h in a full character domain still maps to theta\_i(h),
254 because F fixes the entire scalar center. Thus the dyadic marking is
255 retained together with the full original character values.
256 
257 Write W=V perpendicular-sum U. Finite Stone--von Neumann gives
258 
259 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
260 eta_W isomorphic to eta_src tensor eta_U.
261 \end{Verbatim}
262 
263 Choose a line in eta\_U and its projector e. It lies in the actual
264 Heisenberg image algebra, and the marked source subgroup acts on e
265 eta\_W by precisely its supplied irreducible Heisenberg representation.
266 Its lift squares remain the operators in (3). The existing sector
267 recovery theorem then recovers the unchanged inducing representation
268 Lambda, and the same arithmetic candidate. There is no C-equivariance
269 equation to solve because C=\{1\}. QED.
270 
271 This realizes an actual finite marked subgroup in the scalar extension
272 of the actual type, with actual represented operators that are complex
273 scalars times type operators. It does not assert that every marked
274 source element is the image of an unscaled element of the old or new
275 arithmetic matrix group. That stronger requirement of a literal embedding is absent from the present contract.
276 
277 It also does not assert that the newly marked subgroup equals a
278 separately specified canonical native subgroup of the host. The marked
279 subgroup is part of the result and must be retained in the artifact.
280 Omitting it and recording only the unmarked P\_W would reproduce the
281 loss displayed by D8/Q8.
282 
283 \hypertarget{dyadic_markings-if-the-host-refinement-is-independently-fixed}{%
284 \subsection{5. If the host refinement is independently
285 fixed}\label{dyadic_markings-if-the-host-refinement-is-independently-fixed}}
286 
287 Suppose instead that the actual host arrives with a particular
288 nonsingular quadratic refinement q\_W and its actual finite mu\_2
289 central extension H\_W. An attachment into that marked extension
290 requires a quadratic isometric embedding, not merely a symplectic
291 embedding. There is a sharp capacity test.
292 
293 \textbf{Theorem.} Let dim V\_src=2s and dim W=2R. With embeddings
294 otherwise free, a quadratic isometric embedding
295 
296 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
297 (V_src,q_src) -> (W,q_W)
298 \end{Verbatim}
299 
300 exists if and only if R\textgreater=s and, in the equal-capacity case
301 R=s,
302 
303 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
304 Arf(q_src)=Arf(q_W).                                  (4)
305 \end{Verbatim}
306 
307 If R\textgreater s, either source Arf type embeds.
308 
309 \textbf{Proof.} Necessity of dimension is immediate. An
310 equal-dimensional embedding is an isometry, forcing (4). If
311 R\textgreater s, choose a nondegenerate quadratic space U of
312 dimension 2(R-s) with
313 
314 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
315 Arf(q_U)=Arf(q_W)+Arf(q_src).
316 \end{Verbatim}
317 
318 Both Arf types exist in every positive even dimension, by original
319 Proposition 13.7. The orthogonal sum V\_src perpendicular-sum U then has
320 the same dimension and Arf invariant as W. Original Standard Fact 13.4
321 gives an isometry to W. Restriction to V\_src gives the desired
322 embedding. QED.
323 
324 After this embedding is chosen, the preimage of its image in H\_W has
325 exactly q\_src. The criterion for a fixed two-element center in Section~2 gives
326 the extension isomorphism. Generating lifts with the specified squares
327 can be matched. Additional fully prescribed section elements still
328 require their exact product relations, as described in Section~2.
329 
330 Thus \textbf{one spare symplectic plane absorbs the Arf mismatch},
331 without changing the host's own refinement. This conclusion remains
332 conditional on the host's actual marked refinement/finite extension
333 being supplied or constructed. It does not manufacture a canonical
334 arithmetic quadratic datum from its dimension.
335 
336 For a preassigned embedding f, the missing equation is instead
337 
338 \begin{Verbatim}[fontsize=\small,breaklines=true,breakanywhere=true]
339 q_W(f(v))=q_src(v) for all v.                          (5)
340 \end{Verbatim}
341 
342 Its discrepancy q\_W composed with f minus q\_src is a linear
343 functional. Strict capacity allows a different quadratic embedding when it is free. It does not authorize replacing a fixed original map, fixed
344 depth placement, or fixed transport marking.
345 
346 \hypertarget{dyadic_markings-exact-outcome-for-the-dyadic-construction}{%
347 \subsection{6. Exact outcome for the dyadic
348 construction}\label{dyadic_markings-exact-outcome-for-the-dyadic-construction}}
349 
350 Under the retained one-vertex, C=\{1\}, full scalar-pushout realization
351 contract, an actual host with sufficient symplectic capacity does
352 support every supplied finite dyadic marking, provided the transported
353 finite subgroup, lifts, refinement, and phase are explicitly kept. The
354 proof is Section~4, rather than an assertion that commutators determine
355 the dyadic sign.
356 
357 If a particular host-native quadratic extension is fixed in advance, use
358 Section~5. Strict capacity suffices for its quadratic embedding. Equal capacity requires the Arf equation, and a preassigned embedding requires
359 (5). If only the type quotient is known and a specifically canonical
360 host quadratic datum is requested, constructing and comparing that datum
361 remains an arithmetic obligation. The scalar-pushout proof must not
362 silently claim to have done it.
363 
364 No part of this note handles nontrivial prescribed C actions. In that
365 case quadratic embedding, full extension action, lift markings, and
366 chosen honest phase operators must all be equivariant. Dimension and Arf equality alone do not settle those equations.
367 
368 \hypertarget{dyadic_markings-evidence-and-author-self-review}{%
369 \subsection{Evidence and author
370 self-review}\label{dyadic_markings-evidence-and-author-self-review}}
371 
372 Read directly: original Definition~11.1, Sections~13 and 15, and visual
373 appendix pages V--22/V--23 in the retained raw file; final Block166
374 \path{PROOF166.md}, Section~2, and \path{LEADING_LAYER_CAPACITY166.md}, Sections~2.1
375 and 4. The extension criterion and D8/Q8 calculation are complete finite
376 proofs. The quadratic embedding theorem uses the Arf classification
377 already explicitly supplied by the original paper. The sector conclusion
378 reuses the retained exact recovery theorem and does not assert new
379 arithmetic existence.
380 
381 Self-review checked that complex lift rescaling is never treated as an
382 automorphism changing squares within a fixed marked extension, that the
383 marked subgroup remains in the output, that preassigned maps differ from
384 freely chosen embeddings, and that fixed native refinements require
385 their own actual input. No independent review of this note or new Lean
386 execution is claimed here.

Back to source controls

Back to Realization Calculus