Edition README
Realization Boundaries
README.md
1 # Realization Boundaries
2
3 ## Finite Grammar, Infinite Groups, and the Limits of Reconstruction
4
5 **Komorebi P. · Realization Calculus · MIT license**
6
7 A monograph, Lean library, and exact Python implementation about what finite observations preserve, what completion forgets, and what information is required to compute a realization.
8
9 The central family consists of countable abelian groups
10
11 $$
12 D=\bigoplus_p C_p\subseteq G_A\subseteq P=\prod_p C_p.
13 $$
14
15 Every member has the same full unmarked finite-quotient system and profinite completion. Yet
16
17 $$
18 G_A\cong G_B\iff A\triangle B\text{ is finite},\qquad
19 G_A\text{ has an }X\text{-computable copy}\iff A\le_T X.
20 $$
21
22 Every ordinary Turing degree occurs as a least presentation degree over one fixed computable observation system. Every fixed countable description grammar misses continuum many pairwise nonisomorphic members. The development also proves subgroup classification, root certificates, exact finite quotients, homomorphism structure, and categorical reconstruction boundaries.
23
24 **All 45 registered monograph contracts are complete in the checked Lean companion.**
25
26 | Accepted verification | Result |
27 |---|---:|
28 | Production modules rebuilt and kernel-replayed | 66 |
29 | Named source theorems and lemmas | 813 |
30 | Audited declarations | 2,188 |
31 | Positive contract declarations | 205 |
32 | Intended rejection controls | 44 |
33 | Passing command gates | 183 |
34
35 These counts describe the accepted mathematical release. GitHub packaging changes preserve its checked proof inputs and original receipt.
36
37 ## Start here
38
39 - [Read the 66-page monograph](publication/Realization_Boundaries_Monograph.pdf).
40 - [Browse the Lean entry point](RealizationBoundaries.lean) and [production modules](RealizationBoundaries).
41 - [See the complete statement coverage map](docs/MONOGRAPH_COVERAGE.md).
42 - [Inspect exact audited declaration types](docs/ACCEPTED_EXACT_DECLARATIONS.json).
43 - [Read the verification report](LEAN_VERIFICATION_REPORT.md) and [accepted receipt](verification/accepted_v1.0.0/run.json).
44 - [Run the worked Python examples](publication/monograph_source/README.md).
45 - [Build and verify from source](docs/BUILDING.md).
46
47 ## Quick start
48
49 Run commands from the repository root after extracting the ZIP or checking out the repository.
50
51 ```bash
52 python3 verify_integrity.py
53 lake exe cache get
54 lake build
55 ```
56
57 The Lean commands require an installed Lean toolchain manager such as `elan`. The repository's [lean-toolchain](lean-toolchain), [Lake configuration](lakefile.toml), and [dependency manifest](lake-manifest.json) pin the exact compiler and dependency revisions. The cache command downloads the pinned dependencies and their compiled caches. Keep the manifest unchanged when reproducing this release.
58
59 For the full Linux or WSL2 audit, once the dependencies are present:
60
61 ```bash
62 bash verify_with_lake.sh --output ../realization-boundaries-verification
63 ```
64
65 The output directory must be new. This runs the existing strict verifier using the pinned Lean installation on `PATH`. A separately supplied offline portable kit is also supported; see [building instructions](docs/BUILDING.md#offline-portable-kit).
66
67 For the exact Python examples, which need only Python 3.10 or later and its standard library:
68
69 ```bash
70 cd publication/monograph_source
71 python3 worked_example.py
72 python3 src/replay_printed_example.py
73 ```
74
75 ## Scope and evidence
76
77 The coverage registry links every numbered contract to accepted declarations. Computability claims use explicit oracle programs, decidable semantic equality, and genuinely bijective names. The original group, its completion, marked and unmarked copies, and semantic descriptions versus effective presentations are kept distinct.
78
79 Accepted proof dependencies are restricted to `propext`, `Classical.choice`, and `Quot.sound`. The production audit accepts no placeholder proof, project axiom, unsafe declaration, or native-decision trust axiom. Replay uses the same Lean implementation and pinned imported caches. It is not independent-kernel checking or external peer review.
80
81 The Lean code proves finite-code interpretation, root oracle and loop bounds, and cocycle query locality. Polynomial bit-cost bounds and kernel certification of the separate Python runtime are outside the release's claims. The Python suites passed 189,069 exact finite assertions; those are implementation checks, separate from the universal Lean proofs.
82
83 ## Repository contents
84
85 | Path | Contents |
86 |---|---|
87 | `RealizationBoundaries/` | Checked Lean production sources |
88 | `tests/` | Positive contracts, native examples, and rejection controls |
89 | `scripts/` | Original accepted verification tooling |
90 | `publication/` | Monograph PDF, editable source, vector figures, and Python implementation |
91 | `docs/` | Coverage, proof interfaces, reviews, and historical notes |
92 | `verification/accepted_v1.0.0/` | Accepted compiler, audit, replay, and identity evidence |
93 | `verification/development/` | Clearly labeled development attempts and reviews |
94 | `provenance/` | Preserved predecessor material |
95
96 [Citation](CITATION.cff) · [Contributing](CONTRIBUTING.md) · [Release notes](RELEASE_NOTES.md) · [License](LICENSE) · [Progress ledger](PROGRESS_LEDGER_v1.0.0.md)