Proof packet round 4: 13 registered Side24/RN Props and remaining-Prop triage (source readback PASS; alignment pending)

specifications/lean_statement_proofs_20261011/SCOPE.md

@@ -31,9 +31,9 @@ statement proved here: **PENDING_INDEPENDENT_REVIEW**. Organizational-independen
 | family | the theorems establish | not established |
 |---|---|---|
 | P15 (`Specifications.P15`, modules P15Elementary, P15Structure, P15Hazard, P15Covers, P15Budget, P15Interpolation) | exact finite arithmetic and finite combinatorics of the registered Props: generator prices, the demand-one refutation data, `ρ* < 6/7` and its certificate, the 816-benchmark counts, palette identities, cover (816 and not 815) and union bound (P11); Proposition P1; both halves of Theorem P2 as the Props state them (the cover criterion (P7) and the hazard bound (P8) for prices `0 ≤ c_v ≤ p_v`) with the local statements (P2)-(P5); the restricted transformed-price budget (T1) with (T4), (T5) and the six-block transformed range; (F9), (F13), the sharpness clause of `ρ*` for the triple block; the hazard interpolation (F5)-(F8) (separate coordinatewise concavity of `t ↦ -log μ_{p(t)}(A)` for a proper downset, the product bound, the `φ` bound, the full-ground price bound and its exactness `iff`), the local bound (F12), Theorem F as `FullTransformedPriceBudget` states it ((F2): for every `p ∈ [0,1]^X`, every `0 ≤ c_v ≤ φ(p_v)` and `K ≥ K_H(d)`, `coverCost ≤ cappedHazard ρ* μ`) and the 20-digit enclosure (F3) of `ρ*`; all for the formal `RealizedData` record, downset, `coverCost` (an `sInf`) and `mu` | the informal P15 claims (P15-PRICE-BOUNDARY, P15-REALIZED-COVERS, FULL-PRICE, PRICE-BUDGET), their dispositions, Theorem F itself: the hazard interpolation (F4)-(F8), the block bound (F12) and the budget (F2), the 20-digit `ρ*` enclosure (F3); attainment of the `sInf`; alignment of `RealizedData`/`IsRealizedFamily`/`downset`/`coverCost`/`mu` with the informal objects (PENDING_INDEPENDENT_REVIEW), any prize statement |
