Realization Boundaries

Download original file

Read the formatted document

1 # Monograph coverage — final release
2 
3 All **45 numbered contracts are COMPLETE** under their exact documented semantics. This is a statement-contract count, not an effort estimate or a novelty count.
4 
5 | Statement | Title | Status |
6 |---|---|---|
7 | 1.5 | Countable-code bound | COMPLETE |
8 | 1.8 | Reachability obstruction | COMPLETE |
9 | 2.1 | The torsion subgroup of the product | COMPLETE |
10 | 2.2 | Diagonal endomorphisms of the direct sum | COMPLETE |
11 | 2.3 | An infinite seed obstruction | COMPLETE |
12 | 2.4 | Topological cyclicity | COMPLETE |
13 | 2.5 | Profinite completion of the direct sum | COMPLETE |
14 | 2.6 | Unique division in the ambient quotient | COMPLETE |
15 | 3.1 | Subgroup and isomorphism classification | COMPLETE |
16 | 3.2 | Finite observations leave continuum many possibilities | COMPLETE |
17 | 3.3 | The prime-spectrum criterion | COMPLETE |
18 | 3.4 |  | COMPLETE |
19 | 3.5 | Unary selector classification | COMPLETE |
20 | 4.2 | Pure-preimage correspondence | COMPLETE |
21 | 4.3 | Ambient root criterion | COMPLETE |
22 | 4.4 | One finite-quotient system for every preimage | COMPLETE |
23 | 4.5 | Finite-target equivalence | COMPLETE |
24 | 4.6 | Structure of an ambient preimage | COMPLETE |
25 | 5.1 | Unique normal form | COMPLETE |
26 | 5.2 | A finite support bound | COMPLETE |
27 | 5.3 | Explicit group law | COMPLETE |
28 | 5.4 | One cocycle value reads one coordinate | COMPLETE |
29 | 5.5 | Finitely generated subgroups | COMPLETE |
30 | 6.1 | Root or obstruction | COMPLETE |
31 | 6.2 | All roots and their number | COMPLETE |
32 | 6.3 | All integer quotients | COMPLETE |
33 | 6.4 | Common profinite completion | COMPLETE |
34 | 7.1 | Tail signature | COMPLETE |
35 | 7.2 | Unmarked isomorphism classification | COMPLETE |
36 | 7.3 | Marked classification | COMPLETE |
37 | 7.5 | Complete homomorphism description | COMPLETE |
38 | 7.6 | Torsion-image obstruction | COMPLETE |
39 | 7.7 | Endomorphism ring | COMPLETE |
40 | 7.8 | Automorphisms | COMPLETE |
41 | 7.9 | Seed-rank separation | COMPLETE |
42 | 8.1 | Uniform construction relative to the selector | COMPLETE |
43 | 8.2 | Uniform marked decoding | COMPLETE |
44 | 8.3 | Exact oracle criterion | COMPLETE |
45 | 8.4 | Degree variation with fixed observations | COMPLETE |
46 | 9.1 | No decoder from the unmarked finite-quotient system | COMPLETE |
47 | 9.2 | A proper map invisible after completion | COMPLETE |
48 | 9.3 | Faithfulness and failure of fullness | COMPLETE |
49 | 9.4 | Reflection within the paired-prime family | COMPLETE |
50 | 10.1 | Escape within one profinite-completion class | COMPLETE |
51 | 10.2 | Admissible expansion | COMPLETE |
52 
53 ## 1.5 — Countable-code bound
54 
55 Arbitrary countable finite syntax, arbitrary validity, and single-valued semantics; actual semantic image is countable.
56 
57 Declarations: `RealizationBoundaries.finite_description_outputs_countable`, `RealizationBoundaries.finite_description_cardinal_bound`
58 
59 ## 1.8 — Reachability obstruction
60 
61 Actual dependent direct sum, vanishing transfer blocks, finite operator words, finite directed paths, and the omitted-packet closed-kernel consequence.
62 
63 Declarations: `RealizationBoundaries.operator_hull_reachable`, `RealizationBoundaries.unreachable_packet_obstructs`, `RealizationBoundaries.unreachable_packet_obstructs_topological`, `RealizationBoundaries.graphReach_iff_finite_path`
64 
65 ## 2.1 — The torsion subgroup of the product
66 
67 The original finite-support subgroup is torsion, dense and proper in the actual unrestricted product.
68 
69 Declarations: `RealizationBoundaries.torsion_iff_finiteSupport`, `RealizationBoundaries.finiteSupport_dense`, `RealizationBoundaries.finiteSupport_ne_top`
70 
71 ## 2.2 — Diagonal endomorphisms of the direct sum
72 
73 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 Declarations: `RealizationBoundaries.finiteSupportEndomorphismRingEquiv`, `RealizationBoundaries.finiteSupportDiagonalRing_bijective`, `RealizationBoundaries.finiteSupport_endomorphism_coordinate`, `RealizationBoundaries.finiteSupport_endomorphism_preserves_zero`
76 
77 ## 2.3 — An infinite seed obstruction
78 
79 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.
80 
81 Declarations: `RealizationBoundaries.finiteSupport_seed_certificate`, `RealizationBoundaries.finiteSupport_no_finite_endomorphism_seeds`, `RealizationBoundaries.finiteSupport_no_finite_topological_seeds`, `RealizationBoundaries.finiteSupport_endomorphismSeedRank`, `RealizationBoundaries.finiteSupport_topologicalEndomorphismSeedRank`
82 
83 ## 2.4 — Topological cyclicity
84 
85 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.
86 
87 Declarations: `RealizationBoundaries.finite_coordinate_interpolation`, `RealizationBoundaries.ambient_cyclic_dense`, `RealizationBoundaries.ambient_topological_generator`, `RealizationBoundaries.ambient_ordinaryTopologicalRank`
88 
89 ## 2.5 — Profinite completion of the direct sum
90 
91 Topological additive equivalence from Mathlib's actual all-finite-quotients completion of D to P, respecting the canonical map.
92 
93 Declarations: `RealizationBoundaries.finiteSupportCompletionEquiv`, `RealizationBoundaries.finiteSupportCompletionEquiv_eta`
94 
95 ## 2.6 — Unique division in the ambient quotient
96 
97 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.
98 
99 Declarations: `RealizationBoundaries.tail_nsmul_bijective`, `RealizationBoundaries.tail_rational_module_unique`, `RealizationBoundaries.hom_zero_of_divisible`, `RealizationBoundaries.not_injective_hom_of_divisible`
100 
101 ## 3.1 — Subgroup and isomorphism classification
102 
103 Actual subgroup classification and intrinsic prime torsion; literal lattice operations; independently induced membership topology and Cantor homeomorphism.
104 
105 Declarations: `RealizationBoundaries.subgroupSpectrumOrderIso`, `RealizationBoundaries.finiteSupport_subgroup_fullyInvariant`, `RealizationBoundaries.spectrumSubgroup_isomorphic_iff`, `RealizationBoundaries.subgroupCantorHomeomorph`, `RealizationBoundaries.natSubgroupCantorHomeomorph`
106 
107 ## 3.2 — Finite observations leave continuum many possibilities
108 
109 Exact continuum cardinality after every finite observation, pairwise abstract nonisomorphism, and existence plus uniqueness from coherent finite patterns.
110 
111 Declarations: `RealizationBoundaries.spectrumObservationFiber_card`, `RealizationBoundaries.spectrumObservation_not_isomorphic`, `RealizationBoundaries.compatible_spectrum_patterns_exists_unique`
112 
113 ## 3.3 — The prime-spectrum criterion
114 
115 Full finite-or-infinite copy convention; actual native oracle-computable stage listings, positive witness tests and partial-recursive domains are proved equivalent.
116 
117 Declarations: `RealizationBoundaries.oracle_spectrum_copy_iff_stageListing`, `RealizationBoundaries.oracle_spectrum_copy_iff_enumerable`, `RealizationBoundaries.oracleEnumerable_iff_stageListing`
118 
119 ## 3.4 — 
120 
121 Actual diagonal halting complement, no finite or infinite computable copy, native relator enumeration and the universal commuting prime-order presentation of the actual quotient.
122 
123 Declarations: `RealizationBoundaries.haltingSpectrum_no_any_computable_copy`, `RealizationBoundaries.haltingGroup_prime_order_presentation`, `RealizationBoundaries.computable_primeOrderRelatorLabel`, `RealizationBoundaries.primrec_haltingRelatorIndexStage`, `RealizationBoundaries.haltingRelatorIndexStage_exact`
124 
125 ## 3.5 — Unary selector classification
126 
127 Genuine finite unary automata and both directions of ultimate periodicity; actual prime-spectrum abstract isomorphism criterion.
128 
129 Declarations: `RealizationBoundaries.unary_selector_classification`, `RealizationBoundaries.unaryRecognizable_iff_ultimatelyPeriodic`
130 
131 ## 4.2 — Pure-preimage correspondence
132 
133 Both directions, both inverse laws and order reflection are checked. Purity is root lifting in P; inclusion of D is explicit.
134 
135 Declarations: `RealizationBoundaries.IsPure`, `RealizationBoundaries.pure_root_closed`, `RealizationBoundaries.rationalImage`, `RealizationBoundaries.purePreimageOrderIso`, `RealizationBoundaries.exists_unique_rational_preimage`
136 
137 ## 4.3 — Ambient root criterion
138 
139 Both directions for every positive multiplier and every actual preimage.
140 
141 Declarations: `RealizationBoundaries.ambient_root_iff`, `RealizationBoundaries.preimage_root_iff`
142 
143 ## 4.4 — One finite-quotient system for every preimage
144 
145 Canonical integer quotients, coordinate transitions, finite-target cofinal kernels and the actual profinite completion are checked.
146 
147 Declarations: `RealizationBoundaries.integerQuotientEquiv`, `RealizationBoundaries.integerQuotientEquiv_mk`, `RealizationBoundaries.coordinateRestriction_map`, `RealizationBoundaries.finite_target_coordinate_kernel`, `RealizationBoundaries.profiniteCompletionEquiv`, `RealizationBoundaries.profiniteCompletionEquiv_eta`
148 
149 ## 4.5 — Finite-target equivalence
150 
151 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.
152 
153 Declarations: `RealizationBoundaries.finiteSupportRestrictionEquiv`, `RealizationBoundaries.finiteSupportRestrictionEquiv_apply`, `RealizationBoundaries.finiteSupportRestrictionEquiv_natural`
154 
155 ## 4.6 — Structure of an ambient preimage
156 
157 Adds the exact rational dimension formulation, including zero and finite dimension, to all preserved structural conclusions.
158 
159 Declarations: `RealizationBoundaries.preimage_countable_iff_rational_rank`, `RealizationBoundaries.preimage_countable_iff_dimension_finite_or_countably_infinite`
160 
161 ## 5.1 — Unique normal form
162 
163 Existence, uniqueness, the selector-independent Q x D domain and countable infinitude of every paired group are now checked.
164 
165 Declarations: `RealizationBoundaries.normalForm_exists`, `RealizationBoundaries.normalForm_unique`, `RealizationBoundaries.normalFormEquiv`, `RealizationBoundaries.paired_countably_infinite`, `RealizationBoundaries.NormalForm.pairEquiv`, `RealizationBoundaries.pairedNormalFormEquiv`
166 
167 ## 5.2 — A finite support bound
168 
169 The actual infinite-coordinate defect is supported on denominator primes.
170 
171 Declarations: `RealizationBoundaries.sectionDefect_support`, `RealizationBoundaries.sectionDefect_finite`
172 
173 ## 5.3 — Explicit group law
174 
175 Separate twisted group type, all additive group laws, and actual additive equivalence to the preimage.
176 
177 Declarations: `RealizationBoundaries.cocycle_identity`, `RealizationBoundaries.normalAdd_assoc`, `RealizationBoundaries.normalAdd_comm`, `RealizationBoundaries.normalAdd_zero`, `RealizationBoundaries.normalAdd_inverse`, `RealizationBoundaries.NormalForm.realizationEquiv`
178 
179 ## 5.4 — One cocycle value reads one coordinate
180 
181 Literal finite-support equality for the printed cocycle value, plus exact coordinate recovery.
182 
183 Declarations: `RealizationBoundaries.cocycle_reads_coordinate`, `RealizationBoundaries.cocycle_coordinate_nonzero_iff`
184 
185 ## 5.5 — Finitely generated subgroups
186 
187 Every actual FG subgroup is squarefree finite cyclic or Z times a squarefree finite cyclic group; no splitting hypothesis is assumed.
188 
189 Declarations: `RealizationBoundaries.paired_fg_subgroup_classification`, `RealizationBoundaries.rational_subgroup_fg_isAddCyclic`
190 
191 ## 6.1 — Root or obstruction
192 
193 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.
194 
195 Declarations: `RealizationBoundaries.finite_root_algorithm_correct`, `RealizationBoundaries.codedNormalValue_represents`, `RealizationBoundaries.certifiedRootSolver_error`, `RealizationBoundaries.certifiedRootSolver_ok`, `RealizationBoundaries.finiteRootSolver_complete`, `RealizationBoundaries.finiteRootSolver_support_bound`, `RealizationBoundaries.countedCertifiedRootSolver_erase`, `RealizationBoundaries.countedCertifiedRootSolver_step_bound`, `RealizationBoundaries.countedCertifiedRootSolver_query_bound`
196 
197 ## 6.2 — All roots and their number
198 
199 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.
200 
201 Declarations: `RealizationBoundaries.RootFiber`, `RealizationBoundaries.rootKernelEquiv`, `RealizationBoundaries.rootFiberTranslation`, `RealizationBoundaries.rootFiber_coset_iff`, `RealizationBoundaries.rootFiberEquiv`, `RealizationBoundaries.rootFiberEquiv_symm_apply`, `RealizationBoundaries.rootFiber_finite`, `RealizationBoundaries.rootKernel_card`, `RealizationBoundaries.rootFiber_card_of_solvable`, `RealizationBoundaries.rootFiber_card`, `RealizationBoundaries.prime_power_root_count`
202 
203 ## 6.3 — All integer quotients
204 
205 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.
206 
207 Declarations: `RealizationBoundaries.integerQuotientEquiv`, `RealizationBoundaries.divisorCrtEquiv`, `RealizationBoundaries.cyclicIntegerQuotientEquiv`, `RealizationBoundaries.cyclicIntegerQuotientEquiv_mk`, `RealizationBoundaries.quotientRestriction`, `RealizationBoundaries.integerQuotientEquiv_restriction`, `RealizationBoundaries.cyclicIntegerQuotientEquiv_restriction`, `RealizationBoundaries.multiples_eq_radical`, `RealizationBoundaries.finite_quotient_exists_iff`, `RealizationBoundaries.finite_surjection_ker`
208 
209 ## 6.4 — Common profinite completion
210 
211 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.
212 
213 Declarations: `RealizationBoundaries.pairedCompletionEquiv`, `RealizationBoundaries.profiniteCompletionEquiv_eta`, `RealizationBoundaries.completion_eta_isEmbedding`, `RealizationBoundaries.fullProfiniteTopology_eq`
214 
215 ## 7.1 — Tail signature
216 
217 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.
218 
219 Declarations: `RealizationBoundaries.tailExceptions_finite`, `RealizationBoundaries.normalForm_coordinate_ne_zero_iff`, `RealizationBoundaries.selector_tail_signature`
220 
221 ## 7.2 — Unmarked isomorphism classification
222 
223 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.
224 
225 Declarations: `RealizationBoundaries.pairedGroup_isomorphic_iff`, `RealizationBoundaries.pairedGroup_eq_of_finite_disagreement`, `RealizationBoundaries.pairedEquivOfFiniteDisagreement_val`, `RealizationBoundaries.normalFormTransportEquiv_apply`, `RealizationBoundaries.normalFormTransport_add`
226 
227 ## 7.3 — Marked classification
228 
229 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.
230 
231 Declarations: `RealizationBoundaries.selectors_equal_of_markedEquiv`, `RealizationBoundaries.pairedGroup_marked_isomorphic_iff`, `RealizationBoundaries.toggleBit_not_marked_isomorphic`
232 
233 ## 7.5 — Complete homomorphism description
234 
235 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.
236 
237 Declarations: `RealizationBoundaries.hom_coordinate_formula`, `RealizationBoundaries.homDiagonal_unique`, `RealizationBoundaries.diagonalHomEquiv`, `RealizationBoundaries.diagonalTail`, `RealizationBoundaries.diagonalAdmissible_selector_iff`, `RealizationBoundaries.diagonalAdmissible_iff_finite_defect`, `RealizationBoundaries.selectorHomEquiv`, `RealizationBoundaries.preimage_hom_continuous`, `RealizationBoundaries.completionHom_coordinates`
238 
239 ## 7.6 — Torsion-image obstruction
240 
241 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.
242 
243 Declarations: `RealizationBoundaries.finite_disagreement_of_nontorsion_image`, `RealizationBoundaries.hom_image_finiteSupport`, `RealizationBoundaries.hom_image_torsion`, `RealizationBoundaries.torsionFactor_commutes`, `RealizationBoundaries.torsionFactor_unique`, `RealizationBoundaries.no_injective_hom_of_infinite_disagreement`, `RealizationBoundaries.no_surjective_hom_of_infinite_disagreement`, `RealizationBoundaries.pairedGroup_embeds_iff`, `RealizationBoundaries.pairedGroup_surjects_iff`
244 
245 ## 7.7 — Endomorphism ring
246 
247 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.
248 
249 Declarations: `RealizationBoundaries.endomorphismRingEquiv`, `RealizationBoundaries.diagonalEndRing_mem_iff`, `RealizationBoundaries.diagonalSlope_unique`, `RealizationBoundaries.diagonalSlope_eq_of_finite_defect`, `RealizationBoundaries.quotientScalar`, `RealizationBoundaries.quotientScalar_surjective`, `RealizationBoundaries.quotientScalar_eq_zero_iff`, `RealizationBoundaries.endomorphismQuotientScalar`, `RealizationBoundaries.endomorphismQuotientScalar_surjective`
250 
251 ## 7.8 — Automorphisms
252 
253 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.
254 
255 Declarations: `RealizationBoundaries.hom_injective_iff_diagonal_nonzero`, `RealizationBoundaries.diagonalSlope_ne_zero`, `RealizationBoundaries.inverseDiagonal_admissible`, `RealizationBoundaries.selectorEquivOfNonzeroDiagonal`, `RealizationBoundaries.selectorEquiv_inverse_coordinate`, `RealizationBoundaries.selector_endomorphism_automorphism_iff`, `RealizationBoundaries.selector_hom_bijective_iff`
256 
257 ## 7.9 — Seed-rank separation
258 
259 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.
260 
261 Declarations: `RealizationBoundaries.selector_outside_support_finite`, `RealizationBoundaries.paired_seed_certificate`, `RealizationBoundaries.paired_endomorphismSeedRank`, `RealizationBoundaries.paired_topologicalEndomorphismSeedRank`, `RealizationBoundaries.paired_ordinaryTopologicalRank`, `RealizationBoundaries.completionGenerator_generates`, `RealizationBoundaries.canonicalCompletion_ordinaryTopologicalRank`, `RealizationBoundaries.paired_seed_rank_separation`
262 
263 ## 8.1 — Uniform construction relative to the selector
264 
265 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.
266 
267 Declarations: `RealizationBoundaries.pairedOracleCopy`, `RealizationBoundaries.canonicalPairedAddition_oracle_iff`, `RealizationBoundaries.canonicalPairedAddition_graph_equivalent`, `RealizationBoundaries.localNormalAdd_correct`, `RealizationBoundaries.localNormalAdd_loop_oracleComputable`, `RealizationBoundaries.localCocycleQuerySchedule_mem`, `RealizationBoundaries.localCocycleQuerySchedule_nodup`
268 
269 ## 8.2 — Uniform marked decoding
270 
271 Actual addition algorithm, computed integer multiples and terminating complementary positive searches with a supplied marker name.
272 
273 Declarations: `RealizationBoundaries.oracle_marked_copy_reduces`, `RealizationBoundaries.marked_root_presentation_reduces`
274 
275 ## 8.3 — Exact oracle criterion
276 
277 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.
278 
279 Declarations: `RealizationBoundaries.paired_oracle_copy_iff`, `RealizationBoundaries.paired_least_presentation_degree`
280 
281 ## 8.4 — Degree variation with fixed observations
282 
283 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.
284 
285 Declarations: `RealizationBoundaries.every_set_degree_with_fixed_computable_observation`, `RealizationBoundaries.paired_isReduced`, `RealizationBoundaries.allFiniteObservation_fixed_computable`, `RealizationBoundaries.computableObservationQuotientIso`
286 
287 ## 9.1 — No decoder from the unmarked finite-quotient system
288 
289 Actual all-finite-quotient diagrams and source-free cofinal natural comparisons. Arbitrary invariant decoders are impossible; no completion-only surrogate or computability assumption.
290 
291 Declarations: `RealizationBoundaries.coordinateIndexFunctor_initial`, `RealizationBoundaries.coordinateObservationIso`, `RealizationBoundaries.no_unmarked_observation_decoder`
292 
293 ## 9.2 — A proper map invisible after completion
294 
295 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.
296 
297 Declarations: `RealizationBoundaries.finiteSupport_inclusion_not_surjective`, `RealizationBoundaries.finiteSupportToPairedCompletion`, `RealizationBoundaries.finiteSupportToPairedCompletion_eta`
298 
299 ## 9.3 — Faithfulness and failure of fullness
300 
301 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.
302 
303 Declarations: `RealizationBoundaries.official_completion_map_injective`, `RealizationBoundaries.residuallyFiniteCompletion_faithful`, `RealizationBoundaries.pairedCompletionFunctor_not_full`, `RealizationBoundaries.boundaryCompletionFunctor_not_reflects_isomorphisms`
304 
305 ## 9.4 — Reflection within the paired-prime family
306 
307 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.
308 
309 Declarations: `RealizationBoundaries.completionHom`, `RealizationBoundaries.completionHom_eta`, `RealizationBoundaries.completionHom_unique`, `RealizationBoundaries.completionHom_comp`, `RealizationBoundaries.completionHom_isomorphism_iff`, `RealizationBoundaries.selector_completion_reflection`, `RealizationBoundaries.paired_completion_reflects_isomorphisms`
310 
311 ## 10.1 — Escape within one profinite-completion class
312 
313 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.
314 
315 Declarations: `RealizationBoundaries.countableGrammarEscape_not_output`, `RealizationBoundaries.countableGrammarEscape_pairwise_nonisomorphic`, `RealizationBoundaries.countableGrammarEscape_no_embedding`, `RealizationBoundaries.countableGrammarEscape_family_cardinality`, `RealizationBoundaries.pairedCompletionEquiv`, `RealizationBoundaries.paired_countably_infinite`, `RealizationBoundaries.not_injective_hom_of_divisible`
316 
317 ## 10.2 — Admissible expansion
318 
319 Actual valid-description translation, semantic preservation, shortest witnesses and the exact length-overhead inequality.
320 
321 Declarations: `RealizationBoundaries.DescriptionGrammar.admissible_expansion`, `RealizationBoundaries.DescriptionGrammar.admissible_expansion_length`, `RealizationBoundaries.DescriptionGrammar.admissible_expansion_complexity`

Back to source controls