Continuum setup, replay instructions, and scope
Physics
README.md
1 # Komorebi Physics: centered continuum verification
2
3 Formal checkpoint **0.51.0**, PHYS-CENT-51.
4
5 This source package completes the centered approximation block for the free
6 Dirac field on a fixed flat torus. Its centered operators act on the same
7 infinite Fourier coefficient space as the self-adjoint continuum Hamiltonian.
8 The checked results cover the full maximal first-order domain, every nonreal
9 spectral parameter, and quadratic generator and propagator bounds under an
10 explicit third-order Fourier moment assumption.
11
12 The four new modules contain **74 named theorems, 15 definitions and 11
13 abbreviations**. The fresh gate audited **162 compiled environment
14 declarations** from those modules, including generated helpers. The unchanged
15 strong-generator module contributes **37 named theorems and 2 definitions**,
16 with **47 compiled environment declarations** rechecked in
17 the same gate. These are scoped counts, not a total for the physics program.
18
19 ## Main results
20
21 - Bounded, self-adjoint centered operators for every nonzero real spacing.
22 - Graph-domain convergence for every vector in the maximal continuum domain.
23 - Two-sided strong-resolvent convergence for every nonreal complex parameter
24 and every square-summable field, with actual inverse and domain laws.
25 - Generator error at most `h² M₃(f) / 6` and propagator error at most
26 `|t| h² M₃(f) / 6`, with the corresponding uniform bound on `|t| ≤ T`, `T ≥ 0`.
27 - All these statements transported through the actual Fourier equivalence to
28 physical torus fields. The modal perturbation proof does not assume that
29 different Dirac matrices commute.
30
31 ## Evidence and navigation
32
33 - [Accepted gate receipt](verification/block51/current/receipt.json):
34 26 fresh local compilation targets, 64 recorded commands,
35 21 controls (8 positive, 12 elaboration rejections,
36 1 axiom-policy rejection).
37 - [Proof guide](docs/BLOCK_51_PROOF_GUIDE.md) and [source map](docs/SOURCE_MAP.md).
38 - [Scoped inventory](declaration_inventory.json) and [progress ledger](PROGRESS_LEDGER_v0.51.0.md).
39 - [Preservation record](BLOCK51_PRESERVATION.json) and [acceptance record](BLOCK51_ACCEPTANCE.json).
40 - [Predecessor metadata](history/metadata_v0.49.0/PRESERVATION.json), retained unchanged.
41
42 The compiler is Lean 4.34.0-rc2 at commit
43 `6a10ac8c22beadecabdbb0919c2b50214762f91d`. Mathlib is pinned to
44 `aeb72f1e9981b6d35b426b16dca7759be3e7ba06`. Compiled external dependencies
45 are reused. The new local import closure was compiled into an empty object
46 directory. The five root modules received recursive axiom audits and actual
47 `leanchecker` replay using the same Lean kernel and imported environment.
48
49 ## Replay
50
51 With the documented pinned portable runtime restored, run from this directory:
52
53 ```sh
54 python3 verification/block51/current/snapshot/runner/verify_centered.py \
55 --project . \
56 --runtime /absolute/path/to/Komorebi_Portable_Lean_4.34.0-rc2 \
57 --controls verification/block51/current/snapshot/CONTROL_MANIFEST.json \
58 --out-dir /absolute/path/to/a-new-verification-directory
59 ```
60
61 The output directory must not already exist. The runtime is external and is not
62 reconstructed from this source package. Its compiler/source/cache identity is
63 checked by the supplied runner. Mutable dependency Git indexes are explicitly
64 excluded from the relevant runtime endpoint comparison and retained in the
65 provenance records.
66
67 ## Exact boundaries
68
69 The bounded global operator has an explicitly auxiliary zero value at spacing
70 zero. Its modal evaluation and inverse laws require nonzero spacing, and its
71 graph limit uses a punctured neighborhood. The centered modal propagator and
72 resolvent instead use their continuum fill at zero. They are not identified as
73 the evolution or inverse of the auxiliary zero operator there.
74
75 The third-order moment requires actual series summability. The compact-time
76 bound retains `T ≥ 0`. This checkpoint proves strong resolvent convergence,
77 not operator-norm resolvent convergence. It does not identify a changing finite
78 sampled lattice with the fixed Fourier space.
79
80 Abstract unbounded spectral-functional-calculus linkage, finite-grid comparison,
81 interacting gauge evolution, the wider historical evidence audit, and physical
82 cosmological production remain separate obligations. Earlier cosmological
83 failures have not been repaired by these free-field theorems.
84
85 Original code retains the supplied MIT grant. Original prose and figures retain
86 the supplied CC BY 4.0 grant and third-party exceptions. See the publication
87 license and provenance notices supplied alongside this formal package.