BLOCK_51_PROOF_GUIDE.md
Physics
BLOCK_51_PROOF_GUIDE.md
1 # Block 51 proof guide
2
3 The source target is the centered approximation argument in sections 3 and 4 of
4 *The Dirac Group and Its Generator*. The proof works on the inherited complete
5 coefficient Hilbert space and the actual torus Fourier equivalence.
6
7 ## Construction and proof order
8
9 1. `Relativistic3DCenteredConvergence` transports the arbitrary real-momentum
10 Clifford square into the Hilbert spinor representation. Its exact norm
11 identity controls both individual symbols and their differences.
12 2. `boundedModewiseOperator` lifts any uniformly bounded family of mode maps
13 to a continuous linear operator on the full coefficient space. The sine
14 bound gives the centered norm estimate `sqrt(m²+3h⁻²)` for `h ≠ 0`.
15 Summing modal symmetry proves self-adjointness.
16 3. The sine quotient is expressed using the continuous sinc function. This
17 supplies a genuine two-sided modal limit. Centered modal norms are bounded
18 by continuum modal norms, so errors are dominated by twice the continuum
19 output. Its square sum is finite on the maximal domain. The checked
20 coefficient dominated-convergence lemma yields the complete graph limit.
21 4. `Relativistic3DCenteredResolvent` constructs modal inverses for every nonreal
22 parameter, using self-adjoint real spectrum and the imaginary-part norm
23 lower bound. The uniform `1/abs(z.im)` estimate lifts the inverses to the
24 coefficient space. The identity `H R_z f = f + z R_z f` proves range
25 membership in the unbounded domain, and both inverse laws are supplied.
26 5. Applying the resolvent identity to `g = R_z f` reduces the resolvent error
27 to the already proved graph error at this actual domain vector. The bound
28 proves strong resolvent convergence for every square-summable input and
29 every nonreal parameter. No convergence in operator norm is asserted.
30 6. `Relativistic3DCenteredRates` uses the global sine error with coefficient
31 `1/6`. The third-order condition is a `Summable` proposition. It implies
32 first-order domain membership and bounds the summed squared modal errors.
33 This proves the full generator estimate under precisely the stated extra
34 regularity.
35 7. `Relativistic3DModalPerturbation` differentiates the interpolation
36 `U_A(t-s) U_B(s) ψ`. The two matrices need not commute. Unitarity and the
37 real mean-value estimate give the perturbation bound with `abs(t)` for
38 positive and negative times. Applying the exact Clifford difference norm
39 and the third-order moment yields the full propagator rate.
40 8. The inherited Fourier equivalence transports graph limits, actual
41 resolvents, inverse laws, and rates to physical torus fields. The compact
42 time bounds are pointwise uniform on `[-T,T]` with the explicit `T ≥ 0`.
43
44 ## Zero spacing and domain boundaries
45
46 The bounded global centered operator has auxiliary value zero at `h = 0`.
47 Its mode evaluation and inverse identities require `h ≠ 0`, and graph
48 convergence uses a punctured neighborhood. The filled modal propagator and
49 resolvent take continuum values at zero and are not identified as the
50 evolution or inverse of that auxiliary zero operator there.
51
52 The global third-order moment is not a finite-grid approximation. No rate is
53 claimed for arbitrary square-summable data without its summability hypothesis.
54 Strong resolvent convergence, in contrast, does hold for every such input.
55 The rate keeps the stated coefficient `1/6`; its optimality is not separately
56 proved.
57
58 ## Verification and sensitivity
59
60 The fresh gate compiles the exact local import closure into empty local object
61 storage, audits all compiled constants owned by the five root modules, replays
62 each root with `leanchecker`, and runs positive, elaboration-rejection and
63 axiom-policy controls. Named source declarations and generated environment
64 constants are counted separately. External compiled dependencies and the Lean
65 kernel are reused under their recorded pins.
66
67 Positive controls exercise negative mass, negative spacing and time, physical
68 transport, arbitrary nonreal parameters, and concrete modes. Rejection controls
69 remove or alter spacing/domain/moment witnesses, signs, constants and filter
70 types. The custom-axiom control compiles in isolation before the recursive
71 axiom audit rejects it. Missing imports, timeouts and resource errors are not
72 accepted as intended rejections.
73
74 The complete result is in the [gate receipt](../verification/block51/current/receipt.json)
75 and [scoped inventory](../declaration_inventory.json). The [progress ledger](../PROGRESS_LEDGER_v0.51.0.md)
76 preserves failed development and infrastructure attempts separately from the
77 accepted run.
78
79 ## Remaining programs
80
81 The abstract unbounded spectral-functional-calculus API linkage remains open.
82 Finite-grid sampling, interpolation and aliasing require separate maps and
83 estimates. Background or dynamical gauge coupling and cosmological matching,
84 state preparation, capture and abundance are not consequences of this block.
85 The full historical physics aggregate has not received a new complete audit.