Machine-readable coverage register
Realization Boundaries
MONOGRAPH_COVERAGE.json
This is the original source text. Reading it does not run or verify the program.
1 [
2 {
3 "statement": "1.5",
4 "kind": "proposition",
5 "title": "Countable-code bound",
6 "label": "thm:codecount",
7 "chapter": "What a realization must supply",
8 "source": "publication/monograph_source/manuscript/chapters/01_contracts.tex",
9 "source_line": 35,
10 "printed_page": "2",
11 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
12 "lean_status": "COMPLETE",
13 "lean_declarations": [
14 "RealizationBoundaries.finite_description_outputs_countable",
15 "RealizationBoundaries.finite_description_cardinal_bound"
16 ],
17 "scope_note": "Arbitrary countable finite syntax, arbitrary validity, and single-valued semantics; actual semantic image is countable."
18 },
19 {
20 "statement": "1.8",
21 "kind": "theorem",
22 "title": "Reachability obstruction",
23 "label": "thm:reach",
24 "chapter": "What a realization must supply",
25 "source": "publication/monograph_source/manuscript/chapters/01_contracts.tex",
26 "source_line": 63,
27 "printed_page": "3",
28 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
29 "lean_status": "COMPLETE",
30 "lean_declarations": [
31 "RealizationBoundaries.operator_hull_reachable",
32 "RealizationBoundaries.unreachable_packet_obstructs",
33 "RealizationBoundaries.unreachable_packet_obstructs_topological",
34 "RealizationBoundaries.graphReach_iff_finite_path"
35 ],
36 "scope_note": "Actual dependent direct sum, vanishing transfer blocks, finite operator words, finite directed paths, and the omitted-packet closed-kernel consequence."
37 },
38 {
39 "statement": "2.1",
40 "kind": "theorem",
41 "title": "The torsion subgroup of the product",
42 "label": "thm:torP",
43 "chapter": "The squarefree ambient system",
44 "source": "publication/monograph_source/manuscript/chapters/02_ambient.tex",
45 "source_line": 35,
46 "printed_page": "5",
47 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
48 "lean_status": "COMPLETE",
49 "lean_declarations": [
50 "RealizationBoundaries.torsion_iff_finiteSupport",
51 "RealizationBoundaries.finiteSupport_dense",
52 "RealizationBoundaries.finiteSupport_ne_top"
53 ],
54 "scope_note": "The original finite-support subgroup is torsion, dense and proper in the actual unrestricted product."
55 },
56 {
57 "statement": "2.2",
58 "kind": "proposition",
59 "title": "Diagonal endomorphisms of the direct sum",
60 "label": "thm:endD",
61 "chapter": "The squarefree ambient system",
62 "source": "publication/monograph_source/manuscript/chapters/02_ambient.tex",
63 "source_line": 48,
64 "printed_page": "6",
65 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
66 "lean_status": "COMPLETE",
67 "lean_declarations": [
68 "RealizationBoundaries.finiteSupportEndomorphismRingEquiv",
69 "RealizationBoundaries.finiteSupportDiagonalRing_bijective",
70 "RealizationBoundaries.finiteSupport_endomorphism_coordinate",
71 "RealizationBoundaries.finiteSupport_endomorphism_preserves_zero"
72 ],
73 "scope_note": "The actual finite-support group D has endomorphism ring isomorphic to the full prime-coordinate product. All endomorphisms are derived to be diagonal, and zero-coordinate preservation is proved. Seed-rank cardinalities remain separate."
74 },
75 {
76 "statement": "2.3",
77 "kind": "corollary",
78 "title": "An infinite seed obstruction",
79 "label": "thm:rankD",
80 "chapter": "The squarefree ambient system",
81 "source": "publication/monograph_source/manuscript/chapters/02_ambient.tex",
82 "source_line": 60,
83 "printed_page": "6",
84 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
85 "lean_status": "COMPLETE",
86 "lean_declarations": [
87 "RealizationBoundaries.finiteSupport_seed_certificate",
88 "RealizationBoundaries.finiteSupport_no_finite_endomorphism_seeds",
89 "RealizationBoundaries.finiteSupport_no_finite_topological_seeds",
90 "RealizationBoundaries.finiteSupport_endomorphismSeedRank",
91 "RealizationBoundaries.finiteSupport_topologicalEndomorphismSeedRank"
92 ],
93 "scope_note": "Exact least cardinal aleph_0 for full-endomorphism algebraic generation. The closure in the actual induced topology has its own closed-coordinate obstruction and separately proved rank. The upper witness uses the checked countability of the actual group, not finite truncations."
94 },
95 {
96 "statement": "2.4",
97 "kind": "theorem",
98 "title": "Topological cyclicity",
99 "label": "thm:procyclic",
100 "chapter": "The squarefree ambient system",
101 "source": "publication/monograph_source/manuscript/chapters/02_ambient.tex",
102 "source_line": 70,
103 "printed_page": "6",
104 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
105 "lean_status": "COMPLETE",
106 "lean_declarations": [
107 "RealizationBoundaries.finite_coordinate_interpolation",
108 "RealizationBoundaries.ambient_cyclic_dense",
109 "RealizationBoundaries.ambient_topological_generator",
110 "RealizationBoundaries.ambient_ordinaryTopologicalRank"
111 ],
112 "scope_note": "An actual integer matches every finite prime-coordinate pattern by the finite Chinese remainder theorem. This proves density of the ordinary cyclic subgroup of the all-one vector in the genuine product topology. A nontrivial Hausdorff lower bound excludes rank zero, establishing exact ordinary topological rank one."
113 },
114 {
115 "statement": "2.5",
116 "kind": "proposition",
117 "title": "Profinite completion of the direct sum",
118 "label": "thm:Dcompletion",
119 "chapter": "The squarefree ambient system",
120 "source": "publication/monograph_source/manuscript/chapters/02_ambient.tex",
121 "source_line": 90,
122 "printed_page": "7",
123 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
124 "lean_status": "COMPLETE",
125 "lean_declarations": [
126 "RealizationBoundaries.finiteSupportCompletionEquiv",
127 "RealizationBoundaries.finiteSupportCompletionEquiv_eta"
128 ],
129 "scope_note": "Topological additive equivalence from Mathlib's actual all-finite-quotients completion of D to P, respecting the canonical map."
130 },
131 {
132 "statement": "2.6",
133 "kind": "theorem",
134 "title": "Unique division in the ambient quotient",
135 "label": "thm:Vrational",
136 "chapter": "The squarefree ambient system",
137 "source": "publication/monograph_source/manuscript/chapters/02_ambient.tex",
138 "source_line": 102,
139 "printed_page": "8",
140 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
141 "lean_status": "COMPLETE",
142 "lean_declarations": [
143 "RealizationBoundaries.tail_nsmul_bijective",
144 "RealizationBoundaries.tail_rational_module_unique",
145 "RealizationBoundaries.hom_zero_of_divisible",
146 "RealizationBoundaries.not_injective_hom_of_divisible"
147 ],
148 "scope_note": "The full printed assertion is algebraic and already checked: actual quotient, unique rational module and no nonzero divisible subgroup of the product. Historic COMPLETE_ALGEBRAIC label normalized after exact-statement review."
149 },
150 {
151 "statement": "3.1",
152 "kind": "theorem",
153 "title": "Subgroup and isomorphism classification",
154 "label": "thm:subD",
155 "chapter": "Prime spectra and finite descriptions",
156 "source": "publication/monograph_source/manuscript/chapters/03_spectrum.tex",
157 "source_line": 12,
158 "printed_page": "9",
159 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
160 "lean_status": "COMPLETE",
161 "lean_declarations": [
162 "RealizationBoundaries.subgroupSpectrumOrderIso",
163 "RealizationBoundaries.finiteSupport_subgroup_fullyInvariant",
164 "RealizationBoundaries.spectrumSubgroup_isomorphic_iff",
165 "RealizationBoundaries.subgroupCantorHomeomorph",
166 "RealizationBoundaries.natSubgroupCantorHomeomorph"
167 ],
168 "scope_note": "Actual subgroup classification and intrinsic prime torsion; literal lattice operations; independently induced membership topology and Cantor homeomorphism."
169 },
170 {
171 "statement": "3.2",
172 "kind": "corollary",
173 "title": "Finite observations leave continuum many possibilities",
174 "label": "thm:finiteviews",
175 "chapter": "Prime spectra and finite descriptions",
176 "source": "publication/monograph_source/manuscript/chapters/03_spectrum.tex",
177 "source_line": 33,
178 "printed_page": "10",
179 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
180 "lean_status": "COMPLETE",
181 "lean_declarations": [
182 "RealizationBoundaries.spectrumObservationFiber_card",
183 "RealizationBoundaries.spectrumObservation_not_isomorphic",
184 "RealizationBoundaries.compatible_spectrum_patterns_exists_unique"
185 ],
186 "scope_note": "Exact continuum cardinality after every finite observation, pairwise abstract nonisomorphism, and existence plus uniqueness from coherent finite patterns."
187 },
188 {
189 "statement": "3.3",
190 "kind": "theorem",
191 "title": "The prime-spectrum criterion",
192 "label": "thm:spectrumce",
193 "chapter": "Prime spectra and finite descriptions",
194 "source": "publication/monograph_source/manuscript/chapters/03_spectrum.tex",
195 "source_line": 44,
196 "printed_page": "10",
197 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
198 "lean_status": "COMPLETE",
199 "lean_declarations": [
200 "RealizationBoundaries.oracle_spectrum_copy_iff_stageListing",
201 "RealizationBoundaries.oracle_spectrum_copy_iff_enumerable",
202 "RealizationBoundaries.oracleEnumerable_iff_stageListing"
203 ],
204 "scope_note": "Full finite-or-infinite copy convention; actual native oracle-computable stage listings, positive witness tests and partial-recursive domains are proved equivalent."
205 },
206 {
207 "statement": "3.4",
208 "kind": "corollary",
209 "title": "",
210 "label": "thm:noncompD",
211 "chapter": "Prime spectra and finite descriptions",
212 "source": "publication/monograph_source/manuscript/chapters/03_spectrum.tex",
213 "source_line": 72,
214 "printed_page": "11",
215 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
216 "lean_status": "COMPLETE",
217 "lean_declarations": [
218 "RealizationBoundaries.haltingSpectrum_no_any_computable_copy",
219 "RealizationBoundaries.haltingGroup_prime_order_presentation",
220 "RealizationBoundaries.computable_primeOrderRelatorLabel",
221 "RealizationBoundaries.primrec_haltingRelatorIndexStage",
222 "RealizationBoundaries.haltingRelatorIndexStage_exact"
223 ],
224 "scope_note": "Actual diagonal halting complement, no finite or infinite computable copy, native relator enumeration and the universal commuting prime-order presentation of the actual quotient."
225 },
226 {
227 "statement": "3.5",
228 "kind": "theorem",
229 "title": "Unary selector classification",
230 "label": "thm:unary",
231 "chapter": "Prime spectra and finite descriptions",
232 "source": "publication/monograph_source/manuscript/chapters/03_spectrum.tex",
233 "source_line": 86,
234 "printed_page": "11",
235 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
236 "lean_status": "COMPLETE",
237 "lean_declarations": [
238 "RealizationBoundaries.unary_selector_classification",
239 "RealizationBoundaries.unaryRecognizable_iff_ultimatelyPeriodic"
240 ],
241 "scope_note": "Genuine finite unary automata and both directions of ultimate periodicity; actual prime-spectrum abstract isomorphism criterion."
242 },
243 {
244 "statement": "4.2",
245 "kind": "theorem",
246 "title": "Pure-preimage correspondence",
247 "label": "thm:purecorrespondence",
248 "chapter": "Pure preimages and common finite observations",
249 "source": "publication/monograph_source/manuscript/chapters/04_purity.tex",
250 "source_line": 23,
251 "printed_page": "13",
252 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
253 "lean_status": "COMPLETE",
254 "lean_declarations": [
255 "RealizationBoundaries.IsPure",
256 "RealizationBoundaries.pure_root_closed",
257 "RealizationBoundaries.rationalImage",
258 "RealizationBoundaries.purePreimageOrderIso",
259 "RealizationBoundaries.exists_unique_rational_preimage"
260 ],
261 "scope_note": "Both directions, both inverse laws and order reflection are checked. Purity is root lifting in P; inclusion of D is explicit."
262 },
263 {
264 "statement": "4.3",
265 "kind": "theorem",
266 "title": "Ambient root criterion",
267 "label": "thm:ambientroot",
268 "chapter": "Pure preimages and common finite observations",
269 "source": "publication/monograph_source/manuscript/chapters/04_purity.tex",
270 "source_line": 41,
271 "printed_page": "14",
272 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
273 "lean_status": "COMPLETE",
274 "lean_declarations": [
275 "RealizationBoundaries.ambient_root_iff",
276 "RealizationBoundaries.preimage_root_iff"
277 ],
278 "scope_note": "Both directions for every positive multiplier and every actual preimage."
279 },
280 {
281 "statement": "4.4",
282 "kind": "theorem",
283 "title": "One finite-quotient system for every preimage",
284 "label": "thm:generalquotients",
285 "chapter": "Pure preimages and common finite observations",
286 "source": "publication/monograph_source/manuscript/chapters/04_purity.tex",
287 "source_line": 54,
288 "printed_page": "14",
289 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
290 "lean_status": "COMPLETE",
291 "lean_declarations": [
292 "RealizationBoundaries.integerQuotientEquiv",
293 "RealizationBoundaries.integerQuotientEquiv_mk",
294 "RealizationBoundaries.coordinateRestriction_map",
295 "RealizationBoundaries.finite_target_coordinate_kernel",
296 "RealizationBoundaries.profiniteCompletionEquiv",
297 "RealizationBoundaries.profiniteCompletionEquiv_eta"
298 ],
299 "scope_note": "Canonical integer quotients, coordinate transitions, finite-target cofinal kernels and the actual profinite completion are checked."
300 },
301 {
302 "statement": "4.5",
303 "kind": "proposition",
304 "title": "Finite-target equivalence",
305 "label": "thm:finitehom",
306 "chapter": "Pure preimages and common finite observations",
307 "source": "publication/monograph_source/manuscript/chapters/04_purity.tex",
308 "source_line": 72,
309 "printed_page": "15",
310 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
311 "lean_status": "COMPLETE",
312 "lean_declarations": [
313 "RealizationBoundaries.finiteSupportRestrictionEquiv",
314 "RealizationBoundaries.finiteSupportRestrictionEquiv_apply",
315 "RealizationBoundaries.finiteSupportRestrictionEquiv_natural"
316 ],
317 "scope_note": "An equivalence between Hom(H_W,F) and Hom(D,F) for every finite additive-group target. Its forward map is the literal restriction, and naturality under target homomorphisms is proved."
318 },
319 {
320 "statement": "4.6",
321 "kind": "proposition",
322 "title": "Structure of an ambient preimage",
323 "label": "thm:HWstructure",
324 "chapter": "Pure preimages and common finite observations",
325 "source": "publication/monograph_source/manuscript/chapters/04_purity.tex",
326 "source_line": 87,
327 "printed_page": "15",
328 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
329 "lean_status": "COMPLETE",
330 "lean_declarations": [
331 "RealizationBoundaries.preimage_countable_iff_rational_rank",
332 "RealizationBoundaries.preimage_countable_iff_dimension_finite_or_countably_infinite"
333 ],
334 "scope_note": "Adds the exact rational dimension formulation, including zero and finite dimension, to all preserved structural conclusions."
335 },
336 {
337 "statement": "5.1",
338 "kind": "theorem",
339 "title": "Unique normal form",
340 "label": "thm:normalform",
341 "chapter": "The paired-prime groups",
342 "source": "publication/monograph_source/manuscript/chapters/05_construction.tex",
343 "source_line": 44,
344 "printed_page": "18",
345 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
346 "lean_status": "COMPLETE",
347 "lean_declarations": [
348 "RealizationBoundaries.normalForm_exists",
349 "RealizationBoundaries.normalForm_unique",
350 "RealizationBoundaries.normalFormEquiv",
351 "RealizationBoundaries.paired_countably_infinite",
352 "RealizationBoundaries.NormalForm.pairEquiv",
353 "RealizationBoundaries.pairedNormalFormEquiv"
354 ],
355 "scope_note": "Existence, uniqueness, the selector-independent Q x D domain and countable infinitude of every paired group are now checked."
356 },
357 {
358 "statement": "5.2",
359 "kind": "lemma",
360 "title": "A finite support bound",
361 "label": "thm:cocyclesupport",
362 "chapter": "The paired-prime groups",
363 "source": "publication/monograph_source/manuscript/chapters/05_construction.tex",
364 "source_line": 64,
365 "printed_page": "18",
366 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
367 "lean_status": "COMPLETE",
368 "lean_declarations": [
369 "RealizationBoundaries.sectionDefect_support",
370 "RealizationBoundaries.sectionDefect_finite"
371 ],
372 "scope_note": "The actual infinite-coordinate defect is supported on denominator primes."
373 },
374 {
375 "statement": "5.3",
376 "kind": "theorem",
377 "title": "Explicit group law",
378 "label": "thm:cocyclelaw",
379 "chapter": "The paired-prime groups",
380 "source": "publication/monograph_source/manuscript/chapters/05_construction.tex",
381 "source_line": 76,
382 "printed_page": "19",
383 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
384 "lean_status": "COMPLETE",
385 "lean_declarations": [
386 "RealizationBoundaries.cocycle_identity",
387 "RealizationBoundaries.normalAdd_assoc",
388 "RealizationBoundaries.normalAdd_comm",
389 "RealizationBoundaries.normalAdd_zero",
390 "RealizationBoundaries.normalAdd_inverse",
391 "RealizationBoundaries.NormalForm.realizationEquiv"
392 ],
393 "scope_note": "Separate twisted group type, all additive group laws, and actual additive equivalence to the preimage."
394 },
395 {
396 "statement": "5.4",
397 "kind": "proposition",
398 "title": "One cocycle value reads one coordinate",
399 "label": "thm:cocyclebit",
400 "chapter": "The paired-prime groups",
401 "source": "publication/monograph_source/manuscript/chapters/05_construction.tex",
402 "source_line": 96,
403 "printed_page": "19",
404 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
405 "lean_status": "COMPLETE",
406 "lean_declarations": [
407 "RealizationBoundaries.cocycle_reads_coordinate",
408 "RealizationBoundaries.cocycle_coordinate_nonzero_iff"
409 ],
410 "scope_note": "Literal finite-support equality for the printed cocycle value, plus exact coordinate recovery."
411 },
412 {
413 "statement": "5.5",
414 "kind": "proposition",
415 "title": "Finitely generated subgroups",
416 "label": "thm:fgsubgroups",
417 "chapter": "The paired-prime groups",
418 "source": "publication/monograph_source/manuscript/chapters/05_construction.tex",
419 "source_line": 123,
420 "printed_page": "20",
421 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
422 "lean_status": "COMPLETE",
423 "lean_declarations": [
424 "RealizationBoundaries.paired_fg_subgroup_classification",
425 "RealizationBoundaries.rational_subgroup_fg_isAddCyclic"
426 ],
427 "scope_note": "Every actual FG subgroup is squarefree finite cyclic or Z times a squarefree finite cyclic group; no splitting hypothesis is assumed."
428 },
429 {
430 "statement": "6.1",
431 "kind": "theorem",
432 "title": "Root or obstruction",
433 "label": "thm:rootcertificate",
434 "chapter": "Root certificates and finite quotients",
435 "source": "publication/monograph_source/manuscript/chapters/06_roots.tex",
436 "source_line": 14,
437 "printed_page": "21",
438 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
439 "lean_status": "COMPLETE",
440 "lean_declarations": [
441 "RealizationBoundaries.finite_root_algorithm_correct",
442 "RealizationBoundaries.codedNormalValue_represents",
443 "RealizationBoundaries.certifiedRootSolver_error",
444 "RealizationBoundaries.certifiedRootSolver_ok",
445 "RealizationBoundaries.finiteRootSolver_complete",
446 "RealizationBoundaries.finiteRootSolver_support_bound",
447 "RealizationBoundaries.countedCertifiedRootSolver_erase",
448 "RealizationBoundaries.countedCertifiedRootSolver_step_bound",
449 "RealizationBoundaries.countedCertifiedRootSolver_query_bound"
450 ],
451 "scope_note": "For positive multipliers and supplied rational/finite codes: executable root solver, returned prime obstruction, coverage of every original normal form, exact ambient extraction, support and instrumented oracle/loop bounds. No bit-cost or Python kernel-verification claim."
452 },
453 {
454 "statement": "6.2",
455 "kind": "proposition",
456 "title": "All roots and their number",
457 "label": "thm:rootfiber",
458 "chapter": "Root certificates and finite quotients",
459 "source": "publication/monograph_source/manuscript/chapters/06_roots.tex",
460 "source_line": 40,
461 "printed_page": "22",
462 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
463 "lean_status": "COMPLETE",
464 "lean_declarations": [
465 "RealizationBoundaries.RootFiber",
466 "RealizationBoundaries.rootKernelEquiv",
467 "RealizationBoundaries.rootFiberTranslation",
468 "RealizationBoundaries.rootFiber_coset_iff",
469 "RealizationBoundaries.rootFiberEquiv",
470 "RealizationBoundaries.rootFiberEquiv_symm_apply",
471 "RealizationBoundaries.rootFiber_finite",
472 "RealizationBoundaries.rootKernel_card",
473 "RealizationBoundaries.rootFiber_card_of_solvable",
474 "RealizationBoundaries.rootFiber_card",
475 "RealizationBoundaries.prime_power_root_count"
476 ],
477 "scope_note": "Actual fibers and integer-torsion kernels are constructed for every rational preimage H_W. Translation by a supplied root gives the exact coset parametrization. An explicit additive equivalence identifies the kernel with the divisor-coordinate product, and the positive-multiplier fiber is proved finite with radical cardinality when nonempty and zero when obstructed. Prime powers and multiplier one are retained; multiplier zero is separately proved infinite at zero."
478 },
479 {
480 "statement": "6.3",
481 "kind": "theorem",
482 "title": "All integer quotients",
483 "label": "thm:quotientformula",
484 "chapter": "Root certificates and finite quotients",
485 "source": "publication/monograph_source/manuscript/chapters/06_roots.tex",
486 "source_line": 55,
487 "printed_page": "22",
488 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
489 "lean_status": "COMPLETE",
490 "lean_declarations": [
491 "RealizationBoundaries.integerQuotientEquiv",
492 "RealizationBoundaries.divisorCrtEquiv",
493 "RealizationBoundaries.cyclicIntegerQuotientEquiv",
494 "RealizationBoundaries.cyclicIntegerQuotientEquiv_mk",
495 "RealizationBoundaries.quotientRestriction",
496 "RealizationBoundaries.integerQuotientEquiv_restriction",
497 "RealizationBoundaries.cyclicIntegerQuotientEquiv_restriction",
498 "RealizationBoundaries.multiples_eq_radical",
499 "RealizationBoundaries.finite_quotient_exists_iff",
500 "RealizationBoundaries.finite_surjection_ker"
501 ],
502 "scope_note": "The actual quotient by m H_W is additively equivalent to ZMod(rad m), with the representative formula and quotient transitions commuting with canonical residue reduction. The multiples equal the radical multiples as literal subgroups. Every finite quotient is cyclic and squarefree, every finite cyclic squarefree target is achieved by an actual surjection, and its kernel is the literal target-order multiple subgroup."
503 },
504 {
505 "statement": "6.4",
506 "kind": "corollary",
507 "title": "Common profinite completion",
508 "label": "thm:GAcompletion",
509 "chapter": "Root certificates and finite quotients",
510 "source": "publication/monograph_source/manuscript/chapters/06_roots.tex",
511 "source_line": 96,
512 "printed_page": "23",
513 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
514 "lean_status": "COMPLETE",
515 "lean_declarations": [
516 "RealizationBoundaries.pairedCompletionEquiv",
517 "RealizationBoundaries.profiniteCompletionEquiv_eta",
518 "RealizationBoundaries.completion_eta_isEmbedding",
519 "RealizationBoundaries.fullProfiniteTopology_eq"
520 ],
521 "scope_note": "Every paired group has the actual canonical profinite completion P. Its induced product topology equals the full topology induced from the limit of all finite quotients."
522 },
523 {
524 "statement": "7.1",
525 "kind": "lemma",
526 "title": "Tail signature",
527 "label": "thm:tailsignature",
528 "chapter": "Classification, morphisms, and seed rank",
529 "source": "publication/monograph_source/manuscript/chapters/07_classification.tex",
530 "source_line": 8,
531 "printed_page": "25",
532 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
533 "lean_status": "COMPLETE",
534 "lean_declarations": [
535 "RealizationBoundaries.tailExceptions_finite",
536 "RealizationBoundaries.normalForm_coordinate_ne_zero_iff",
537 "RealizationBoundaries.selector_tail_signature"
538 ],
539 "scope_note": "Every nontorsion element of the actual selector group has the eventual prime-root signature. The exception set explicitly includes primes dividing the numerator absolute value, denominator primes, and the finite correction support. No all-prime conclusion is substituted."
540 },
541 {
542 "statement": "7.2",
543 "kind": "theorem",
544 "title": "Unmarked isomorphism classification",
545 "label": "thm:isoclass",
546 "chapter": "Classification, morphisms, and seed rank",
547 "source": "publication/monograph_source/manuscript/chapters/07_classification.tex",
548 "source_line": 22,
549 "printed_page": "25",
550 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
551 "lean_status": "COMPLETE",
552 "lean_declarations": [
553 "RealizationBoundaries.pairedGroup_isomorphic_iff",
554 "RealizationBoundaries.pairedGroup_eq_of_finite_disagreement",
555 "RealizationBoundaries.pairedEquivOfFiniteDisagreement_val",
556 "RealizationBoundaries.normalFormTransportEquiv_apply",
557 "RealizationBoundaries.normalFormTransport_add"
558 ],
559 "scope_note": "Both directions of the unmarked classification are checked. Finite bit disagreement gives literal ambient subgroup equality, a point-preserving AddEquiv, and the exact rational-section finite-correction coordinate transport respecting twisted addition. The conclusion is finite disagreement, not literal selector equality."
560 },
561 {
562 "statement": "7.3",
563 "kind": "corollary",
564 "title": "Marked classification",
565 "label": "thm:markedclass",
566 "chapter": "Classification, morphisms, and seed rank",
567 "source": "publication/monograph_source/manuscript/chapters/07_classification.tex",
568 "source_line": 43,
569 "printed_page": "26",
570 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
571 "lean_status": "COMPLETE",
572 "lean_declarations": [
573 "RealizationBoundaries.selectors_equal_of_markedEquiv",
574 "RealizationBoundaries.pairedGroup_marked_isomorphic_iff",
575 "RealizationBoundaries.toggleBit_not_marked_isomorphic"
576 ],
577 "scope_note": "An additive equivalence carrying the specified indicator to the other specified indicator exists exactly when every selector bit agrees. A one-bit toggle gives the same unmarked group but no such marked isomorphism."
578 },
579 {
580 "statement": "7.5",
581 "kind": "theorem",
582 "title": "Complete homomorphism description",
583 "label": "thm:allhom",
584 "chapter": "Classification, morphisms, and seed rank",
585 "source": "publication/monograph_source/manuscript/chapters/07_classification.tex",
586 "source_line": 58,
587 "printed_page": "26",
588 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
589 "lean_status": "COMPLETE",
590 "lean_declarations": [
591 "RealizationBoundaries.hom_coordinate_formula",
592 "RealizationBoundaries.homDiagonal_unique",
593 "RealizationBoundaries.diagonalHomEquiv",
594 "RealizationBoundaries.diagonalTail",
595 "RealizationBoundaries.diagonalAdmissible_selector_iff",
596 "RealizationBoundaries.diagonalAdmissible_iff_finite_defect",
597 "RealizationBoundaries.selectorHomEquiv",
598 "RealizationBoundaries.preimage_hom_continuous",
599 "RealizationBoundaries.completionHom_coordinates"
600 ],
601 "scope_note": "Every actual additive homomorphism is proved diagonal without continuity or diagonal hypotheses. The exact converse, finite-defect condition, automatic continuity, and its full-completion coordinate action are checked. The diagonal formula holds for all rational preimages H_W, not only paired selector groups."
602 },
603 {
604 "statement": "7.6",
605 "kind": "theorem",
606 "title": "Torsion-image obstruction",
607 "label": "thm:homobstruction",
608 "chapter": "Classification, morphisms, and seed rank",
609 "source": "publication/monograph_source/manuscript/chapters/07_classification.tex",
610 "source_line": 78,
611 "printed_page": "27",
612 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
613 "lean_status": "COMPLETE",
614 "lean_declarations": [
615 "RealizationBoundaries.finite_disagreement_of_nontorsion_image",
616 "RealizationBoundaries.hom_image_finiteSupport",
617 "RealizationBoundaries.hom_image_torsion",
618 "RealizationBoundaries.torsionFactor_commutes",
619 "RealizationBoundaries.torsionFactor_unique",
620 "RealizationBoundaries.no_injective_hom_of_infinite_disagreement",
621 "RealizationBoundaries.no_surjective_hom_of_infinite_disagreement",
622 "RealizationBoundaries.pairedGroup_embeds_iff",
623 "RealizationBoundaries.pairedGroup_surjects_iff"
624 ],
625 "scope_note": "Arbitrary additive homomorphisms, with no continuity or diagonality hypothesis, have torsion image when selectors disagree infinitely. Every map factors uniquely through the actual D, and injective or surjective maps exist exactly at finite disagreement. A nonzero coordinate map is proved in the positive suite, guarding against a false zero-image conclusion."
626 },
627 {
628 "statement": "7.7",
629 "kind": "corollary",
630 "title": "Endomorphism ring",
631 "label": "thm:endGA",
632 "chapter": "Classification, morphisms, and seed rank",
633 "source": "publication/monograph_source/manuscript/chapters/07_classification.tex",
634 "source_line": 94,
635 "printed_page": "27",
636 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
637 "lean_status": "COMPLETE",
638 "lean_declarations": [
639 "RealizationBoundaries.endomorphismRingEquiv",
640 "RealizationBoundaries.diagonalEndRing_mem_iff",
641 "RealizationBoundaries.diagonalSlope_unique",
642 "RealizationBoundaries.diagonalSlope_eq_of_finite_defect",
643 "RealizationBoundaries.quotientScalar",
644 "RealizationBoundaries.quotientScalar_surjective",
645 "RealizationBoundaries.quotientScalar_eq_zero_iff",
646 "RealizationBoundaries.endomorphismQuotientScalar",
647 "RealizationBoundaries.endomorphismQuotientScalar_surjective"
648 ],
649 "scope_note": "The actual endomorphism ring is identified as the admissible diagonal subring, with the eventual-rational selected-coordinate characterization. Infinite selector support makes the rational quotient scalar unique. Ring laws, surjectivity and the exact zero-scalar kernel are proved. Denominator primes remain in the permitted finite exceptional set. The chosen lifts are not claimed to form a homomorphic section."
650 },
651 {
652 "statement": "7.8",
653 "kind": "corollary",
654 "title": "Automorphisms",
655 "label": "thm:autGA",
656 "chapter": "Classification, morphisms, and seed rank",
657 "source": "publication/monograph_source/manuscript/chapters/07_classification.tex",
658 "source_line": 111,
659 "printed_page": "28",
660 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
661 "lean_status": "COMPLETE",
662 "lean_declarations": [
663 "RealizationBoundaries.hom_injective_iff_diagonal_nonzero",
664 "RealizationBoundaries.diagonalSlope_ne_zero",
665 "RealizationBoundaries.inverseDiagonal_admissible",
666 "RealizationBoundaries.selectorEquivOfNonzeroDiagonal",
667 "RealizationBoundaries.selectorEquiv_inverse_coordinate",
668 "RealizationBoundaries.selector_endomorphism_automorphism_iff",
669 "RealizationBoundaries.selector_hom_bijective_iff"
670 ],
671 "scope_note": "The automorphism criterion requires every prime-coordinate scalar to be nonzero. The inverse multiplier is proved to preserve the original rank-one groups, the quotient scalar is proved nonzero, and the actual inverse formula is checked. Product invertibility is not assumed to imply invertibility on arbitrary rational-subspace preimages."
672 },
673 {
674 "statement": "7.9",
675 "kind": "theorem",
676 "title": "Seed-rank separation",
677 "label": "thm:rankGA",
678 "chapter": "Classification, morphisms, and seed rank",
679 "source": "publication/monograph_source/manuscript/chapters/07_classification.tex",
680 "source_line": 120,
681 "printed_page": "28",
682 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
683 "lean_status": "COMPLETE",
684 "lean_declarations": [
685 "RealizationBoundaries.selector_outside_support_finite",
686 "RealizationBoundaries.paired_seed_certificate",
687 "RealizationBoundaries.paired_endomorphismSeedRank",
688 "RealizationBoundaries.paired_topologicalEndomorphismSeedRank",
689 "RealizationBoundaries.paired_ordinaryTopologicalRank",
690 "RealizationBoundaries.completionGenerator_generates",
691 "RealizationBoundaries.canonicalCompletion_ordinaryTopologicalRank",
692 "RealizationBoundaries.paired_seed_rank_separation"
693 ],
694 "scope_note": "For every binary selector: exact algebraic full-endomorphism rank aleph_0, no finite topological operator family, and exact ordinary topological rank aleph_0 in the original group. The actual canonical completion has a named topological generator and ordinary topological rank one. These contracts are defined separately and proved together in the final bundled theorem."
695 },
696 {
697 "statement": "8.1",
698 "kind": "proposition",
699 "title": "Uniform construction relative to the selector",
700 "label": "thm:computeupper",
701 "chapter": "The exact cost of an effective realization",
702 "source": "publication/monograph_source/manuscript/chapters/08_computability.tex",
703 "source_line": 15,
704 "printed_page": "29",
705 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
706 "lean_status": "COMPLETE",
707 "lean_declarations": [
708 "RealizationBoundaries.pairedOracleCopy",
709 "RealizationBoundaries.canonicalPairedAddition_oracle_iff",
710 "RealizationBoundaries.canonicalPairedAddition_graph_equivalent",
711 "RealizationBoundaries.localNormalAdd_correct",
712 "RealizationBoundaries.localNormalAdd_loop_oracleComputable",
713 "RealizationBoundaries.localCocycleQuerySchedule_mem",
714 "RealizationBoundaries.localCocycleQuerySchedule_nodup"
715 ],
716 "scope_note": "Actual native oracle construction with decidable semantic equality and bijective natural names; the fixed canonical addition graph has exactly the selector degree. Optimized addition queries only denominator primes once per prime."
717 },
718 {
719 "statement": "8.2",
720 "kind": "proposition",
721 "title": "Uniform marked decoding",
722 "label": "thm:markeddecode",
723 "chapter": "The exact cost of an effective realization",
724 "source": "publication/monograph_source/manuscript/chapters/08_computability.tex",
725 "source_line": 27,
726 "printed_page": "30",
727 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
728 "lean_status": "COMPLETE",
729 "lean_declarations": [
730 "RealizationBoundaries.oracle_marked_copy_reduces",
731 "RealizationBoundaries.marked_root_presentation_reduces"
732 ],
733 "scope_note": "Actual addition algorithm, computed integer multiples and terminating complementary positive searches with a supplied marker name."
734 },
735 {
736 "statement": "8.3",
737 "kind": "theorem",
738 "title": "Exact oracle criterion",
739 "label": "thm:degree",
740 "chapter": "The exact cost of an effective realization",
741 "source": "publication/monograph_source/manuscript/chapters/08_computability.tex",
742 "source_line": 47,
743 "printed_page": "30",
744 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
745 "lean_status": "COMPLETE",
746 "lean_declarations": [
747 "RealizationBoundaries.paired_oracle_copy_iff",
748 "RealizationBoundaries.paired_least_presentation_degree"
749 ],
750 "scope_note": "Both oracle directions and an attained least presentation degree. The unmarked reduction nonuniformly hard-codes a finite natural name of the actual marker; no uniform marker finder is asserted."
751 },
752 {
753 "statement": "8.4",
754 "kind": "corollary",
755 "title": "Degree variation with fixed observations",
756 "label": "thm:alldegrees",
757 "chapter": "The exact cost of an effective realization",
758 "source": "publication/monograph_source/manuscript/chapters/08_computability.tex",
759 "source_line": 74,
760 "printed_page": "31",
761 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
762 "lean_status": "COMPLETE",
763 "lean_declarations": [
764 "RealizationBoundaries.every_set_degree_with_fixed_computable_observation",
765 "RealizationBoundaries.paired_isReduced",
766 "RealizationBoundaries.allFiniteObservation_fixed_computable",
767 "RealizationBoundaries.computableObservationQuotientIso"
768 ],
769 "scope_note": "Every usual Turing degree of a set, actual reduced countable residually finite abelian groups, common canonical completion, and one fixed native and runnable finite quotient diagram with certified cofinal comparison."
770 },
771 {
772 "statement": "9.1",
773 "kind": "theorem",
774 "title": "No decoder from the unmarked finite-quotient system",
775 "label": "thm:nodecoder",
776 "chapter": "What finite observations cannot reconstruct",
777 "source": "publication/monograph_source/manuscript/chapters/09_reconstruction.tex",
778 "source_line": 14,
779 "printed_page": "33",
780 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
781 "lean_status": "COMPLETE",
782 "lean_declarations": [
783 "RealizationBoundaries.coordinateIndexFunctor_initial",
784 "RealizationBoundaries.coordinateObservationIso",
785 "RealizationBoundaries.no_unmarked_observation_decoder"
786 ],
787 "scope_note": "Actual all-finite-quotient diagrams and source-free cofinal natural comparisons. Arbitrary invariant decoders are impossible; no completion-only surrogate or computability assumption."
788 },
789 {
790 "statement": "9.2",
791 "kind": "proposition",
792 "title": "A proper map invisible after completion",
793 "label": "thm:propercompletion",
794 "chapter": "What finite observations cannot reconstruct",
795 "source": "publication/monograph_source/manuscript/chapters/09_reconstruction.tex",
796 "source_line": 43,
797 "printed_page": "34",
798 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
799 "lean_status": "COMPLETE",
800 "lean_declarations": [
801 "RealizationBoundaries.finiteSupport_inclusion_not_surjective",
802 "RealizationBoundaries.finiteSupportToPairedCompletion",
803 "RealizationBoundaries.finiteSupportToPairedCompletion_eta"
804 ],
805 "scope_note": "The literal inclusion D to G_a is not surjective. Its extension to their actual completions is a topological additive isomorphism, with equality on every canonical D point."
806 },
807 {
808 "statement": "9.3",
809 "kind": "proposition",
810 "title": "Faithfulness and failure of fullness",
811 "label": "thm:faithful",
812 "chapter": "What finite observations cannot reconstruct",
813 "source": "publication/monograph_source/manuscript/chapters/09_reconstruction.tex",
814 "source_line": 55,
815 "printed_page": "35",
816 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
817 "lean_status": "COMPLETE",
818 "lean_declarations": [
819 "RealizationBoundaries.official_completion_map_injective",
820 "RealizationBoundaries.residuallyFiniteCompletion_faithful",
821 "RealizationBoundaries.pairedCompletionFunctor_not_full",
822 "RealizationBoundaries.boundaryCompletionFunctor_not_reflects_isomorphisms"
823 ],
824 "scope_note": "Official global multiplicative completion functor is faithful on all residually finite groups; actual paired category is not full; enlarged category containing D fails to reflect isomorphisms."
825 },
826 {
827 "statement": "9.4",
828 "kind": "proposition",
829 "title": "Reflection within the paired-prime family",
830 "label": "thm:rankonereflection",
831 "chapter": "What finite observations cannot reconstruct",
832 "source": "publication/monograph_source/manuscript/chapters/09_reconstruction.tex",
833 "source_line": 66,
834 "printed_page": "35",
835 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
836 "lean_status": "COMPLETE",
837 "lean_declarations": [
838 "RealizationBoundaries.completionHom",
839 "RealizationBoundaries.completionHom_eta",
840 "RealizationBoundaries.completionHom_unique",
841 "RealizationBoundaries.completionHom_comp",
842 "RealizationBoundaries.completionHom_isomorphism_iff",
843 "RealizationBoundaries.selector_completion_reflection",
844 "RealizationBoundaries.paired_completion_reflects_isomorphisms"
845 ],
846 "scope_note": "For a supplied homomorphism between paired-prime groups, its actual induced map on canonical profinite completions is a continuous additive isomorphism exactly when the supplied original map is an additive isomorphism. The extension is constructed and identified by its eta equation and uniqueness, not by an assumed diagonal formula or an unavailable additive functor API. This does not reconstruct an unknown source from its completion."
847 },
848 {
849 "statement": "10.1",
850 "kind": "theorem",
851 "title": "Escape within one profinite-completion class",
852 "label": "thm:escape",
853 "chapter": "Escaping a fixed finite grammar",
854 "source": "publication/monograph_source/manuscript/chapters/10_grammar.tex",
855 "source_line": 26,
856 "printed_page": "37",
857 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
858 "lean_status": "COMPLETE",
859 "lean_declarations": [
860 "RealizationBoundaries.countableGrammarEscape_not_output",
861 "RealizationBoundaries.countableGrammarEscape_pairwise_nonisomorphic",
862 "RealizationBoundaries.countableGrammarEscape_no_embedding",
863 "RealizationBoundaries.countableGrammarEscape_family_cardinality",
864 "RealizationBoundaries.pairedCompletionEquiv",
865 "RealizationBoundaries.paired_countably_infinite",
866 "RealizationBoundaries.not_injective_hom_of_divisible"
867 ],
868 "scope_note": "Arbitrary fixed countable semantics, infinitely repeated diagonal disagreement, continuum many pairwise nonisomorphic/nonembeddable actual groups with the same completion. No effective semantic evaluator is assumed."
869 },
870 {
871 "statement": "10.2",
872 "kind": "proposition",
873 "title": "Admissible expansion",
874 "label": "thm:grammarextension",
875 "chapter": "Escaping a fixed finite grammar",
876 "source": "publication/monograph_source/manuscript/chapters/10_grammar.tex",
877 "source_line": 54,
878 "printed_page": "39",
879 "evidence": "Printed proof and accepted integrated Lean evidence; exact contracts and scope are recorded below.",
880 "lean_status": "COMPLETE",
881 "lean_declarations": [
882 "RealizationBoundaries.DescriptionGrammar.admissible_expansion",
883 "RealizationBoundaries.DescriptionGrammar.admissible_expansion_length",
884 "RealizationBoundaries.DescriptionGrammar.admissible_expansion_complexity"
885 ],
886 "scope_note": "Actual valid-description translation, semantic preservation, shortest witnesses and the exact length-overhead inequality."
887 }
888 ]
Other PDFs for this work
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: 42ae7950dea9beb648c3c9f4093eb1cadbffdf803fa3fcca514188544d6802fe