Proof packet round 6: ImageBound, EntrywiseCovarianceBound and CovarianceOrdering (Side24Images)

specifications/lean_statement_proofs_20261011/SCOPE.md

@@ -31,7 +31,7 @@ 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`, modules Side24Elementary, Side24Analysis, Side24Interfaces, Side24Covariance, Side24ConeMoment) | 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; the reference covariance lower bound: `Cref d (R 0) R - (1/3) • 1` positive semidefinite, its `IsHermitian` half included, for every orthonormal frame `R` and `d = 2` or `3`, as the Prop states it (the proof does not use that hypothesis; only the helper `Aux.cv_psd`, not an inventory theorem, is stated for every `0 < d`); 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, and the `m = 2` cone moment `∫ coneIntegrand (s, x, y) ∂I.P = (1/2)(25/3 - 20/3 + 8 - 8 √(3/8))` from the law field `sxy_law` alone (not `A_law`); all as the Props state them, for the formal objects (`E d`, `Kinf`, `latticeVec`, `derivContraction`, `gaussDensity`, `jointCov`, `Cref`, `coneIntegrand`, the interface structures); the reference covariance lower bound and the `m = 2` cone moment (round 5) are first receipted by run 38195810463 (PR head `c6ce0256`, actual tested merge `1320c5b2…` with base `be014794…`; receipt theorem_count 75) | 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`); 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 or `Cref` is the covariance of a random object; symmetry of `Cref d u R` for a general `u` or frame; the odd-block minors and eigenvalues `8 ± sqrt 58` (main's theorems, neither imported nor relied on here); that `D_2` is the parent's cone moment `D_u` of (15.1) for the reference law, and the source's Rayleigh integration route as the source's statements; 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) |
+| Side24 (`Specifications.Side24`, modules Side24Elementary, Side24Analysis, Side24Interfaces, Side24Covariance, Side24ConeMoment, Side24Images) | 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`); display (2), the image bound `\|D^q K24(0) u - D^q Kinf(0) u\| < imageConstE` for `d = 2` or `3`, every `q ≤ 6` and every unit tuple `u`, through `D^q K24(0) = θ(0)⁻¹ ∑_n D^q Kinf(24 n)`, by the term-wise derivative on the unit ball (the local exchange of `iteratedFDeriv` and `tsum` is the module's helper `Aux.ib_iteratedFDeriv_tsum_of_isOpen`, not an inventory theorem and not a Mathlib result; the hypothesis `ThetaSummable d` is not used); 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; the reference covariance lower bound: `Cref d (R 0) R - (1/3) • 1` positive semidefinite, its `IsHermitian` half included, for every orthonormal frame `R` and `d = 2` or `3`, as the Prop states it (the proof does not use that hypothesis; only the helper `Aux.cv_psd`, not an inventory theorem, is stated for every `0 < d`); the entrywise bound `\|C24 a b - Cref a b\| ≤ 2 imageConstE` and display (3), `C24 - (1 - epsilon) • Cref` and `(1 + epsilon) • Cref - C24` positive semidefinite in Mathlib's sense, `IsHermitian` included, both at `u = R 0` in an orthonormal frame `R` for `d = 2` or `3`, as the Props state them (the symmetry of `C24` through the term-wise derivative, from Mathlib's `ContDiffAt.iteratedFDeriv_comp_perm` for the analytic `Kinf d`, with the odd total orders vanishing by `n ↦ -n` and the evenness of `Kinf d`; `\|x ⬝ (C24 - Cref) x\| ≤ 26 imageConstE (x ⬝ x)` and `78 imageConstE ≤ epsilon`, not the source's `20E` and `60E < epsilon`); 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, and the `m = 2` cone moment `∫ coneIntegrand (s, x, y) ∂I.P = (1/2)(25/3 - 20/3 + 8 - 8 √(3/8))` from the law field `sxy_law` alone (not `A_law`); all as the Props state them, for the formal objects (`E d`, `Kinf`, `K24`, `thetaSum24`, `latticeVec`, `derivContraction`, `gaussDensity`, `jointCov`, `Cref`, `C24`, `coneIntegrand`, the interface structures); the reference covariance lower bound and the `m = 2` cone moment (round 5) are first receipted by run 38195810463 (PR head `c6ce0256`, actual tested merge `1320c5b2…` with base `be014794…`; receipt theorem_count 75); the image bound, the entrywise bound and display (3) (round 6, module Side24Images) are first receipted by run 38277458954 (PR head `9e305ea5`, actual tested merge `1376175c…` with base `a0323b94…`, the tested merge differing from the head only outside both packets; receipt theorem_count 78) | 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; any image bound for `q > 6` or `d ∉ {2, 3}`; differentiability of `K24` as a statement (used only inside the proofs, on the unit ball); the spectral-norm bound `20E` (not specified) and the source's route through it and `60E < epsilon` (not reproduced; main's `UniversalLaw.Side24.covariance_relative_bound` is neither imported, cited nor relied on); the passage to marginal and conditional covariances (not specified); 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, `Cref` or `C24` is the covariance of a random object; symmetry of `Cref d u R` for a general `u` or frame; the odd-block minors and eigenvalues `8 ± sqrt 58` (main's theorems, neither imported nor relied on here); that `D_2` is the parent's cone moment `D_u` of (15.1) for the reference law, and the source's Rayleigh integration route as the source's statements; 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 |
 

specifications/lean_statement_proofs_20261011/SpecificationProofs.lean

@@ -11,3 +11,4 @@ import SpecificationProofs.Side24Interfaces
 import SpecificationProofs.RNCluster
 import SpecificationProofs.Side24Covariance
 import SpecificationProofs.Side24ConeMoment
+import SpecificationProofs.Side24Images