-| Side24 (`Specifications.Side24`) | elementary exponential bounds, a term-ratio bound, the D2 cone-moment algebra, the reference-coefficient identity, the elementary cone integral, as the Props state them | the coefficient enclosure `c_{d,24}` (REVIEWED_SCOPED is transcribed, not derived), the Gaussian-moment and derivative-bound statements, the lattice image sum over a `tsum`, the interface-level statements |
-| RN (`Specifications.RN`) | the elementary probability identities and bounds N1–N5 as the Props state them, for the interface objects they quantify over | the Radon–Nikodym uniformity lemma `D3-LEMMA-RN-UNIF` (OPEN), the five validity premises of Theorem D1 v2.2(2) (OPEN), any identification of the interface with the actual field |
-| Lifetime, Field | nothing is expected to be provable (interface-level statements); no theorem is inventoried | everything |
+| Side24 (`Specifications.Side24`, modules Side24Elementary, Side24Analysis, Side24Interfaces) | elementary exponential bounds, a term-ratio bound, the D2 cone-moment algebra, the reference-coefficient identity, the elementary cone integral; the summability of the theta family `n ↦ exp(-‖z + 24 n‖²/2)` over `Fin d → ℤ` for every `d` and `z`; the Section 2 derivative bounds for Mathlib's `iteratedFDeriv ℝ q (Kinf d)` at unit tuples and `q ≤ 6` (the pairing bound `exp(-‖x‖²/2) pairingSum q ‖x‖`, `76 ‖x‖⁶ exp(-‖x‖²/2)` at `‖x‖ ≥ 1`, `15` at `0`); the lattice image sum (summable and `≤ 1458 e^{-288}` for `d ≤ 3`); the Section 1 reference blocks in an orthonormal frame (`Cov(G) = I`, `Var(t) = 15`, `Cov(t, G) = (-3, 0, …)`, `pinCov = diagonal (3, 1, …, 1)`, `τ² = 6`) and the pin density product `(2π)^{-d}/√3` for the formal `gaussDensity`; the Section 4 integrand ratio bounds (arithmetic in `epsilon`, `exponentA`, `exponentB`) and the density comparison for positive-definite matrices with `(1 - epsilon) • C0 ≤ C ≤ (1 + epsilon) • C0` in the Loewner order; and, for a GIVEN `I : ConeMomentInterface`, `D_1 = 4/3`, the trace moments `5/3`, `25/3`, `√(3/8)` and the Rayleigh law of `x² + y²` as a distribution function, from the interface's law fields alone; all as the Props state them, for the formal objects (`E d`, `Kinf`, `latticeVec`, `derivContraction`, `gaussDensity`, the interface structures) | the coefficient enclosure `c_{d,24}` (REVIEWED_SCOPED is transcribed, not derived): nothing here encloses the coefficient, and `CoefficientEnclosure` / `ReferenceComparison` are predicates on `PeriodicCoefficientInterface`, which takes the cone moment as a GIVEN field; `ImageBound`, `CovarianceOrdering`, `EntrywiseCovarianceBound` (no local term-wise iterated differentiation of the lattice sum at Mathlib `d13f23b7`), `ReferenceCovarianceLowerBound`, `ConeMomentD2Identity`; that `ConeMomentInterface` or `PeriodicCoefficientInterface` has an inhabitant, or that their law fields are the conditional law `A_u \| V_u = 0` of any field (no field is constructed); that any `gradCov`/`pinCov` matrix is the covariance of a random object; the source's shell count and closed-form derivative displays, which stay unspecified; alignment of the formal objects with the source's (PENDING_INDEPENDENT_REVIEW) |
+| RN (`Specifications.RN`, modules RNProbability, RNCluster) | the elementary probability identities and bounds N1–N5 as the Props state them, for the interface objects they quantify over; Theorem O's obstruction as `RareClusterPoissonObstructionO` states it, for a GIVEN family of pmfs `μ r : ℕ → ℝ` satisfying (H1) `∑ n μ r n ≤ A r³` and (H2) `a r³ ≤ 1 - μ r 0 - μ r 1` on `(0, r0]`: for all small `r`, every Poisson law is at `pmfTV` distance at least `(a/2) r³` from `μ r`, and one (`lam = 0`) is within `A r³`, with `2a ≤ A` derived, not assumed | the Radon–Nikodym uniformity lemma `D3-LEMMA-RN-UNIF` (OPEN), the five validity premises of Theorem D1 v2.2(2) (OPEN), any identification of the interface with the actual field; that (H1) or (H2) hold for the Gaussian window count (the source takes them from [D5] Theorem G_d and [C6] Corollary Theta; neither is revalidated here, and the Prop ties `μ` to no field), the mean-matched statement `lambda = mu`, Theorems C and S, the source's infimum form verbatim (the existential with witness `lam = 0` is what is proved); the 19 remaining RN Props over `PinnedLawInterface` (the D5 window bounds, the dimension lift, Theorem A(2)/A(3), the Palm and Fourier routes, Corollary D, the OPEN witness-collision target), which the interface under-determines (README table) |
+| Lifetime, Field | no theorem is inventoried; the round-4 triage (README table) classifies the 31 Props as 24 predicates (vocabulary), 3 interface-blocked (falsified by the constant laws `p ≡ 0` / `p ≡ 1` of `PairLawInterface`) and 4 Lifetime Props blocked on Mathlib developments (density versions, Kac–Rice), not on the interface | everything |
 
 The three lines of each theorem's docstring (`Proves:`, `Method:`, `Does not establish:`) are the
 per-theorem version of this table and are required by the gate.

specifications/lean_statement_proofs_20261011/SpecificationProofs.lean

@@ -6,3 +6,6 @@ import SpecificationProofs.P15Budget
 import SpecificationProofs.Side24Elementary
 import SpecificationProofs.RNProbability
 import SpecificationProofs.P15Interpolation
+import SpecificationProofs.Side24Analysis
+import SpecificationProofs.Side24Interfaces
+import SpecificationProofs.RNCluster