Proof packet round 3: Theorem F's hazard interpolation (F4-F8, F12, F2) and the F3 enclosure (8 theorems; source-bound hosted receipt recorded; alignment pending)

specifications/lean_statement_proofs_20261011/README.md

@@ -43,17 +43,15 @@ register gives it.
 
 ## Registered Props without a theorem here, and why
 
-Inventory at this commit: 52 theorems, 51 of the 141 registered `def … : Prop` declarations (`TriangleNeedsThree`
-is proved twice). The other 90 fall into the groups below. None is weakened, restated or relabelled: the register
+Inventory at this commit: 60 theorems, 59 of the 141 registered `def … : Prop` declarations (`TriangleNeedsThree`
+is proved twice). The other 82 fall into the groups below. None is weakened, restated or relabelled: the register
 keeps every one at `specified`, and a group's reason is a statement about what Mathlib and this packet can reach
 today, not about the truth of the Prop.
 
 | group | Props (names without `UniversalLaw.Spec.<Module>.`) | why no theorem here |
 |---|---|---|
 | P15 parametrised predicates | `IsRealizedFamily`, `IsGood`, `IsKDecomposable`, `IsGeneratorCover`, `IsPaletteFeasible`, `IsMinimalForbidden`, `IsTransversal`, `IsProperDownset` | predicates with free arguments, not closed statements: a theorem of their type would assert them for every argument, which is false (`IsGood F Finset.univ` fails for every realized family). They are the vocabulary of the other Props, not targets. |
-| P15 hazard interpolation (full-price note Section 2) | `CoordinatewiseConcavity`, `HazardProductBound` (F6), `HazardPhiBound` (F7), `FullGroundPriceBound` (F8), `FullGroundBudgetIff` | need the concavity of `t ↦ -log μ_{p(t)}(A)`, `p_i(t) = 1 - e^{-t_i}`, in each coordinate, i.e. the derivative formulas (F4)-(F5) that the source does not display and the statement packet does not specify; a real-analysis development (differentiability of finite exponential sums, sign of the second derivative) with no Mathlib shortcut. (F7), (F8) and the `iff` are its consequences. |
-| P15 full budget | `LocalPriceBoundFull` (F12), `FullTransformedPriceBudget` (F2) | (F12) is (F8) applied to each block's capacity family together with `H_(n,a) ≥ h_star` (`CapacityWorstCase`, proved) and `rho_star = 1/h_star`; (F2) assembles (F12) through (F13) (`GlobalAssemblyHazard`, proved) and the cover criterion (`FullBlockCoverIff`, proved). Both wait on the group above. |
-| P15 enclosure | `RhoStarEnclosure` (F3) | twenty decimal digits of `1/(3 - log(3e - 2))`: needs certified `exp` and `log` enclosures far beyond Mathlib's nine-digit `Real.exp_one_lt_d9`; a proof-producing interval pipeline (Taylor remainders at some twenty-five terms in exact rationals) is the route. `RhoStarBelowSixSevenths` and `SixSeventhsCertificate` (proved) are the coarse version. |
+| P15 full-price note, formerly listed here | — | the hazard interpolation `CoordinatewiseConcavity`, `HazardProductBound` (F6), `HazardPhiBound` (F7), `FullGroundPriceBound` (F8), `FullGroundBudgetIff`, the full budget `LocalPriceBoundFull` (F12), `FullTransformedPriceBudget` (F2) and the enclosure `RhoStarEnclosure` (F3) have theorems in `P15Interpolation` since round 3: the concavity from the one-coordinate split of `μ_p(A)` (affine in `e^{-t_i}`, coefficients `0 ≤ S_in ≤ S_out` for a downset) and `concaveOn_of_deriv2_nonpos`, not from the undisplayed derivative formulas (F4)-(F5), which stay unspecified; (F6)-(F8), (F12) and (F2) as their consequences through `CapacityWorstCase`, `GlobalAssemblyHazard` and `FullBlockCoverIff`; (F3) by `Real.exp_bound` at degrees 26 and 16 compared by `norm_num` against the 20-digit rationals, a different certificate from the source's `full_price.py` procedure, which stays unspecified. Every theorem-shaped Prop of claim `p15-full-price` now has a theorem; the claim stays `specified`. |
 | Side24 derivative bounds | `IsUnitTuple` (predicate), `DerivativePairingBound`, `DerivativeBoundAtLeastOne`, `DerivativeBoundAtZero` | explicit `iteratedFDeriv ℝ q (fun x => exp (-‖x‖² / 2))` in arbitrary unit directions: Mathlib has no closed form for the iterated Fréchet derivatives of a Gaussian (the Hermite expansion behind the pairing sums); the arithmetic of the pairing sums is kernel-proved on main (`UniversalLaw.Side24.pairing_sum_six`, …). |
 | Side24 lattice sums | `ThetaSummable`, `LatticeImageSumBound`, `ImageBound` | summability of `n ↦ exp (-‖z + 24 n‖² / 2)` over `Fin d → ℤ` and the explicit tail `≤ 1458 e^{-288}`: Gaussian-decay summability over `ℤ^d` and a shell count; Mathlib's Jacobi-theta results are one-dimensional. |
 | Side24 covariance and density | `NegDefCone` (predicate), `ReferenceOddAndPinBlocks`, `CovarianceOrdering`, `EntrywiseCovarianceBound`, `ReferenceCovarianceLowerBound`, `DensityComparison`, `IntegrandRatioBounds`, `ReferencePinDensityProduct` | built on the derivative contractions above (`jointCov`, `gradCov`, `pinCov`, `derivContraction`); the matrix arithmetic is kernel-proved on main, the evaluation of the Fréchet derivatives is not available. |
@@ -69,8 +67,9 @@ The register (`../lean_statements_20261010/REGISTER.json`) says the same per cla
 README.md  SCOPE.md  check.py  test_check.py  replay.sh
 lakefile.toml  lean-toolchain  lake-manifest.json  SpecificationProofs.lean
 SpecificationProofs/<Module>.lean      namespace UniversalLaw.Proofs.<Module>; P15 is split by theme into
-                                       P15Elementary, P15Structure, P15Hazard, P15Covers, P15Budget (in
-                                       import order), Side24Elementary and RNProbability are one each
+                                       P15Elementary, P15Structure, P15Hazard, P15Covers, P15Budget,
+                                       P15Interpolation (in import order), Side24Elementary and RNProbability
+                                       are one each
 ```
 
 Rules for every module (enforced by `check.py`, see its module docstring):

specifications/lean_statement_proofs_20261011/SCOPE.md

@@ -30,7 +30,7 @@ statement proved here: **PENDING_INDEPENDENT_REVIEW**. Organizational-independen
 
 | family | the theorems establish | not established |
 |---|---|---|
-| P15 (`Specifications.P15`, modules P15Elementary, P15Structure, P15Hazard, P15Covers, P15Budget) | 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; 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 |
+| 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 |

specifications/lean_statement_proofs_20261011/SpecificationProofs.lean

@@ -5,3 +5,4 @@ import SpecificationProofs.P15Covers
 import SpecificationProofs.P15Budget
 import SpecificationProofs.Side24Elementary
 import SpecificationProofs.RNProbability
+import SpecificationProofs.P15Interpolation