diff --git a/specifications/lean_statement_proofs_20261011/README.md b/specifications/lean_statement_proofs_20261011/README.md index 19978b48c..2ed4c371c 100644 --- a/specifications/lean_statement_proofs_20261011/README.md +++ b/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..`) | 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/.lean namespace UniversalLaw.Proofs.; 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): diff --git a/specifications/lean_statement_proofs_20261011/SCOPE.md b/specifications/lean_statement_proofs_20261011/SCOPE.md index e60a08579..523a53d27 100644 --- a/specifications/lean_statement_proofs_20261011/SCOPE.md +++ b/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 | diff --git a/specifications/lean_statement_proofs_20261011/SpecificationProofs.lean b/specifications/lean_statement_proofs_20261011/SpecificationProofs.lean index 7ad5fd68a..43685b383 100644 --- a/specifications/lean_statement_proofs_20261011/SpecificationProofs.lean +++ b/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 diff --git a/specifications/lean_statement_proofs_20261011/SpecificationProofs/P15Interpolation.lean b/specifications/lean_statement_proofs_20261011/SpecificationProofs/P15Interpolation.lean new file mode 100644 index 000000000..ff4dbea66 --- /dev/null +++ b/specifications/lean_statement_proofs_20261011/SpecificationProofs/P15Interpolation.lean @@ -0,0 +1,1183 @@ +import Specifications.P15 +import SpecificationProofs.P15Elementary +import SpecificationProofs.P15Hazard +import SpecificationProofs.P15Covers +import SpecificationProofs.P15Budget + +/-! +# P15 interpolation proofs: Theorem F's hazard interpolation (displays (F4)-(F8), (F12), (F2)) +and the (F3) enclosure of `rho_star` + +Scientific effect: NONE. Organizational-independence credit: 0 (Anthropic / Claude). + +Every theorem outside the `Aux` namespace has as its type exactly one registered `Prop` of +`Specifications/P15.lean` (statement packet `specifications/lean_statements_20261010`, which is +not modified here). A kernel-checked proof of such a `Prop` is evidence about that `Prop` only: +it does not make the informal Layer 0 note reviewed, accepted or "verified", it does not +identify the formal definitions with the informal objects (that alignment is +PENDING_INDEPENDENT_REVIEW), and it promotes, closes, discharges or reclassifies nothing. + +Helper lemmas live in `UniversalLaw.Proofs.P15Interpolation.Aux`, tagged by the display they +serve (`f3_`, `cc_`, `f6_`, `f7_`, `f8_`, `bi_`, `lp_`, `f2_`); the gate inventories only the +eight theorems outside that namespace. The mathematics, in the order of the module: + +* (F3) `rhoStarLower < rho_star < rhoStarUpper < 6/7`, with `rho_star = 1 / (3 - log(3e - 2))`. + Exact rational arithmetic throughout: `rho_star < U` iff `3e - 2 < exp(3 - 1/U)` and + `L < rho_star` iff `exp(3 - 1/L) < 3e - 2`; writing `3 - 1/U = 2 + x_U` with `|x_U| < 1/5`, + `exp(3 - 1/U) = (exp 1)^2 exp x_U`, and `Real.exp_bound` at degree 26 (for `e`) and degree 16 + (for `exp x_U`, `exp x_L`) gives rational enclosures that `norm_num` compares against the + decimal literals (margins about `1.08 * 10^-20` and `7.53 * 10^-20`). +* (F4), (F5) The split of `mu_p(A)` at one coordinate: with `p_i` replaced by `x`, + `mu(A) = x S_in + (1 - x) S_out`, where `S_in`, `S_out` are the sums, over the members of `A` + containing, respectively avoiding, the coordinate, of the weight over the other coordinates. + For a downset `S_in ≤ S_out` (erasing the coordinate injects the first family into the second + and preserves the reduced weight) and `S_out > 0` once `∅ ∈ A` and every other `p_j < 1`. + With `x = 1 - exp(-s)` this is `S_in + (S_out - S_in) exp(-s)`, and `s ↦ -log(a + b exp(-s))` + with `a, b ≥ 0`, `a + b > 0` has second derivative `-a b exp(-s) / (a + b exp(-s))^2 ≤ 0` + (`concaveOn_of_deriv2_nonpos`): separate coordinatewise concavity of the hazard `F_A`. +* (F6) The chord inequality of that concavity on `[0,1]`, `f(s) ≥ (1 - s) f(0) + s f(1) ≥ s f(1)` + since `f(0) = -log mu ≥ 0`, iterated over the coordinates (`Finset.induction_on`, raising one + coordinate to `1` at a time): `(prod_i t_i) H_A ≤ F_A(t)`, as `F_A(1, …, 1) = H_A`. +* (F7) For `p` in the cube put `t_i := phi(p_i) ∈ [0,1]` and `p'_i := 1 - exp(-t_i) ≤ p_i`; + `mu(A)` is antitone in the probability vector for a downset (the same split), so + `-log mu_p(A) ≥ -log mu_p'(A) = F_A(t) ≥ (prod_i phi(p_i)) H_A`. +* (F8) `prod_i c_i ≤ prod_i phi(p_i) ≤ 1` for `0 ≤ c_i ≤ phi(p_i)`, and when `mu_p(A) > 0`, + `prod_i phi(p_i) ≤ (1/H_A) [-log mu_p(A)]` by (F7) with `H_A > 0`; the exactness remark: the + capped budget at `rho = 1` holds for all admissible `p, c` iff `H_A ≥ 1` (the (⇒) direction + instantiates `p ≡ p_star`, `c ≡ 1`, admissible since `phi p_star = 1`). +* (F12) Each block `X_i` of a realized family is enumerated by `Fin n_i`, `n_i = a_i d_i + 1`; + along the enumeration `mu_p(D_i)` is the product measure of the capacity family + `{T : |T| ≤ a_i}` (`LocalRestriction`), a proper downset, so (F7) and `CapacityWorstCase` + (`h_star ≤ H_{n_i, a_i}`) give `price(X_i) ≤ rho_star [-log mu_p(D_i)]` and `price(X_i) ≤ 1`. +* (F2) `covercost ≤ 1` (the cover `{∅}`); for `K ≥ K_H(d)` the full blocks cover, so + `covercost ≤ sum_i price(X_i) ≤ rho_star sum_i [-log mu_p(D_i)] ≤ rho_star [-log mu_p(D)]` + by (F12) and the global assembly (F13), `P15Hazard.globalAssemblyHazard`. +-/ + +namespace UniversalLaw.Proofs.P15Interpolation + +open UniversalLaw.Spec.P15 + +namespace Aux + +/-! ## (F3) The enclosure of `rho_star` + +### A 29-decimal enclosure of `e` from the degree-26 Taylor bound -/ + +/-- `2.71828182845904523536028746620 < e`: the 26-term Taylor sum of `exp 1` minus the tail bound +`27 / (26! * 26)` of `Real.exp_bound`, evaluated exactly by `norm_num`. -/ +theorem f3_exp_one_gt : (271828182845904523536028746620 : ℝ) / 10 ^ 29 < Real.exp 1 := by + have h := Real.exp_bound (x := (1 : ℝ)) (by simp) (n := 26) (by norm_num) + rw [abs_sub_le_iff] at h + obtain ⟨-, h2⟩ := h + norm_num [Finset.sum_range_succ] at h2 + linarith + +/-- `e < 2.71828182845904523536028747136`: the 26-term Taylor sum of `exp 1` plus the tail bound +`27 / (26! * 26)` of `Real.exp_bound`, evaluated exactly by `norm_num`. -/ +theorem f3_exp_one_lt : Real.exp 1 < (271828182845904523536028747136 : ℝ) / 10 ^ 29 := by + have h := Real.exp_bound (x := (1 : ℝ)) (by simp) (n := 26) (by norm_num) + rw [abs_sub_le_iff] at h + obtain ⟨h1, -⟩ := h + norm_num [Finset.sum_range_succ] at h1 + linarith + +/-! ### Degree-16 Taylor enclosures of `exp x_U` and `exp x_L` + +`x_U = 1 - 1/rhoStarUpper = -3863004568775331983 / 21136995431224668017` (reduced) and +`x_L = 1 - 1/rhoStarLower = -15452018275101327933 / 84547981724898672067`, both about `-0.18276`. -/ + +/-- Lower bound `0.83296775704110158100003160908803 ≤ exp x_U` from `Real.exp_bound` at degree 16. -/ +theorem f3_exp_xU_ge : + (83296775704110158100003160908803 : ℝ) / 10 ^ 32 ≤ + Real.exp (-3863004568775331983 / 21136995431224668017) := by + have hx : |(-3863004568775331983 / 21136995431224668017 : ℝ)| ≤ 1 := + abs_le.mpr ⟨by norm_num, by norm_num⟩ + have h := Real.exp_bound hx (n := 16) (by norm_num) + rw [abs_sub_le_iff] at h + obtain ⟨-, h2⟩ := h + norm_num [Finset.sum_range_succ] at h2 + linarith + +/-- Upper bound `exp x_L ≤ 0.83296775704110158098837919695330` from `Real.exp_bound` at degree 16. -/ +theorem f3_exp_xL_le : + Real.exp (-15452018275101327933 / 84547981724898672067) ≤ + (83296775704110158098837919695330 : ℝ) / 10 ^ 32 := by + have hx : |(-15452018275101327933 / 84547981724898672067 : ℝ)| ≤ 1 := + abs_le.mpr ⟨by norm_num, by norm_num⟩ + have h := Real.exp_bound hx (n := 16) (by norm_num) + rw [abs_sub_le_iff] at h + obtain ⟨h1, -⟩ := h + norm_num [Finset.sum_range_succ] at h1 + linarith + +/-! ### The two logarithmic inequalities -/ + +/-- `log(3e - 2) < 2 + x_U = 3 - 1/rhoStarUpper`: equivalently `3e - 2 < (exp 1)^2 * exp x_U`, +with `e` and `exp x_U` replaced by their rational bounds (`norm_num` margin about `1.08e-20`). -/ +theorem f3_log_lt : + Real.log (3 * Real.exp 1 - 2) < 2 + (-3863004568775331983 / 21136995431224668017 : ℝ) := by + rw [Real.log_lt_iff_lt_exp P15Elementary.Aux.three_exp_sub_two_pos, Real.exp_add, + P15Elementary.Aux.exp_two_eq] + have he_lo := f3_exp_one_gt + have he_hi := f3_exp_one_lt + have hx := f3_exp_xU_ge + have hsq : ((271828182845904523536028746620 : ℝ) / 10 ^ 29) ^ 2 ≤ Real.exp 1 ^ 2 := + pow_le_pow_left₀ (by norm_num) he_lo.le 2 + have hprod : ((271828182845904523536028746620 : ℝ) / 10 ^ 29) ^ 2 * + ((83296775704110158100003160908803 : ℝ) / 10 ^ 32) ≤ + Real.exp 1 ^ 2 * Real.exp (-3863004568775331983 / 21136995431224668017) := + mul_le_mul hsq hx (by norm_num) (sq_nonneg _) + have key : 3 * ((271828182845904523536028747136 : ℝ) / 10 ^ 29) - 2 < + ((271828182845904523536028746620 : ℝ) / 10 ^ 29) ^ 2 * + ((83296775704110158100003160908803 : ℝ) / 10 ^ 32) := by + norm_num + linarith + +/-- `2 + x_L = 3 - 1/rhoStarLower < log(3e - 2)`: equivalently `(exp 1)^2 * exp x_L < 3e - 2`, +with `e` and `exp x_L` replaced by their rational bounds (`norm_num` margin about `7.53e-20`). -/ +theorem f3_lt_log : + 2 + (-15452018275101327933 / 84547981724898672067 : ℝ) < Real.log (3 * Real.exp 1 - 2) := by + rw [Real.lt_log_iff_exp_lt P15Elementary.Aux.three_exp_sub_two_pos, Real.exp_add, + P15Elementary.Aux.exp_two_eq] + have he_lo := f3_exp_one_gt + have he_hi := f3_exp_one_lt + have hx := f3_exp_xL_le + have hsq : Real.exp 1 ^ 2 ≤ ((271828182845904523536028747136 : ℝ) / 10 ^ 29) ^ 2 := + pow_le_pow_left₀ (Real.exp_pos 1).le he_hi.le 2 + have hprod : Real.exp 1 ^ 2 * Real.exp (-15452018275101327933 / 84547981724898672067) ≤ + ((271828182845904523536028747136 : ℝ) / 10 ^ 29) ^ 2 * + ((83296775704110158098837919695330 : ℝ) / 10 ^ 32) := + mul_le_mul hsq hx (Real.exp_pos _).le (by norm_num) + have key : ((271828182845904523536028747136 : ℝ) / 10 ^ 29) ^ 2 * + ((83296775704110158098837919695330 : ℝ) / 10 ^ 32) < + 3 * ((271828182845904523536028746620 : ℝ) / 10 ^ 29) - 2 := by + norm_num + linarith + +/-! ### The three conjuncts of (F3) -/ + +/-- `0 < h_star` written out, from `one_lt_hStar`. -/ +theorem f3_hStar_pos : (0 : ℝ) < 3 - Real.log (3 * Real.exp 1 - 2) := by + have h := P15Elementary.Aux.one_lt_hStar + unfold hStar at h + linarith + +/-- `rho_star < rhoStarUpper`. -/ +theorem f3_rhoStar_lt_upper : rhoStar < rhoStarUpper := by + unfold rhoStar rhoStarUpper + rw [div_lt_iff₀ f3_hStar_pos] + have h := f3_log_lt + linarith + +/-- `rhoStarLower < rho_star`. -/ +theorem f3_lower_lt_rhoStar : rhoStarLower < rhoStar := by + unfold rhoStar rhoStarLower + rw [lt_div_iff₀ f3_hStar_pos] + have h := f3_lt_log + linarith + +/-- `rhoStarUpper < 6/7`, a rational inequality. -/ +theorem f3_upper_lt_six_sevenths : rhoStarUpper < 6 / 7 := by + unfold rhoStarUpper + norm_num + +open Finset + +/-! ## (F4), (F5) The split of the product weight at one coordinate and separate concavity -/ + +/-- The weight of `U` over the coordinates other than `i`: `prod_{v in U, v ≠ i} p_v * +prod_{v notin U, v ≠ i} (1 - p_v)`. -/ +noncomputable def cc_wOther {Y : Type} [Fintype Y] [DecidableEq Y] (p : Y → ℝ) (i : Y) + (U : Finset Y) : ℝ := + (∏ v ∈ U.erase i, p v) * ∏ v ∈ (univ \ U).erase i, (1 - p v) + +/-- The reduced weight is nonnegative when every `p_v` lies in `[0, 1]`. -/ +theorem cc_wOther_nonneg {Y : Type} [Fintype Y] [DecidableEq Y] {p : Y → ℝ} + (hp : ∀ v, 0 ≤ p v ∧ p v ≤ 1) (i : Y) (U : Finset Y) : 0 ≤ cc_wOther p i U := by + unfold cc_wOther + refine mul_nonneg (Finset.prod_nonneg fun v _ => (hp v).1) (Finset.prod_nonneg fun v _ => ?_) + linarith [(hp v).2] + +/-- The reduced weight of the empty set is positive when every `p_v < 1`. -/ +theorem cc_wOther_empty_pos {Y : Type} [Fintype Y] [DecidableEq Y] {p : Y → ℝ} + (hp : ∀ v, p v < 1) (i : Y) : 0 < cc_wOther p i ∅ := by + unfold cc_wOther + rw [Finset.erase_empty, Finset.prod_empty, one_mul] + exact Finset.prod_pos fun v _ => by linarith [hp v] + +/-- Erasing the distinguished coordinate does not change the reduced weight. -/ +theorem cc_wOther_erase {Y : Type} [Fintype Y] [DecidableEq Y] (p : Y → ℝ) (i : Y) + (U : Finset Y) : cc_wOther p i (U.erase i) = cc_wOther p i U := by + unfold cc_wOther + have h1 : (U.erase i).erase i = U.erase i := Finset.erase_idem + have h2 : (univ \ U.erase i).erase i = (univ \ U).erase i := by + ext v + simp only [mem_erase, mem_sdiff, mem_univ, true_and] + tauto + rw [h1, h2] + +/-- A finite product splits off the factor at `i` when `i` belongs to the index set. -/ +theorem cc_prod_split_at {Y : Type} [DecidableEq Y] (s : Finset Y) (f : Y → ℝ) (i : Y) : + ∏ v ∈ s, f v = (if i ∈ s then f i else 1) * ∏ v ∈ s.erase i, f v := by + by_cases h : i ∈ s + · rw [ite_eq_left h, Finset.mul_prod_erase s f h] + · rw [ite_eq_right h, one_mul, Finset.erase_eq_of_notMem h] + +/-- The weight of `U` under `p` with coordinate `i` replaced by `x`: the factor at `i` is +`x` or `1 - x` according to `i ∈ U`, times the reduced weight. -/ +theorem cc_weight_update {Y : Type} [Fintype Y] [DecidableEq Y] (p : Y → ℝ) (i : Y) (x : ℝ) + (U : Finset Y) : + weight (Function.update p i x) U = (if i ∈ U then x else 1 - x) * cc_wOther p i U := by + unfold weight cc_wOther + have h1 := cc_prod_split_at U (Function.update p i x) i + have h2 := cc_prod_split_at (univ \ U) (fun v => 1 - Function.update p i x v) i + simp only [Function.update_self] at h1 h2 + have e1 : ∏ v ∈ U.erase i, Function.update p i x v = ∏ v ∈ U.erase i, p v := + Finset.prod_congr rfl (fun v hv => Function.update_of_ne (ne_of_mem_erase hv) x p) + have e2 : ∏ v ∈ (univ \ U).erase i, (1 - Function.update p i x v) + = ∏ v ∈ (univ \ U).erase i, (1 - p v) := + Finset.prod_congr rfl (fun v hv => by rw [Function.update_of_ne (ne_of_mem_erase hv)]) + rw [h1, h2, e1, e2] + by_cases hi : i ∈ U + · have hi' : i ∉ univ \ U := by simp [hi] + rw [ite_eq_left hi, ite_eq_right hi', ite_eq_left hi] + ring + · have hi' : i ∈ univ \ U := by simp [hi] + rw [ite_eq_right hi, ite_eq_left hi', ite_eq_right hi] + ring + +/-- Display (F4): the split of `mu_p(A)` at coordinate `i`, for any family `A` (general finite +ground type). -/ +theorem cc_muOf_update {Y : Type} [Fintype Y] [DecidableEq Y] (A : Finset (Finset Y)) + (p : Y → ℝ) (i : Y) (x : ℝ) : + muOf A (Function.update p i x) = + x * ∑ U ∈ A.filter (fun U => i ∈ U), cc_wOther p i U + + (1 - x) * ∑ U ∈ A.filter (fun U => i ∉ U), cc_wOther p i U := by + unfold muOf + simp only [cc_weight_update, ite_mul] + rw [Finset.sum_ite, Finset.mul_sum, Finset.mul_sum] + +/-- For a downset, the sum over the members containing `i` is at most the sum over the members +avoiding `i` (`U ↦ U.erase i` injects the first into the second and preserves `cc_wOther`). -/ +theorem cc_sum_in_le_sum_out {Y : Type} [Fintype Y] [DecidableEq Y] {A : Finset (Finset Y)} + (hA : ∀ U ∈ A, ∀ V : Finset Y, V ⊆ U → V ∈ A) {p : Y → ℝ} + (hp : ∀ v, 0 ≤ p v ∧ p v ≤ 1) (i : Y) : + ∑ U ∈ A.filter (fun U => i ∈ U), cc_wOther p i U + ≤ ∑ U ∈ A.filter (fun U => i ∉ U), cc_wOther p i U := by + have hinj : Set.InjOn (fun U : Finset Y => U.erase i) + (A.filter (fun U => i ∈ U) : Set (Finset Y)) := by + intro U hU V hV hUV + have hU' : i ∈ U := (Finset.mem_filter.1 (Finset.mem_coe.1 hU)).2 + have hV' : i ∈ V := (Finset.mem_filter.1 (Finset.mem_coe.1 hV)).2 + exact Finset.erase_injOn' i hU' hV' hUV + have himg : (A.filter (fun U => i ∈ U)).image (fun U => U.erase i) + ⊆ A.filter (fun U => i ∉ U) := by + intro V hV + rw [Finset.mem_image] at hV + obtain ⟨U, hU, rfl⟩ := hV + rw [Finset.mem_filter] at hU ⊢ + exact ⟨hA U hU.1 _ (Finset.erase_subset i U), Finset.notMem_erase i U⟩ + calc ∑ U ∈ A.filter (fun U => i ∈ U), cc_wOther p i U + = ∑ U ∈ A.filter (fun U => i ∈ U), cc_wOther p i (U.erase i) := + Finset.sum_congr rfl (fun U _ => (cc_wOther_erase p i U).symm) + _ = ∑ V ∈ (A.filter (fun U => i ∈ U)).image (fun U => U.erase i), cc_wOther p i V := + (Finset.sum_image hinj).symm + _ ≤ ∑ U ∈ A.filter (fun U => i ∉ U), cc_wOther p i U := + Finset.sum_le_sum_of_subset_of_nonneg himg (fun U _ _ => cc_wOther_nonneg hp i U) + +/-- The sum over the members avoiding `i` is positive once `∅ ∈ A` and every `p_v < 1`. -/ +theorem cc_sum_out_pos {Y : Type} [Fintype Y] [DecidableEq Y] {A : Finset (Finset Y)} + (h0 : ∅ ∈ A) {p : Y → ℝ} (hp : ∀ v, 0 ≤ p v ∧ p v < 1) (i : Y) : + 0 < ∑ U ∈ A.filter (fun U => i ∉ U), cc_wOther p i U := by + have hmem : ∅ ∈ A.filter (fun U => i ∉ U) := + Finset.mem_filter.2 ⟨h0, Finset.notMem_empty i⟩ + have hp1 : ∀ v, 0 ≤ p v ∧ p v ≤ 1 := fun v => ⟨(hp v).1, (hp v).2.le⟩ + exact lt_of_lt_of_le (cc_wOther_empty_pos (fun v => (hp v).2) i) + (Finset.single_le_sum (fun U _ => cc_wOther_nonneg hp1 i U) hmem) + +/-- `mu_p(A)` is antitone in each coordinate for a downset and `p` in the cube. -/ +theorem cc_muOf_update_antitone {Y : Type} [Fintype Y] [DecidableEq Y] {A : Finset (Finset Y)} + (hA : ∀ U ∈ A, ∀ V : Finset Y, V ⊆ U → V ∈ A) {p : Y → ℝ} + (hp : ∀ v, 0 ≤ p v ∧ p v ≤ 1) (i : Y) {x y : ℝ} (hxy : x ≤ y) : + muOf A (Function.update p i y) ≤ muOf A (Function.update p i x) := by + rw [cc_muOf_update, cc_muOf_update] + have h := cc_sum_in_le_sum_out hA hp i + nlinarith [mul_nonneg (sub_nonneg.2 hxy) (sub_nonneg.2 h)] + +/-! ### The one-variable function `s ↦ -log(a + b exp(-s))` (display (F5)) -/ + +/-- `a + b exp(-s) > 0` for `a, b ≥ 0` with `a + b > 0`. -/ +theorem cc_affineExp_pos {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : 0 < a + b) (s : ℝ) : + 0 < a + b * Real.exp (-s) := by + have he := Real.exp_pos (-s) + rcases lt_or_eq_of_le ha with ha' | ha' + · have : 0 ≤ b * Real.exp (-s) := mul_nonneg hb he.le + linarith + · have hb' : 0 < b := by linarith + have := mul_pos hb' he + linarith + +/-- First derivative: `d/ds (-log(a + b e^{-s})) = b e^{-s} / (a + b e^{-s})`. -/ +theorem cc_hasDerivAt_negLog {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : 0 < a + b) (s : ℝ) : + HasDerivAt (fun x => -Real.log (a + b * Real.exp (-x))) + (b * Real.exp (-s) / (a + b * Real.exp (-s))) s := by + have hpos := cc_affineExp_pos ha hb hab s + have h1 : HasDerivAt (fun x : ℝ => a + b * Real.exp (-x)) (b * (Real.exp (-s) * -1)) s := + ((hasDerivAt_neg' (x := s)).exp.const_mul b).const_add a + have h2 := (h1.log hpos.ne').neg + exact h2.congr_deriv (by ring) + +/-- Second derivative: `d/ds (b e^{-s} / (a + b e^{-s})) = -a b e^{-s} / (a + b e^{-s})^2`. -/ +theorem cc_hasDerivAt_ratio {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : 0 < a + b) (s : ℝ) : + HasDerivAt (fun x => b * Real.exp (-x) / (a + b * Real.exp (-x))) + (-(a * b * Real.exp (-s)) / (a + b * Real.exp (-s)) ^ 2) s := by + have hpos := cc_affineExp_pos ha hb hab s + have hnum : HasDerivAt (fun x : ℝ => b * Real.exp (-x)) (b * (Real.exp (-s) * -1)) s := + (hasDerivAt_neg' (x := s)).exp.const_mul b + have hden : HasDerivAt (fun x : ℝ => a + b * Real.exp (-x)) (b * (Real.exp (-s) * -1)) s := + hnum.const_add a + have h := hnum.div hden hpos.ne' + exact h.congr_deriv (by ring) + +/-- Display (F5), one variable: `s ↦ -log(a + b exp(-s))` is concave on `[0, 1]` for +`a, b ≥ 0`, `a + b > 0` (`concaveOn_of_deriv2_nonpos`). -/ +theorem cc_concaveOn_negLog {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : 0 < a + b) : + ConcaveOn ℝ (Set.Icc (0 : ℝ) 1) (fun s => -Real.log (a + b * Real.exp (-s))) := by + have hd1 := cc_hasDerivAt_negLog ha hb hab + have hd2 := cc_hasDerivAt_ratio ha hb hab + have hderiv : deriv (fun s => -Real.log (a + b * Real.exp (-s))) + = fun s => b * Real.exp (-s) / (a + b * Real.exp (-s)) := by + funext s + exact (hd1 s).deriv + refine concaveOn_of_deriv2_nonpos (convex_Icc 0 1) ?_ ?_ ?_ ?_ + · exact fun s _ => (hd1 s).continuousAt.continuousWithinAt + · exact fun s _ => (hd1 s).differentiableAt.differentiableWithinAt + · rw [hderiv] + exact fun s _ => (hd2 s).differentiableAt.differentiableWithinAt + · intro s _ + show deriv (deriv (fun s => -Real.log (a + b * Real.exp (-s)))) s ≤ 0 + rw [hderiv, (hd2 s).deriv] + apply div_nonpos_of_nonpos_of_nonneg + · have : 0 ≤ a * b * Real.exp (-s) := mul_nonneg (mul_nonneg ha hb) (Real.exp_pos _).le + linarith + · exact sq_nonneg _ + +/-! ### Assembly of (F5) -/ + +/-- `F_A(t[i := s])` is `-log mu(A)` at `p(t)` with coordinate `i` replaced by `1 - exp(-s)`. -/ +theorem cc_hazardCoord_update_eq {Y : Type} [Fintype Y] [DecidableEq Y] + (A : Finset (Finset Y)) (t : Y → ℝ) (i : Y) (s : ℝ) : + hazardCoord A (Function.update t i s) = + -Real.log (muOf A (Function.update (fun j => 1 - Real.exp (-t j)) i + (1 - Real.exp (-s)))) := by + unfold hazardCoord + have h : (fun j => 1 - Real.exp (-(Function.update t i s j))) + = Function.update (fun j => 1 - Real.exp (-t j)) i (1 - Real.exp (-s)) := by + funext j + by_cases hj : j = i + · subst hj + simp + · rw [Function.update_of_ne hj, Function.update_of_ne hj] + rw [h] + +/-- Display (F5) on a general finite ground type: for a downset containing `∅` and `t` in the +cube, `s ↦ F_A(t[i := s])` is concave on `[0, 1]`. -/ +theorem cc_concaveOn_hazardCoord_update {Y : Type} [Fintype Y] [DecidableEq Y] + {A : Finset (Finset Y)} (h0 : ∅ ∈ A) (hdown : ∀ U ∈ A, ∀ V : Finset Y, V ⊆ U → V ∈ A) + (i : Y) (t : Y → ℝ) (ht : ∀ j, 0 ≤ t j ∧ t j ≤ 1) : + ConcaveOn ℝ (Set.Icc (0 : ℝ) 1) (fun s : ℝ => hazardCoord A (Function.update t i s)) := by + obtain ⟨p, hp_def⟩ : ∃ p : Y → ℝ, p = fun j => 1 - Real.exp (-t j) := ⟨_, rfl⟩ + have hp : ∀ v, 0 ≤ p v ∧ p v < 1 := by + intro v + rw [hp_def] + show 0 ≤ 1 - Real.exp (-t v) ∧ 1 - Real.exp (-t v) < 1 + have h1 := (ht v).1 + have he : Real.exp (-t v) ≤ 1 := by + rw [Real.exp_le_one_iff] + linarith + have he' : 0 < Real.exp (-t v) := Real.exp_pos _ + constructor <;> linarith + have hp1 : ∀ v, 0 ≤ p v ∧ p v ≤ 1 := fun v => ⟨(hp v).1, (hp v).2.le⟩ + have hle := cc_sum_in_le_sum_out hdown hp1 i + have hpos := cc_sum_out_pos h0 hp i + have hSin0 : 0 ≤ ∑ U ∈ A.filter (fun U => i ∈ U), cc_wOther p i U := + Finset.sum_nonneg fun U _ => cc_wOther_nonneg hp1 i U + have hfun : (fun s : ℝ => hazardCoord A (Function.update t i s)) = + fun s => -Real.log ((∑ U ∈ A.filter (fun U => i ∈ U), cc_wOther p i U) + + ((∑ U ∈ A.filter (fun U => i ∉ U), cc_wOther p i U) + - ∑ U ∈ A.filter (fun U => i ∈ U), cc_wOther p i U) * Real.exp (-s)) := by + funext s + rw [cc_hazardCoord_update_eq, ← hp_def, cc_muOf_update] + rw [show ∀ x Sin Sout : ℝ, (1 - x) * Sin + (1 - (1 - x)) * Sout = Sin + (Sout - Sin) * x + from fun x Sin Sout => by ring] + rw [hfun] + exact cc_concaveOn_negLog hSin0 (sub_nonneg.2 hle) (by linarith) + +/-! ## (F6) The hazard product bound `F_A(t) ≥ (prod_i t_i) H_A` + +### Elementary bounds on `mu_p(A)` and on the hazard `F_A` -/ + +/-- `mu_p(A) ≤ 1` for `p` in the cube: `A ⊆ univ.powerset`, the weights are nonnegative +(`weight_nonneg`) and all of them sum to one (`sum_weight_eq_one`). -/ +theorem f6_muOf_le_one {Y : Type} [Fintype Y] [DecidableEq Y] (A : Finset (Finset Y)) + {p : Y → ℝ} (hp : ∀ v, 0 ≤ p v ∧ p v ≤ 1) : muOf A p ≤ 1 := by + unfold muOf + rw [← UniversalLaw.Proofs.P15Elementary.Aux.sum_weight_eq_one p] + exact Finset.sum_le_sum_of_subset_of_nonneg + (fun U _ => Finset.mem_powerset.2 (Finset.subset_univ U)) + (fun U _ _ => UniversalLaw.Proofs.P15Budget.Aux.weight_nonneg hp U) + +/-- `0 ≤ mu_p(A)` for `p` in the cube. -/ +theorem f6_muOf_nonneg {Y : Type} [Fintype Y] [DecidableEq Y] (A : Finset (Finset Y)) + {p : Y → ℝ} (hp : ∀ v, 0 ≤ p v ∧ p v ≤ 1) : 0 ≤ muOf A p := + Finset.sum_nonneg fun U _ => UniversalLaw.Proofs.P15Budget.Aux.weight_nonneg hp U + +/-- `1 - exp(-u) ∈ [0, 1]` for `u ∈ [0, 1]` (indeed for every `u ≥ 0`). -/ +theorem f6_one_sub_exp_neg_mem {u : ℝ} (hu : 0 ≤ u ∧ u ≤ 1) : + 0 ≤ 1 - Real.exp (-u) ∧ 1 - Real.exp (-u) ≤ 1 := by + constructor + · have h : Real.exp (-u) ≤ 1 := Real.exp_le_one_iff.2 (by linarith [hu.1]) + linarith + · have h := Real.exp_pos (-u) + linarith + +/-- The coordinates `p_j(u) = 1 - exp(-u_j)` lie in the cube when `u` does. -/ +theorem f6_coords_mem {Y : Type} {u : Y → ℝ} (hu : ∀ j, 0 ≤ u j ∧ u j ≤ 1) : + ∀ v, 0 ≤ 1 - Real.exp (-u v) ∧ 1 - Real.exp (-u v) ≤ 1 := + fun v => f6_one_sub_exp_neg_mem (hu v) + +/-- `0 ≤ F_A(u)` on the cube: `-log m ≥ 0` for `0 ≤ m ≤ 1` (`Real.log_nonpos`; `log 0 = 0`, so +no positivity of `mu` is needed). -/ +theorem f6_hazardCoord_nonneg {Y : Type} [Fintype Y] [DecidableEq Y] (A : Finset (Finset Y)) + {u : Y → ℝ} (hu : ∀ j, 0 ≤ u j ∧ u j ≤ 1) : 0 ≤ hazardCoord A u := by + unfold hazardCoord + have hp := f6_coords_mem hu + have h := Real.log_nonpos (f6_muOf_nonneg A hp) (f6_muOf_le_one A hp) + linarith + +/-- `F_A(1, …, 1) = H_A`, since `1 - exp(-1) = p_star`. -/ +theorem f6_hazardCoord_one {Y : Type} [Fintype Y] [DecidableEq Y] (A : Finset (Finset Y)) : + hazardCoord A (fun _ => (1 : ℝ)) = hazardStar A := by + unfold hazardCoord hazardStar pStar + rfl + +/-! ### The chord inequality and its iteration -/ + +/-- Chord inequality at one coordinate: if `s ↦ F_A(update u i s)` is concave on `[0, 1]` and +`u` lies in the cube, then `u_i · F_A(update u i 1) ≤ F_A(u)`. -/ +theorem f6_chord {Y : Type} [Fintype Y] [DecidableEq Y] (A : Finset (Finset Y)) (i : Y) + (u : Y → ℝ) (hu : ∀ j, 0 ≤ u j ∧ u j ≤ 1) + (hconc : ConcaveOn ℝ (Set.Icc (0 : ℝ) 1) + (fun s : ℝ => hazardCoord A (Function.update u i s))) : + u i * hazardCoord A (Function.update u i 1) ≤ hazardCoord A u := by + have h0 : (0 : ℝ) ∈ Set.Icc (0 : ℝ) 1 := Set.left_mem_Icc.2 zero_le_one + have h1 : (1 : ℝ) ∈ Set.Icc (0 : ℝ) 1 := Set.right_mem_Icc.2 zero_le_one + have hs := hu i + have hc := hconc.2 h0 h1 (by linarith [hs.2] : (0 : ℝ) ≤ 1 - u i) hs.1 (by ring) + simp only [smul_eq_mul, mul_zero, zero_add, mul_one, Function.update_eq_self] at hc + have hf0 : 0 ≤ hazardCoord A (Function.update u i 0) := by + apply f6_hazardCoord_nonneg + intro j + rcases eq_or_ne j i with rfl | hj + · simp + · rw [Function.update_of_ne hj] + exact hu j + have hprod := mul_nonneg (sub_nonneg.2 hs.2) hf0 + linarith + +/-- The vector `u_s` which equals `1` on `s` and `t` elsewhere lies in the cube when `t` does. -/ +theorem f6_raised_mem {Y : Type} [DecidableEq Y] {t : Y → ℝ} (ht : ∀ j, 0 ≤ t j ∧ t j ≤ 1) + (s : Finset Y) : + ∀ j, 0 ≤ (if j ∈ s then (1 : ℝ) else t j) ∧ (if j ∈ s then (1 : ℝ) else t j) ≤ 1 := by + intro j + split_ifs + · exact ⟨zero_le_one, le_refl 1⟩ + · exact ht j + +/-- Raising one more coordinate: `u_{insert a s} = update u_s a 1`. -/ +theorem f6_raised_insert {Y : Type} [DecidableEq Y] (t : Y → ℝ) (a : Y) (s : Finset Y) : + (fun j => if j ∈ insert a s then (1 : ℝ) else t j) = + Function.update (fun j => if j ∈ s then (1 : ℝ) else t j) a 1 := by + funext j + by_cases hj : j = a + · subst hj + simp + · simp [Finset.mem_insert, hj] + +/-- Iterated chord inequality: for every finite set `s` of coordinates, +`(prod_{j ∈ s} t_j) · F_A(u_s) ≤ F_A(t)`, where `u_s` is `t` with the coordinates in `s` raised +to `1`. Induction over `s` (`Finset.induction_on`) with `f6_chord` at each step. -/ +theorem f6_prod_hazardCoord_le {Y : Type} [Fintype Y] [DecidableEq Y] (A : Finset (Finset Y)) + (hconc : ∀ (i : Y) (u : Y → ℝ), (∀ j, 0 ≤ u j ∧ u j ≤ 1) → + ConcaveOn ℝ (Set.Icc (0 : ℝ) 1) (fun s : ℝ => hazardCoord A (Function.update u i s))) + (t : Y → ℝ) (ht : ∀ j, 0 ≤ t j ∧ t j ≤ 1) (s : Finset Y) : + (∏ j ∈ s, t j) * hazardCoord A (fun j => if j ∈ s then (1 : ℝ) else t j) ≤ + hazardCoord A t := by + induction s using Finset.induction_on with + | empty => simp + | insert a s ha ih => + have hus := f6_raised_mem ht s + have hchord := f6_chord A a (fun j => if j ∈ s then (1 : ℝ) else t j) hus (hconc a _ hus) + simp only [ite_eq_right ha] at hchord + have hprod : 0 ≤ ∏ j ∈ s, t j := Finset.prod_nonneg fun j _ => (ht j).1 + rw [Finset.prod_insert ha, f6_raised_insert t a s] + calc t a * (∏ j ∈ s, t j) * + hazardCoord A (Function.update (fun j => if j ∈ s then (1 : ℝ) else t j) a 1) + = (∏ j ∈ s, t j) * + (t a * hazardCoord A (Function.update (fun j => if j ∈ s then (1 : ℝ) else t j) a 1)) := by + ring + _ ≤ (∏ j ∈ s, t j) * hazardCoord A (fun j => if j ∈ s then (1 : ℝ) else t j) := + mul_le_mul_of_nonneg_left hchord hprod + _ ≤ hazardCoord A t := ih + +/-- Display (F6) from display (F5): assuming `CoordinatewiseConcavity`, the hazard product bound +holds. Takes `s = univ` in `f6_prod_hazardCoord_le`, where `u_univ = (1, …, 1)` and +`F_A(1, …, 1) = H_A` (`f6_hazardCoord_one`). -/ +theorem f6_hazardProductBound_of_concavity (h5 : UniversalLaw.Spec.P15.CoordinatewiseConcavity) : + UniversalLaw.Spec.P15.HazardProductBound := by + intro n A hn hA t ht + have hconc : ∀ (i : Fin n) (u : Fin n → ℝ), (∀ j, 0 ≤ u j ∧ u j ≤ 1) → + ConcaveOn ℝ (Set.Icc (0 : ℝ) 1) (fun s : ℝ => hazardCoord A (Function.update u i s)) := + fun i u hu => h5 n A hn hA i u hu + have key := f6_prod_hazardCoord_le A hconc t ht (univ : Finset (Fin n)) + have hfun : (fun j : Fin n => if j ∈ (univ : Finset (Fin n)) then (1 : ℝ) else t j) = + fun _ => (1 : ℝ) := by + funext j + simp + rw [hfun, f6_hazardCoord_one] at key + exact key + +/-! ## (F7) The hazard `phi` bound `-log mu_p(A) ≥ H_A prod_i phi(p_i)` + +### (a) The transformed price `phi` maps `[0,1]` into `[0,1]` -/ + +/-- `0 ≤ phi x` for `x ≥ 0`: when `x < 1`, `-log(1 - x) ≥ 0` since `0 < 1 - x ≤ 1`. -/ +theorem f7_phi_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ phi x := by + unfold phi + split_ifs with h + · refine le_min zero_le_one ?_ + have hlog : Real.log (1 - x) ≤ 0 := Real.log_nonpos (by linarith) (by linarith) + linarith + · exact zero_le_one + +/-- `phi x ≤ 1` for every real `x`. -/ +theorem f7_phi_le_one (x : ℝ) : phi x ≤ 1 := by + unfold phi + split_ifs with h + · exact min_le_left _ _ + · exact le_refl 1 + +/-- `phi` maps `[0,1]` into `[0,1]`. -/ +theorem f7_phi_mem {x : ℝ} (hx : 0 ≤ x ∧ x ≤ 1) : 0 ≤ phi x ∧ phi x ≤ 1 := + ⟨f7_phi_nonneg hx.1, f7_phi_le_one x⟩ + +/-! ### (b) `p' = 1 - exp(-phi p)` lies in `[0, p]` -/ + +/-- `0 ≤ 1 - exp(-phi x)` for `x ≥ 0` (since `phi x ≥ 0`). -/ +theorem f7_one_sub_exp_neg_phi_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ 1 - Real.exp (-phi x) := by + have h : Real.exp (-phi x) ≤ 1 := Real.exp_le_one_iff.2 (by linarith [f7_phi_nonneg hx]) + linarith + +/-- `1 - exp(-phi x) ≤ x` on `[0,1]`: for `x < 1`, `phi x ≤ -log(1 - x)` so +`exp(-phi x) ≥ exp(log(1 - x)) = 1 - x`; for `x = 1`, `1 - exp(-1) ≤ 1`. -/ +theorem f7_one_sub_exp_neg_phi_le {x : ℝ} (hx : 0 ≤ x ∧ x ≤ 1) : + 1 - Real.exp (-phi x) ≤ x := by + by_cases h : x < 1 + · have hphi : phi x ≤ -Real.log (1 - x) := by + unfold phi + rw [ite_eq_left h] + exact min_le_right _ _ + have hpos : 0 < 1 - x := by linarith + have h1 : Real.exp (Real.log (1 - x)) ≤ Real.exp (-phi x) := + Real.exp_le_exp.2 (by linarith) + rw [Real.exp_log hpos] at h1 + linarith + · have hx1 : x = 1 := le_antisymm hx.2 (not_lt.1 h) + have hphi : phi x = 1 := by + unfold phi + rw [ite_eq_right h] + rw [hphi, hx1] + have := Real.exp_pos (-1 : ℝ) + linarith + +/-! ### (c) Antitonicity of `mu_p(A)` in the probability vector (from the split (F4)) -/ + +/-- The interpolating vector `r_s` (`q` on `s`, `p` elsewhere) lies in the cube when both do. -/ +theorem f7_mix_mem {Y : Type} [DecidableEq Y] {p q : Y → ℝ} (hp : ∀ j, 0 ≤ p j ∧ p j ≤ 1) + (hq : ∀ j, 0 ≤ q j ∧ q j ≤ 1) (s : Finset Y) : + ∀ j, 0 ≤ (if j ∈ s then q j else p j) ∧ (if j ∈ s then q j else p j) ≤ 1 := by + intro j + split_ifs + · exact hq j + · exact hp j + +/-- Switching one more coordinate to `q`: `r_{insert a s} = update r_s a (q a)`. -/ +theorem f7_mix_insert {Y : Type} [DecidableEq Y] (p q : Y → ℝ) (a : Y) (s : Finset Y) : + (fun j => if j ∈ insert a s then q j else p j) = + Function.update (fun j => if j ∈ s then q j else p j) a (q a) := by + funext j + by_cases hj : j = a + · subst hj + simp + · simp [Finset.mem_insert, hj] + +/-- For `a ∉ s`, `r_s` is its own update at `a` by `p a`. -/ +theorem f7_mix_eq_update_self {Y : Type} [DecidableEq Y] (p q : Y → ℝ) (a : Y) (s : Finset Y) + (ha : a ∉ s) : + (fun j => if j ∈ s then q j else p j) = + Function.update (fun j => if j ∈ s then q j else p j) a (p a) := by + funext j + by_cases hj : j = a + · subst hj + simp [ha] + · simp [hj] + +/-- Moving from `p` down to `q` one coordinate at a time: for every finite set `s` of +coordinates, `mu_p(A) ≤ mu_(r_s)(A)` (induction over `s`, `cc_muOf_update_antitone` at each +step). -/ +theorem f7_muOf_le_mix {Y : Type} [Fintype Y] [DecidableEq Y] {A : Finset (Finset Y)} + (hA : ∀ U ∈ A, ∀ V : Finset Y, V ⊆ U → V ∈ A) {p q : Y → ℝ} + (hp : ∀ j, 0 ≤ p j ∧ p j ≤ 1) (hq : ∀ j, 0 ≤ q j ∧ q j ≤ 1) (hqp : ∀ j, q j ≤ p j) + (s : Finset Y) : + muOf A p ≤ muOf A (fun j => if j ∈ s then q j else p j) := by + induction s using Finset.induction_on with + | empty => simp + | insert a s ha ih => + have hmem := f7_mix_mem hp hq s + have hstep := cc_muOf_update_antitone hA hmem a (hqp a) + rw [← f7_mix_eq_update_self p q a s ha] at hstep + rw [f7_mix_insert p q a s] + exact ih.trans hstep + +/-- Antitonicity of `mu(A)` in the probability vector for a downset: `q ≤ p` pointwise, both in +the cube, gives `mu_p(A) ≤ mu_q(A)`. -/ +theorem f7_muOf_antitone {Y : Type} [Fintype Y] [DecidableEq Y] {A : Finset (Finset Y)} + (hA : ∀ U ∈ A, ∀ V : Finset Y, V ⊆ U → V ∈ A) {p q : Y → ℝ} + (hp : ∀ j, 0 ≤ p j ∧ p j ≤ 1) (hq : ∀ j, 0 ≤ q j ∧ q j ≤ 1) (hqp : ∀ j, q j ≤ p j) : + muOf A p ≤ muOf A q := by + have h := f7_muOf_le_mix hA hp hq hqp (univ : Finset Y) + have hfun : (fun j : Y => if j ∈ (univ : Finset Y) then q j else p j) = q := by + funext j + simp + rw [hfun] at h + exact h + +/-! ### (d) Display (F7) from display (F6) -/ + +/-- Display (F7) from display (F6): assuming `HazardProductBound`, the hazard `phi` bound holds. +With `t_i := phi(p_i) ∈ [0,1]` and `p'_i := 1 - exp(-t_i) ∈ [0, p_i]`, antitonicity gives +`0 < mu_p(A) ≤ mu_p'(A)`, so `-log mu_p(A) ≥ -log mu_p'(A) = F_A(t) ≥ (prod_i t_i) H_A`. -/ +theorem f7_hazardPhiBound_of_productBound (h6 : UniversalLaw.Spec.P15.HazardProductBound) : + UniversalLaw.Spec.P15.HazardPhiBound := by + intro n A hn hA p hp hpos + have hdown : ∀ U ∈ A, ∀ V : Finset (Fin n), V ⊆ U → V ∈ A := hA.2.2 + have ht : ∀ j, 0 ≤ phi (p j) ∧ phi (p j) ≤ 1 := fun j => f7_phi_mem (hp j) + have hp' : ∀ j, 0 ≤ 1 - Real.exp (-phi (p j)) ∧ 1 - Real.exp (-phi (p j)) ≤ 1 := + fun j => ⟨f7_one_sub_exp_neg_phi_nonneg (hp j).1, + (f7_one_sub_exp_neg_phi_le (hp j)).trans (hp j).2⟩ + have hle : muOf A p ≤ muOf A (fun j => 1 - Real.exp (-phi (p j))) := + f7_muOf_antitone hdown hp hp' (fun j => f7_one_sub_exp_neg_phi_le (hp j)) + have hlog : -Real.log (muOf A (fun j => 1 - Real.exp (-phi (p j)))) ≤ -Real.log (muOf A p) := + neg_le_neg (Real.log_le_log hpos hle) + have h6' := h6 n A hn hA (fun j => phi (p j)) ht + have hcoord : hazardCoord A (fun j => phi (p j)) = + -Real.log (muOf A (fun j => 1 - Real.exp (-phi (p j)))) := rfl + rw [hcoord] at h6' + calc hazardStar A * ∏ i, phi (p i) = (∏ i, phi (p i)) * hazardStar A := mul_comm _ _ + _ ≤ -Real.log (muOf A (fun j => 1 - Real.exp (-phi (p j)))) := h6' + _ ≤ -Real.log (muOf A p) := hlog + +/-! ## (F8) The full-ground price bound -/ + +/-- `prod_i phi(p_i) ≤ 1` for `p ∈ [0, 1]^n`, from `0 ≤ phi ≤ 1` on `[0, 1]` +(`Finset.prod_le_one₀`). -/ +theorem f8_prod_phi_le_one {n : ℕ} (p : Fin n → ℝ) (hp : ∀ j, 0 ≤ p j ∧ p j ≤ 1) : + ∏ i, phi (p i) ≤ 1 := + Finset.prod_le_one₀ (fun i _ => f7_phi_nonneg (hp i).1) (fun i _ => f7_phi_le_one (p i)) + +/-- `prod_i c_i ≤ prod_i phi(p_i)` for `0 ≤ c_i ≤ phi(p_i)` (`Finset.prod_le_prod₀`). -/ +theorem f8_prod_le_prod_phi {n : ℕ} (p c : Fin n → ℝ) (hc : ∀ j, 0 ≤ c j ∧ c j ≤ phi (p j)) : + ∏ i, c i ≤ ∏ i, phi (p i) := + Finset.prod_le_prod₀ (fun i _ => (hc i).1) (fun i _ => (hc i).2) + +/-- Display (F8) from display (F7): given `HazardPhiBound`, the full-ground price bound holds. +Fix `n`, a proper downset `A` on `Fin n`, `p ∈ [0, 1]^n` and `0 ≤ c ≤ phi ∘ p`. The cap `1` is +`f8_prod_le_prod_phi` and `f8_prod_phi_le_one`; when `0 < mu_p(A)`, (F7) gives +`H_A prod_i phi(p_i) ≤ -log mu_p(A)` and `0 < H_A` (`P15Elementary.hazardStarPositive`), so +`prod_i phi(p_i) = H_A⁻¹ (H_A prod_i phi(p_i)) ≤ H_A⁻¹ [-log mu_p(A)]` (`inv_mul_cancel_left₀`, +`mul_le_mul_of_nonneg_left`); `P15Budget.Aux.le_cappedHazard_of` reaches the capped hazard. -/ +theorem f8_fullGroundPriceBound_of_phiBound (h7 : UniversalLaw.Spec.P15.HazardPhiBound) : + UniversalLaw.Spec.P15.FullGroundPriceBound := by + intro n A hn hA p c hp hc + have hprod : ∏ i, c i ≤ ∏ i, phi (p i) := f8_prod_le_prod_phi p c hc + have hphi1 : ∏ i, phi (p i) ≤ 1 := f8_prod_phi_le_one p hp + refine UniversalLaw.Proofs.P15Budget.Aux.le_cappedHazard_of (hprod.trans hphi1) fun hm => ?_ + have hH : 0 < hazardStar A := UniversalLaw.Proofs.P15Elementary.hazardStarPositive n A hn hA + have hne : hazardStar A ≠ 0 := hH.ne' + have h7' : hazardStar A * ∏ i, phi (p i) ≤ -Real.log (muOf A p) := h7 n A hn hA p hp hm + calc ∏ i, c i ≤ ∏ i, phi (p i) := hprod + _ = (hazardStar A)⁻¹ * (hazardStar A * ∏ i, phi (p i)) := + (inv_mul_cancel_left₀ hne _).symm + _ ≤ (hazardStar A)⁻¹ * -Real.log (muOf A p) := + mul_le_mul_of_nonneg_left h7' (inv_nonneg.mpr hH.le) + _ = 1 / hazardStar A * -Real.log (muOf A p) := by rw [one_div] + +/-! ## (F8), exactness remark: the full-ground budget equivalence -/ + +/-- `0 ≤ prod_i phi(p_i)` for `p ∈ [0, 1]^n` (`Finset.prod_nonneg`). -/ +theorem bi_prod_phi_nonneg {n : ℕ} (p : Fin n → ℝ) (hp : ∀ j, 0 ≤ p j ∧ p j ≤ 1) : + 0 ≤ ∏ i, phi (p i) := + Finset.prod_nonneg fun i _ => f7_phi_nonneg (hp i).1 + +/-- The (⇐) direction, display (F8) with `rho = 1`: given display (F7) and `1 ≤ H_A`, every +`p ∈ [0, 1]^n` and `0 ≤ c ≤ phi ∘ p` satisfy `prod_i c_i ≤ cappedHazard 1 (mu_p(A))`. The cap +`1` is `f8_prod_le_prod_phi` and `f8_prod_phi_le_one`; when `0 < mu_p(A)`, +`prod_i phi(p_i) ≤ H_A prod_i phi(p_i)` (`le_mul_of_one_le_left`, from `0 ≤ prod_i phi(p_i)` +and `1 ≤ H_A`) and `H_A prod_i phi(p_i) ≤ -log mu_p(A)` by (F7); +`P15Budget.Aux.le_cappedHazard_of` reaches the capped hazard. -/ +theorem bi_budget_of_one_le_hazardStar (h7 : UniversalLaw.Spec.P15.HazardPhiBound) {n : ℕ} + {A : Finset (Finset (Fin n))} (hn : 1 ≤ n) (hA : IsProperDownset A) + (h1 : 1 ≤ hazardStar A) (p c : Fin n → ℝ) (hp : ∀ j, 0 ≤ p j ∧ p j ≤ 1) + (hc : ∀ j, 0 ≤ c j ∧ c j ≤ phi (p j)) : + ∏ i, c i ≤ cappedHazard 1 (muOf A p) := by + have hprod : ∏ i, c i ≤ ∏ i, phi (p i) := f8_prod_le_prod_phi p c hc + have hphi1 : ∏ i, phi (p i) ≤ 1 := f8_prod_phi_le_one p hp + refine UniversalLaw.Proofs.P15Budget.Aux.le_cappedHazard_of (hprod.trans hphi1) fun hm => ?_ + have hphi0 : 0 ≤ ∏ i, phi (p i) := bi_prod_phi_nonneg p hp + have h7' : hazardStar A * ∏ i, phi (p i) ≤ -Real.log (muOf A p) := h7 n A hn hA p hp hm + calc ∏ i, c i ≤ ∏ i, phi (p i) := hprod + _ ≤ hazardStar A * ∏ i, phi (p i) := le_mul_of_one_le_left hphi0 h1 + _ ≤ -Real.log (muOf A p) := h7' + _ = 1 * -Real.log (muOf A p) := (one_mul _).symm + +/-- `0 < mu_{p_star}(A)` for a proper downset `A`: every weight at the constant vector +`p_star ∈ (0, 1)` is nonnegative (`P15Budget.Aux.weight_nonneg`), and the member `∅ ∈ A` +contributes `prod_{v} (1 - p_star) > 0` (`Finset.prod_pos`), so `Finset.single_le_sum` gives +the claim. -/ +theorem bi_muOf_pStar_pos {n : ℕ} {A : Finset (Finset (Fin n))} (hA : IsProperDownset A) : + 0 < muOf A (fun _ => pStar) := by + have hp0 : 0 < pStar := UniversalLaw.Proofs.P15Elementary.Aux.pStar_pos + have hp1 : pStar < 1 := UniversalLaw.Proofs.P15Elementary.Aux.pStar_lt_one + have hw_nonneg : ∀ U : Finset (Fin n), 0 ≤ weight (fun _ : Fin n => pStar) U := + fun U => UniversalLaw.Proofs.P15Budget.Aux.weight_nonneg (fun _ => ⟨hp0.le, hp1.le⟩) U + have hempty_w : 0 < weight (fun _ : Fin n => pStar) (∅ : Finset (Fin n)) := by + unfold weight + rw [prod_empty, one_mul] + exact Finset.prod_pos fun v _ => by + show (0 : ℝ) < 1 - pStar + linarith + unfold muOf + exact lt_of_lt_of_le hempty_w (Finset.single_le_sum (fun U _ => hw_nonneg U) hA.1) + +/-- The (⇒) direction: if every `p ∈ [0, 1]^n` and `0 ≤ c ≤ phi ∘ p` satisfy +`prod_i c_i ≤ cappedHazard 1 (mu_p(A))`, then `1 ≤ H_A`. Instantiate at `p ≡ p_star`, `c ≡ 1`, +admissible since `0 ≤ p_star ≤ 1` and `phi p_star = 1` (`P15Elementary.phiAtPStar`); then +`prod_i 1 = 1` (`Finset.prod_const_one`), `0 < mu_{p_star}(A)` (`bi_muOf_pStar_pos`) selects +the branch `min 1 (1 * -log mu_{p_star}(A))` of `cappedHazard`, and `le_min_iff` extracts +`1 ≤ -log mu_{p_star}(A)`, which is `hazardStar A` by definition. -/ +theorem bi_one_le_hazardStar_of_budget {n : ℕ} {A : Finset (Finset (Fin n))} + (hA : IsProperDownset A) + (hall : ∀ (p c : Fin n → ℝ), (∀ j, 0 ≤ p j ∧ p j ≤ 1) → (∀ j, 0 ≤ c j ∧ c j ≤ phi (p j)) → + ∏ i, c i ≤ cappedHazard 1 (muOf A p)) : + 1 ≤ hazardStar A := by + have hp0 : 0 < pStar := UniversalLaw.Proofs.P15Elementary.Aux.pStar_pos + have hp1 : pStar < 1 := UniversalLaw.Proofs.P15Elementary.Aux.pStar_lt_one + have hphi : phi pStar = 1 := UniversalLaw.Proofs.P15Elementary.phiAtPStar + have hp : ∀ j : Fin n, 0 ≤ (fun _ : Fin n => pStar) j ∧ (fun _ : Fin n => pStar) j ≤ 1 := + fun _ => ⟨hp0.le, hp1.le⟩ + have hc : ∀ j : Fin n, 0 ≤ (fun _ : Fin n => (1 : ℝ)) j ∧ + (fun _ : Fin n => (1 : ℝ)) j ≤ phi ((fun _ : Fin n => pStar) j) := + fun _ => ⟨zero_le_one, hphi.symm.le⟩ + have h := hall (fun _ => pStar) (fun _ => (1 : ℝ)) hp hc + simp only [Finset.prod_const_one] at h + have hm : 0 < muOf A (fun _ => pStar) := bi_muOf_pStar_pos hA + unfold cappedHazard at h + simp only [hm, ↓reduceIte, one_mul] at h + unfold hazardStar + exact (le_min_iff.1 h).2 + +/-- The budget equivalence from display (F7): given `HazardPhiBound`, for `n ≥ 1` and a proper +downset `A` on `Fin n`, the universal capped budget at `rho = 1` holds iff `1 ≤ H_A`. The two +directions are `bi_one_le_hazardStar_of_budget` and `bi_budget_of_one_le_hazardStar`. -/ +theorem bi_fullGroundBudgetIff_of_phiBound (h7 : UniversalLaw.Spec.P15.HazardPhiBound) : + UniversalLaw.Spec.P15.FullGroundBudgetIff := by + intro n A hn hA + constructor + · intro hall + exact bi_one_le_hazardStar_of_budget hA hall + · intro h1 p c hp hc + exact bi_budget_of_one_le_hazardStar h7 hn hA h1 p c hp hc + +/-! ## (F12) The local price bound + +### Elementary facts -/ + +/-- The capacity family `{T ⊆ Fin n : |T| ≤ a}` is a proper downset when `a < n`: it contains +the empty set, misses `univ` (of size `n > a`), and is closed under taking subsets. -/ +theorem lp_capacityFamily_properDownset (n a : ℕ) (h : a < n) : + IsProperDownset (capacityFamily n a) := by + refine ⟨?_, ?_, ?_⟩ + · show ∅ ∈ (univ : Finset (Fin n)).powerset.filter (fun U => U.card ≤ a) + rw [mem_filter, mem_powerset, card_empty] + exact ⟨empty_subset _, Nat.zero_le _⟩ + · intro huniv + have hcard : (univ : Finset (Fin n)).card ≤ a := (mem_filter.mp huniv).2 + rw [card_univ, Fintype.card_fin] at hcard + exact absurd hcard (not_le.mpr h) + · intro U hU V hVU + have hU' : U.card ≤ a := (mem_filter.mp hU).2 + exact mem_filter.mpr ⟨mem_powerset.mpr (subset_univ V), le_trans (card_le_card hVU) hU'⟩ + +/-! ### Enumerating a finite set by `Fin (card)` -/ + +/-- Every `B : Finset X` is enumerated injectively by `Fin B.card`, with range exactly `B`. -/ +theorem lp_exists_enum {X : Type} (B : Finset X) : + ∃ e : Fin B.card → X, Function.Injective e ∧ ∀ v, v ∈ B ↔ ∃ k, e k = v := by + refine ⟨fun k => (B.equivFin.symm k).1, ?_, ?_⟩ + · intro k₁ k₂ h + exact B.equivFin.symm.injective (Subtype.ext h) + · intro v + constructor + · intro hv + exact ⟨B.equivFin ⟨v, hv⟩, by simp⟩ + · rintro ⟨k, rfl⟩ + exact (B.equivFin.symm k).2 + +/-- An injection `e : Fin n → X` with range `B` maps `univ` onto `B`. -/ +theorem lp_map_univ_eq {X : Type} {B : Finset X} {n : ℕ} (e : Fin n → X) + (he : Function.Injective e) (hrange : ∀ v, v ∈ B ↔ ∃ k, e k = v) : + (univ : Finset (Fin n)).map ⟨e, he⟩ = B := by + ext v + rw [hrange v] + simp only [mem_map, mem_univ, true_and, Function.Embedding.coeFn_mk] + +/-- Products over `B` are products over `Fin n` along the enumeration. -/ +theorem lp_prod_univ_eq {X : Type} {B : Finset X} {n : ℕ} (e : Fin n → X) + (he : Function.Injective e) (hrange : ∀ v, v ∈ B ↔ ∃ k, e k = v) (f : X → ℝ) : + ∏ k, f (e k) = ∏ v ∈ B, f v := by + rw [← lp_map_univ_eq e he hrange, Finset.prod_map] + rfl + +/-- For `S ⊆ B`, the image of the preimage `{k : e k ∈ S}` is `S`. -/ +theorem lp_map_filter_eq {X : Type} [DecidableEq X] {B : Finset X} {n : ℕ} (e : Fin n → X) + (he : Function.Injective e) (hrange : ∀ v, v ∈ B ↔ ∃ k, e k = v) {S : Finset X} + (hS : S ⊆ B) : + ((univ : Finset (Fin n)).filter (fun k => e k ∈ S)).map ⟨e, he⟩ = S := by + ext v + simp only [mem_map, mem_filter, mem_univ, true_and, Function.Embedding.coeFn_mk] + constructor + · rintro ⟨k, hk, rfl⟩ + exact hk + · intro hv + obtain ⟨k, rfl⟩ := (hrange v).mp (hS hv) + exact ⟨k, hv, rfl⟩ + +/-- The preimage of the image of `T` is `T` (injectivity of the enumeration). -/ +theorem lp_filter_map_eq {X : Type} [DecidableEq X] {n : ℕ} (e : Fin n → X) + (he : Function.Injective e) (T : Finset (Fin n)) : + (univ : Finset (Fin n)).filter (fun k => e k ∈ T.map ⟨e, he⟩) = T := by + ext k + simp only [mem_filter, mem_univ, true_and, mem_map, Function.Embedding.coeFn_mk] + constructor + · rintro ⟨a, ha, hak⟩ + rwa [he hak] at ha + · intro hk + exact ⟨k, hk, rfl⟩ + +/-! ### Transport of the local good probability to the capacity family -/ + +/-- Along an enumeration `e : Fin n → X` of the block `X_i`, the local good probability +`mu_p(D_i)` is the product measure of the capacity family `{T : |T| ≤ a_i}` on `Fin n` under +the transported vector `p ∘ e`. Uses `LocalRestriction` (a block subset is good iff its size is +at most `a_i`) and the bijection `T ↦ T.map e` between subsets of `Fin n` and subsets of the +block, which preserves size and matches the two weight products. -/ +theorem lp_localGood_eq_muOf {X : Type} [Fintype X] [DecidableEq X] {F : RealizedData X} + (hF : IsRealizedFamily F) (p : X → ℝ) (i : Fin F.b) {n : ℕ} (e : Fin n → X) + (he : Function.Injective e) (hrange : ∀ v, v ∈ block F i ↔ ∃ k, e k = v) : + localGood F p i = muOf (capacityFamily n (F.a i)) (fun k => p (e k)) := by + have hLR := UniversalLaw.Proofs.P15Covers.localRestriction F hF i + have hmapuniv := lp_map_univ_eq e he hrange + have hind : ∀ S ∈ (block F i).powerset, + Set.indicator (downset F) + (fun S => (∏ v ∈ S, p v) * ∏ v ∈ block F i \ S, (1 - p v)) S = + if S.card ≤ F.a i then (∏ v ∈ S, p v) * ∏ v ∈ block F i \ S, (1 - p v) else 0 := by + intro S hS + have hgood : S ∈ downset F ↔ S.card ≤ F.a i := by + show IsGood F S ↔ S.card ≤ F.a i + exact hLR S (mem_powerset.mp hS) + by_cases h : S.card ≤ F.a i + · rw [Set.indicator_of_mem (hgood.mpr h), ite_eq_left h] + · rw [Set.indicator_of_notMem (fun h' => h (hgood.mp h')), ite_eq_right h] + unfold localGood + rw [Finset.sum_congr rfl hind, ← Finset.sum_filter] + unfold muOf capacityFamily + symm + refine Finset.sum_nbij' (fun T => T.map ⟨e, he⟩) + (fun S => (univ : Finset (Fin n)).filter (fun k => e k ∈ S)) ?_ ?_ ?_ ?_ ?_ + · intro T hT + rw [mem_filter, mem_powerset] at hT + rw [mem_filter, mem_powerset] + refine ⟨?_, ?_⟩ + · rw [← hmapuniv] + exact map_subset_map.mpr hT.1 + · rw [card_map] + exact hT.2 + · intro S hS + rw [mem_filter, mem_powerset] at hS + rw [mem_filter, mem_powerset] + refine ⟨subset_univ _, ?_⟩ + rw [← card_map ⟨e, he⟩, lp_map_filter_eq e he hrange hS.1] + exact hS.2 + · intro T _ + exact lp_filter_map_eq e he T + · intro S hS + rw [mem_filter, mem_powerset] at hS + exact lp_map_filter_eq e he hrange hS.1 + · intro T _ + show weight (fun k => p (e k)) T = + (∏ v ∈ T.map ⟨e, he⟩, p v) * ∏ v ∈ block F i \ T.map ⟨e, he⟩, (1 - p v) + unfold weight + rw [Finset.prod_map, ← hmapuniv, ← Finset.map_sdiff, Finset.prod_map] + rfl + +/-! ### Display (F12) in hypothesis form -/ + +/-- Display (F12) under the hypothesis `HazardPhiBound` (display (F7)): for every realized +family with `d_i ≥ 2`, every `p ∈ [0,1]^X`, every `0 ≤ c_v ≤ phi(p_v)` and every block with +`mu_p(D_i) > 0`, `price(X_i) ≤ rho_star · (-log mu_p(D_i))` and `price(X_i) ≤ 1`. -/ +theorem lp_localPriceBoundFull_of_phiBound (h7 : UniversalLaw.Spec.P15.HazardPhiBound) + {X : Type} [Fintype X] [DecidableEq X] (F : RealizedData X) : + UniversalLaw.Spec.P15.LocalPriceBoundFull F := by + intro hF hd p c hp hc i hpos + obtain ⟨e, he, hrange⟩ := lp_exists_enum (block F i) + have hcard : (block F i).card = F.a i * F.d i + 1 := hF.2.2.1 i + have ha1 : 1 ≤ F.a i := hF.1 i + have hd2 : 2 ≤ F.d i := hd i + have hmul : F.a i * 2 ≤ F.a i * F.d i := Nat.mul_le_mul_left (F.a i) hd2 + have hn1 : 1 ≤ (block F i).card := by rw [hcard]; omega + have hlt : F.a i < (block F i).card := by rw [hcard]; omega + have h2a : 2 * F.a i + 1 ≤ (block F i).card := by rw [hcard]; omega + -- transport to the capacity family on `Fin n` + have htrans : localGood F p i = + muOf (capacityFamily (block F i).card (F.a i)) (fun k => p (e k)) := + lp_localGood_eq_muOf hF p i e he hrange + have hproper : IsProperDownset (capacityFamily (block F i).card (F.a i)) := + lp_capacityFamily_properDownset _ _ hlt + have hpos' : 0 < muOf (capacityFamily (block F i).card (F.a i)) (fun k => p (e k)) := by + rw [← htrans] + exact hpos + -- display (F7) on the transported vector + have h7' : hazardStar (capacityFamily (block F i).card (F.a i)) * ∏ k, phi (p (e k)) ≤ + -Real.log (muOf (capacityFamily (block F i).card (F.a i)) (fun k => p (e k))) := + h7 _ _ hn1 hproper (fun k => p (e k)) (fun k => hp (e k)) hpos' + rw [← htrans] at h7' + have hprod : ∏ k, phi (p (e k)) = ∏ v ∈ block F i, phi (p v) := + lp_prod_univ_eq e he hrange (fun v => phi (p v)) + -- the sharp worst case (F11): `h_star ≤ H_{n,a}` and `0 < h_star` + obtain ⟨hmono, heq1, heq2, hgt1⟩ := UniversalLaw.Proofs.P15Elementary.capacityWorstCase + have hHstar : hStar ≤ hazardStar (capacityFamily (block F i).card (F.a i)) := by + have := hmono (F.a i) _ ha1 h2a + rwa [heq1, heq2] at this + have hhpos : 0 < hStar := lt_trans zero_lt_one hgt1 + have hH0 : 0 ≤ hazardStar (capacityFamily (block F i).card (F.a i)) := + le_of_lt (lt_of_lt_of_le hhpos hHstar) + -- the price + have hG0 : 0 ≤ genPrice c (block F i) := Finset.prod_nonneg (fun v _ => (hc v).1) + have hGP : genPrice c (block F i) ≤ ∏ v ∈ block F i, phi (p v) := + Finset.prod_le_prod₀ (fun v _ => (hc v).1) (fun v _ => (hc v).2) + have hG1 : genPrice c (block F i) ≤ 1 := + Finset.prod_le_one₀ (fun v _ => (hc v).1) (fun v _ => (hc v).2.trans (f7_phi_le_one _)) + refine ⟨?_, hG1⟩ + have key : hStar * genPrice c (block F i) ≤ -Real.log (localGood F p i) := by + calc hStar * genPrice c (block F i) + ≤ hazardStar (capacityFamily (block F i).card (F.a i)) * genPrice c (block F i) := + mul_le_mul_of_nonneg_right hHstar hG0 + _ ≤ hazardStar (capacityFamily (block F i).card (F.a i)) * ∏ v ∈ block F i, phi (p v) := + mul_le_mul_of_nonneg_left hGP hH0 + _ = hazardStar (capacityFamily (block F i).card (F.a i)) * ∏ k, phi (p (e k)) := by + rw [hprod] + _ ≤ -Real.log (localGood F p i) := h7' + have hrho : rhoStar = 1 / hStar := rfl + rw [hrho, one_div, inv_mul_eq_div, le_div_iff₀ hhpos, mul_comm] + exact key + +/-! ## (F2) The full transformed-price budget -/ + +/-- `0 ≤ rho_star`: `rho_star = 1 / (3 - log(3e - 2))` is definitionally `1 / h_star`, and +`1 < h_star` (`P15Elementary.Aux.one_lt_hStar`). -/ +theorem f2_rhoStar_nonneg : 0 ≤ rhoStar := by + have h : (1 : ℝ) < 3 - Real.log (3 * Real.exp 1 - 2) := + UniversalLaw.Proofs.P15Elementary.Aux.one_lt_hStar + unfold rhoStar + exact div_nonneg zero_le_one (by linarith) + +/-- Display (F2) from display (F12): given the local price bound for every realized family, the +full transformed-price budget holds for every realized family. The hypothesis `h12` is the +registered `Prop` `LocalPriceBoundFull`, quantified over the ground type so that it can be +discharged by the inventory theorem `localPriceBoundFull`. -/ +theorem f2_fullTransformedPriceBudget_of_local + (h12 : ∀ {X : Type} [Fintype X] [DecidableEq X] (F : RealizedData X), + UniversalLaw.Spec.P15.LocalPriceBoundFull F) + {X : Type} [Fintype X] [DecidableEq X] (F : RealizedData X) : + UniversalLaw.Spec.P15.FullTransformedPriceBudget F := by + intro hF hd p c hp hc K hK + have hc0 : ∀ v, 0 ≤ c v := fun v => (hc v).1 + refine UniversalLaw.Proofs.P15Budget.Aux.le_cappedHazard_of + (UniversalLaw.Proofs.P15Budget.Aux.coverCost_le_one F K hc0) fun hmu => ?_ + calc coverCost F K c + ≤ ∑ i, genPrice c (block F i) := + UniversalLaw.Proofs.P15Budget.Aux.coverCost_le_sum_block hF hc0 hK + _ ≤ ∑ i, rhoStar * (-Real.log (localGood F p i)) := by + refine Finset.sum_le_sum fun i _ => ?_ + have hpos : 0 < localGood F p i := + UniversalLaw.Proofs.P15Hazard.Aux.localGood_pos_of_mu_pos F hp hmu i + exact (h12 F hF hd p c hp hc i hpos).1 + _ = rhoStar * ∑ i, -Real.log (localGood F p i) := by + rw [Finset.mul_sum] + _ ≤ rhoStar * -Real.log (mu F p) := + mul_le_mul_of_nonneg_left + ((UniversalLaw.Proofs.P15Hazard.globalAssemblyHazard F hF p hp).2 hmu) + f2_rhoStar_nonneg + +end Aux + +/-! ## Inventory theorems + +Each theorem below has as its type exactly one registered `Prop`; the chain is +`coordinatewiseConcavity → hazardProductBound → hazardPhiBound → fullGroundPriceBound, +fullGroundBudgetIff, localPriceBoundFull → fullTransformedPriceBudget`, and `rhoStarEnclosure` +is independent of it. -/ + +/-- Proves: `UniversalLaw.Spec.P15.RhoStarEnclosure` (claim `p15-full-price`, display (F3)). +Method: `rho_star < U` iff `3e - 2 < exp(3 - 1/U)` and `L < rho_star` iff `exp(3 - 1/L) < 3e - 2` +(`Real.log_lt_iff_lt_exp`, `Real.lt_log_iff_exp_lt`, `div_lt_iff₀`, `lt_div_iff₀`); with +`3 - 1/U = 2 + x_U`, `exp(3 - 1/U) = (exp 1)^2 * exp x_U` (`Real.exp_add`, `exp_two_eq`), and +`Real.exp_bound` at degree 26 for `e` and degree 16 for `exp x_U`, `exp x_L` gives exact rational +enclosures (`Aux.f3_exp_one_gt/lt`, `Aux.f3_exp_xU_ge`, `Aux.f3_exp_xL_le`) that `norm_num` +compares in `Aux.f3_log_lt`, `Aux.f3_lt_log`; `rhoStarUpper < 6/7` is `norm_num` on rationals. +Does not establish: the informal display (F3) or its review and acceptance; the alignment of the +formal objects with the source's (PENDING_INDEPENDENT_REVIEW); the source's `full_price.py` +Fraction procedure (not specified and not reproduced here: the route above is a different +certificate of the same enclosure), nor any change to the `specified` status that main's +`docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md` records for this target; the disposition of +`p15-full-price`, which is transcribed in the register, not derived here. -/ +theorem rhoStarEnclosure : UniversalLaw.Spec.P15.RhoStarEnclosure := by + unfold UniversalLaw.Spec.P15.RhoStarEnclosure + exact ⟨Aux.f3_lower_lt_rhoStar, Aux.f3_rhoStar_lt_upper, Aux.f3_upper_lt_six_sevenths⟩ + +/-- Proves: `UniversalLaw.Spec.P15.CoordinatewiseConcavity` (claim `p15-full-price`, display (F5)). +Method: split `mu_p(A)` at the coordinate `i` (display (F4), `Aux.cc_muOf_update`): with +`p_i = 1 - exp(-s)` it equals `S_in + (S_out - S_in) exp(-s)`, where `0 ≤ S_in ≤ S_out` for a +downset (`Aux.cc_sum_in_le_sum_out`, the injection `U ↦ U.erase i`) and `S_out > 0` since `∅ ∈ A` +and every `p_j(t) < 1` on the cube (`Aux.cc_sum_out_pos`); then `s ↦ -log(a + b exp(-s))` with +`a, b ≥ 0`, `a + b > 0` is concave by `concaveOn_of_deriv2_nonpos`, its second derivative being +`-a b exp(-s) / (a + b exp(-s))^2 ≤ 0` (`Aux.cc_concaveOn_negLog`, via `HasDerivAt.log`, +`HasDerivAt.div`, `HasDerivAt.deriv`). +Does not establish: the informal display (F5) or its review and acceptance; the alignment of the +formal objects with the source's (PENDING_INDEPENDENT_REVIEW); joint concavity, or the derivative +formulas (F4)-(F5) themselves as registered statements (not specified; concavity is their +consequence); the disposition of `p15-full-price`, which is transcribed in the register, not +derived here. -/ +theorem coordinatewiseConcavity : UniversalLaw.Spec.P15.CoordinatewiseConcavity := by + intro n A _ hA i t ht + obtain ⟨h0, -, hdown⟩ := hA + exact Aux.cc_concaveOn_hazardCoord_update h0 hdown i t ht + +/-- Proves: `UniversalLaw.Spec.P15.HazardProductBound` (claim `p15-full-price`, display (F6)). +Method: chord inequality of the separate coordinatewise concavity `coordinatewiseConcavity` +(display (F5)) on `[0,1]`: `f(s) ≥ (1-s) f(0) + s f(1) ≥ s f(1)` since `f(0) = -log mu ≥ 0` +(`Aux.f6_hazardCoord_nonneg`, from `mu_p(A) ≤ 1` by `sum_weight_eq_one` and `weight_nonneg`); +iterate over the coordinates with `Finset.induction_on` (`Aux.f6_prod_hazardCoord_le`), raising +one coordinate to `1` at each step (`Aux.f6_chord`), and identify `F_A(1, …, 1) = H_A` +(`Aux.f6_hazardCoord_one`, since `1 - exp(-1) = p_star`). +Does not establish: the informal display (F6) or its review and acceptance; the alignment of the +formal objects with the source's (PENDING_INDEPENDENT_REVIEW); the inequality as an informal +statement (the Prop is statement only); the disposition of `p15-full-price`, which is +transcribed in the register, not derived here. -/ +theorem hazardProductBound : UniversalLaw.Spec.P15.HazardProductBound := + Aux.f6_hazardProductBound_of_concavity coordinatewiseConcavity + +/-- Proves: `UniversalLaw.Spec.P15.HazardPhiBound` (claim `p15-full-price`, display (F7)). +Method: put `t_i := phi(p_i) ∈ [0,1]` (`Aux.f7_phi_mem`) and `p'_i := 1 - exp(-t_i) ∈ [0, p_i]` +(`Aux.f7_one_sub_exp_neg_phi_le`, from `phi p ≤ -log(1-p)` and `Real.exp_log`); for a downset +`mu(A)` is antitone in the probability vector (`Aux.f7_muOf_antitone`, built from the +one-coordinate split `Aux.cc_muOf_update` of display (F4) with `S_in ≤ S_out` by +`Finset.sum_image` along `U ↦ U.erase i`, iterated by `Finset.induction_on`), so +`0 < mu_p(A) ≤ mu_p'(A)` and `Real.log_le_log` give `-log mu_p(A) ≥ -log mu_p'(A) = F_A(t)`; +display (F6) `hazardProductBound` then gives `F_A(t) ≥ (prod_i t_i) H_A`, and `mul_comm` +matches the Prop's order. +Does not establish: the informal display (F7) or its review and acceptance; the alignment of the +formal objects with the source's (PENDING_INDEPENDENT_REVIEW); the inequality as an informal +statement (the Prop is statement only), nor anything at `mu_p(A) = 0`, where the source reads +the inequality as an extended one and the Prop states nothing; the disposition of +`p15-full-price`, which is transcribed in the register, not derived here. -/ +theorem hazardPhiBound : UniversalLaw.Spec.P15.HazardPhiBound := + Aux.f7_hazardPhiBound_of_productBound hazardProductBound + +/-- Proves: `UniversalLaw.Spec.P15.FullGroundPriceBound` (claim `p15-full-price`, display (F8)). +Method: `prod_i c_i ≤ prod_i phi(p_i)` for `0 ≤ c_i ≤ phi(p_i)` (`Finset.prod_le_prod₀`) and +`prod_i phi(p_i) ≤ 1` from `0 ≤ phi ≤ 1` on `[0,1]` (`Finset.prod_le_one₀`, `Real.log_nonpos`) +give the cap; when `mu_p(A) > 0`, display (F7), `hazardPhiBound`, gives +`H_A prod_i phi(p_i) ≤ -log mu_p(A)` and `H_A > 0` (`P15Elementary.hazardStarPositive`), so +`prod_i phi(p_i) ≤ (1/H_A) [-log mu_p(A)]` (`inv_mul_cancel_left₀`, `mul_le_mul_of_nonneg_left`); +`P15Budget.Aux.le_cappedHazard_of` reaches the capped hazard. +Does not establish: the informal display (F8) or its review and acceptance; the alignment of the +formal objects with the source's (PENDING_INDEPENDENT_REVIEW); that the full-ground generator +covers any obstruction (the source: "It does not assert that this generator alone covers an +arbitrary obstruction"); the disposition of `p15-full-price`, which is transcribed in the +register, not derived here. -/ +theorem fullGroundPriceBound : UniversalLaw.Spec.P15.FullGroundPriceBound := + Aux.f8_fullGroundPriceBound_of_phiBound hazardPhiBound + +/-- Proves: `UniversalLaw.Spec.P15.FullGroundBudgetIff` (claim `p15-full-price`, display (F8), the +exactness remark following it). +Method: (⇐) is display (F8) with `rho = 1`: `prod_i c_i ≤ prod_i phi(p_i) ≤ 1` +(`Finset.prod_le_prod₀`, `Finset.prod_le_one₀`) and, when `mu_p(A) > 0`, +`prod_i phi(p_i) ≤ H_A prod_i phi(p_i) ≤ -log mu_p(A)` from `1 ≤ H_A` (`le_mul_of_one_le_left`) +and display (F7), `hazardPhiBound`, reaching the cap by `P15Budget.Aux.le_cappedHazard_of`. +(⇒) instantiates the budget at `p ≡ p_star`, `c ≡ 1` (admissible by `P15Elementary.Aux.pStar_pos`, +`pStar_lt_one` and `phi p_star = 1`, `P15Elementary.phiAtPStar`); `mu_{p_star}(A) > 0` since +`∅ ∈ A` contributes `(1 - p_star)^n > 0` (`Finset.single_le_sum`, `P15Budget.Aux.weight_nonneg`), +so `1 ≤ min 1 (-log mu_{p_star}(A))` and `le_min_iff` gives `1 ≤ H_A`. +Does not establish: the informal display (F8) or its review and acceptance; the alignment of the +formal objects with the source's (PENDING_INDEPENDENT_REVIEW); coverage of arbitrary `A` (the +source: "it does not infer coverage of arbitrary A"); the disposition of `p15-full-price`, which +is transcribed in the register, not derived here. -/ +theorem fullGroundBudgetIff : UniversalLaw.Spec.P15.FullGroundBudgetIff := + Aux.bi_fullGroundBudgetIff_of_phiBound hazardPhiBound + +/-- Proves: `UniversalLaw.Spec.P15.LocalPriceBoundFull` (claim `p15-full-price`, display (F12)). +Method: enumerate the block by `Fin n_i` (`Aux.lp_exists_enum`), transport `mu_p(D_i)` to the +capacity family `{|T| ≤ a_i}` via `LocalRestriction` (`Aux.lp_localGood_eq_muOf`), apply +`hazardPhiBound` (display (F7)) to that proper downset (`Aux.lp_capacityFamily_properDownset`), +bound `h_star ≤ H_{n_i,a_i}` by `CapacityWorstCase` and `∏ c ≤ ∏ phi ≤ 1` by +`Finset.prod_le_prod₀`, `Finset.prod_le_one₀`; `rho_star = 1 / h_star` is definitional. +Does not establish: the informal display (F12) or its review and acceptance; the alignment of the +formal objects with the source's (PENDING_INDEPENDENT_REVIEW); the stronger inequality +`price ≤ q_i` ("The inequality price<=q_i is NOT required and is in general stronger than what +is proved here"); the disposition of `p15-full-price`, which is transcribed in the register, not +derived here. -/ +theorem localPriceBoundFull {X : Type} [Fintype X] [DecidableEq X] (F : RealizedData X) : + UniversalLaw.Spec.P15.LocalPriceBoundFull F := + Aux.lp_localPriceBoundFull_of_phiBound hazardPhiBound F + +/-- Proves: `UniversalLaw.Spec.P15.FullTransformedPriceBudget` (claim `p15-full-price`, display (F2)). +Method: `covercost ≤ 1` by the cover `{∅}` (`P15Budget.Aux.coverCost_le_one`); for `K ≥ K_H(d)` +the full blocks cover, so `covercost ≤ sum_i price(X_i)` (`P15Budget.Aux.coverCost_le_sum_block`); +when `mu_p(D) > 0` every `mu_p(D_i) > 0` (`P15Hazard.Aux.localGood_pos_of_mu_pos`) and the local +bound (F12), `localPriceBoundFull`, gives `price(X_i) ≤ rho_star [-log mu_p(D_i)]`; +`Finset.sum_le_sum`, `Finset.mul_sum` and the global assembly (F13), +`P15Hazard.globalAssemblyHazard`, give `sum_i price(X_i) ≤ rho_star [-log mu_p(D)]` with +`rho_star ≥ 0`; `P15Budget.Aux.le_cappedHazard_of` reaches the capped hazard. +Does not establish: the informal display (F2) or its review and acceptance; the alignment of the +formal objects with the source's (PENDING_INDEPENDENT_REVIEW); optimality of `rho_star` (that is +`SharpnessOfRhoStar`); any unrestricted downset or prize statement (the source: "palette size +remains K_H(d), which can depend on H and d"); the nonauthor review recorded in LANDING_CLAIMS +(REVIEWED_SCOPED), which is not reproduced or extended here; the disposition of +`p15-full-price`, which is transcribed in the register, not derived here. -/ +theorem fullTransformedPriceBudget {X : Type} [Fintype X] [DecidableEq X] (F : RealizedData X) : + UniversalLaw.Spec.P15.FullTransformedPriceBudget F := + Aux.f2_fullTransformedPriceBudget_of_local (fun F => localPriceBoundFull F) F + +end UniversalLaw.Proofs.P15Interpolation diff --git a/specifications/lean_statements_20261010/README.md b/specifications/lean_statements_20261010/README.md index 1f5d71922..6e9a1e3b0 100644 --- a/specifications/lean_statements_20261010/README.md +++ b/specifications/lean_statements_20261010/README.md @@ -4,9 +4,10 @@ Scientific effect: **NONE**. Organizational-independence credit of this packet: Claude, delegated AI work). Alignment status of every statement: `PENDING_INDEPENDENT_REVIEW`. Formal progress of every declaration here: `specified`. The sibling proof packet `specifications/lean_statement_proofs_20261011` holds theorems whose type is exactly one of these -Props (51 of the 141 Props, 52 theorems); the register lists them under the claim rows as -statement entries of kind `theorem` with label `proved` (all of them kernel-checked by the hosted run 38121713840: PR head 910809d6, -actual tested merge 5b198699… with base b2d70d77…, same tree as the head), +Props (59 of the 141 Props, 60 theorems); the register lists them under the claim rows as +statement entries of kind `theorem` with label `proved` (52 of them kernel-checked by the hosted run 38121713840: PR head 910809d6, +actual tested merge 5b198699… with base b2d70d77…, same tree as the head; the 8 of `P15Interpolation`, added after PR head 79731b96 (run 38124262242, actual tested merge 318ff194…), by run 38149888699: +PR head 0dcb0016, actual tested merge 4363b692… with base 79731b96…, the head of PR #422, same tree as the head), which changes no label of this packet and no claim-level label. No claim, premise, obligation or disposition changes because this packet exists, builds, or is green in CI, or because a Prop of it is proved. @@ -50,11 +51,11 @@ ladder; it is `specified`. ## Declarations -150 registered declarations (141 `def … : Prop`, 9 interface `structure`), every one with formal progress `specified` in this package; the 123 auxiliary definitions and abbreviations of the modules are inventory only and are not register statements. Names are given without the module namespace `UniversalLaw.Spec..`; the source column is the pinned source named by the docstring's `Source:` line. Anchors and "Not established" cells are copied verbatim from the Lean docstrings (`Anchor:` and `Does not claim:` lines) through REGISTER.json. The last column names the theorems of the sibling proof packet `specifications/lean_statement_proofs_20261011` whose type is exactly the declaration (namespace `UniversalLaw.Proofs..`): 51 of the 141 Props have one (52 theorems; `TriangleNeedsThree` is proved twice), each listed in the register under the claim rows as a statement entry of kind `theorem` with label `proved` (the label of a committed proof package; `kernel-checked` appears only in a run receipt: the hosted `lean-specification-proofs.yml` run 38121713840 receipted all of them and run 38116277597 the first 38; a pull_request run checks out the synthetic merge of the PR head into the base, so each receipt records as checked_commit that merge and not the head: run 38121713840 PR head 910809d6, actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; run 38116277597 PR head 00d2ac6e, actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with the same base; run 38122386459 corroborates on PR head d9b8dd33, actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6; each merge has the same tree as its head). That label belongs to the theorem, not to the declaration here, which stays `specified`, and not to any claim row; a kernel-checked theorem is evidence about its Prop only, and alignment of every statement is `PENDING_INDEPENDENT_REVIEW`. +150 registered declarations (141 `def … : Prop`, 9 interface `structure`), every one with formal progress `specified` in this package; the 123 auxiliary definitions and abbreviations of the modules are inventory only and are not register statements. Names are given without the module namespace `UniversalLaw.Spec..`; the source column is the pinned source named by the docstring's `Source:` line. Anchors and "Not established" cells are copied verbatim from the Lean docstrings (`Anchor:` and `Does not claim:` lines) through REGISTER.json. The last column names the theorems of the sibling proof packet `specifications/lean_statement_proofs_20261011` whose type is exactly the declaration (namespace `UniversalLaw.Proofs..`): 59 of the 141 Props have one (60 theorems; `TriangleNeedsThree` is proved twice), each listed in the register under the claim rows as a statement entry of kind `theorem` with label `proved` (the label of a committed proof package; `kernel-checked` appears only in a run receipt: the hosted `lean-specification-proofs.yml` run 38121713840 receipted the 52 theorems of PR head 910809d6 and run 38116277597 the first 38; a pull_request run checks out the synthetic merge of the PR head into the base, so each receipt records as checked_commit that merge and not the head: run 38121713840 PR head 910809d6, actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; run 38116277597 PR head 00d2ac6e, actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with the same base; run 38122386459 corroborates on PR head d9b8dd33, actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6; each merge has the same tree as its head; the 8 theorems of `P15Interpolation`, added after PR head 79731b96 (run 38124262242, actual tested merge 318ff194eecc42c39a6b27c1d7bf03f30d6a34d9 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, receipt theorem_count 52), are kernel-checked by the hosted run 38149888699 on PR head 0dcb0016 (actual tested merge 4363b6928c62da242952631c6b0357d096c3b252 with base 79731b961fac555f33be3cd90e379b246a5a80e3, the head of PR #422; receipt theorem_count 60, leanchecker PASS) and were first receipted by run 38149524759 on PR head 88c21058 (actual tested merge 3306233bbdeadb15d9b4b07b94cc52a80ed8caeb with the same base); same trees as the heads). That label belongs to the theorem, not to the declaration here, which stays `specified`, and not to any claim row; a kernel-checked theorem is evidence about its Prop only, and alignment of every statement is `PENDING_INDEPENDENT_REVIEW`. ### `Specifications/Field.lean` (12 registered declarations) -| declaration | kind | source | registered under claim rows | proved by (proof packet, `proved`; kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…, same tree as the head) | +| declaration | kind | source | registered under claim rows | proved by (proof packet, `proved`; 52 kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…; the 8 of P15Interpolation by run 38149888699: PR head 0dcb0016, actual tested merge 4363b692… with base 79731b96… (the head of PR #422); same trees as the heads) | |---|---|---|---|---| | `IsLPeriodic` | def_prop | `lifetime-parent` | `math.uniform-matrix-cap-lifetime` | — | | `IsSmooth` | def_prop | `lifetime-parent` | `math.uniform-matrix-cap-lifetime` | — | @@ -71,7 +72,7 @@ ladder; it is `specified`. ### `Specifications/Lifetime.lean` (24 registered declarations) -| declaration | kind | source | registered under claim rows | proved by (proof packet, `proved`; kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…, same tree as the head) | +| declaration | kind | source | registered under claim rows | proved by (proof packet, `proved`; 52 kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…; the 8 of P15Interpolation by run 38149888699: PR head 0dcb0016, actual tested merge 4363b692… with base 79731b96… (the head of PR #422); same trees as the heads) | |---|---|---|---|---| | `IsLPeriodic` | def_prop | `lifetime-parent` | `math.uniform-matrix-cap-lifetime` | — | | `IsSmooth` | def_prop | `lifetime-parent` | `math.uniform-matrix-cap-lifetime` | — | @@ -100,7 +101,7 @@ ladder; it is `specified`. ### `Specifications/Side24.lean` (28 registered declarations) -| declaration | kind | source | registered under claim rows | proved by (proof packet, `proved`; kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…, same tree as the head) | +| declaration | kind | source | registered under claim rows | proved by (proof packet, `proved`; 52 kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…; the 8 of P15Interpolation by run 38149888699: PR head 0dcb0016, actual tested merge 4363b692… with base 79731b96… (the head of PR #422); same trees as the heads) | |---|---|---|---|---| | `ThetaSummable` | def_prop | `side24-proof` | `side24-coefficient` | — | | `IsUnitTuple` | def_prop | `side24-proof` | `side24-coefficient` | — | @@ -133,7 +134,7 @@ ladder; it is `specified`. ### `Specifications/RN.lean` (28 registered declarations) -| declaration | kind | source | registered under claim rows | proved by (proof packet, `proved`; kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…, same tree as the head) | +| declaration | kind | source | registered under claim rows | proved by (proof packet, `proved`; 52 kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…; the 8 of P15Interpolation by run 38149888699: PR head 0dcb0016, actual tested merge 4363b692… with base 79731b96… (the head of PR #422); same trees as the heads) | |---|---|---|---|---| | `IsCriticalPoint` | def_prop | `lifetime-parent` | `rn-fixed-remote-window` | — | | `HessianHasInertia` | def_prop | `lifetime-parent` | `rn-fixed-remote-window` | — | @@ -166,7 +167,7 @@ ladder; it is `specified`. ### `Specifications/P15.lean` (58 registered declarations) -| declaration | kind | source | registered under claim rows | proved by (proof packet, `proved`; kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…, same tree as the head) | +| declaration | kind | source | registered under claim rows | proved by (proof packet, `proved`; 52 kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…; the 8 of P15Interpolation by run 38149888699: PR head 0dcb0016, actual tested merge 4363b692… with base 79731b96… (the head of PR #422); same trees as the heads) | |---|---|---|---|---| | `RealizedData` | structure | `p15-realized-covers` | `p15-realized-covers` | — | | `IsRealizedFamily` | def_prop | `p15-realized-covers` | `p15-realized-covers` | — | @@ -206,22 +207,22 @@ ladder; it is `specified`. | `CapTestAtTwoThirds` | def_prop | `p15-price-budget` | `p15-price-budget-restricted` | `P15Elementary.capTestAtTwoThirds` | | `Benchmark816TransformedRange` | def_prop | `p15-price-budget` | `p15-price-budget-restricted` | `P15Budget.benchmark816TransformedRange` | | `Benchmark816RationalPrice` | def_prop | `p15-price-budget` | `p15-price-budget-restricted` | `P15Structure.benchmark816RationalPrice` | -| `FullTransformedPriceBudget` | def_prop | `p15-full-price` | `p15-full-price`, `math.p15-full-price` | — | -| `RhoStarEnclosure` | def_prop | `p15-full-price` | `p15-full-price`, `math.p15-full-price` | — | +| `FullTransformedPriceBudget` | def_prop | `p15-full-price` | `p15-full-price`, `math.p15-full-price` | `P15Interpolation.fullTransformedPriceBudget` | +| `RhoStarEnclosure` | def_prop | `p15-full-price` | `p15-full-price`, `math.p15-full-price` | `P15Interpolation.rhoStarEnclosure` | | `RhoStarBelowSixSevenths` | def_prop | `p15-full-price` | `p15-full-price` | `P15Elementary.rhoStarBelowSixSevenths` | | `IsProperDownset` | def_prop | `p15-full-price` | `p15-full-price` | — | | `HazardStarPositive` | def_prop | `p15-full-price` | `p15-full-price` | `P15Elementary.hazardStarPositive` | -| `CoordinatewiseConcavity` | def_prop | `p15-full-price` | `p15-full-price` | — | -| `HazardProductBound` | def_prop | `p15-full-price` | `p15-full-price` | — | -| `HazardPhiBound` | def_prop | `p15-full-price` | `p15-full-price` | — | -| `FullGroundPriceBound` | def_prop | `p15-full-price` | `p15-full-price` | — | +| `CoordinatewiseConcavity` | def_prop | `p15-full-price` | `p15-full-price` | `P15Interpolation.coordinatewiseConcavity` | +| `HazardProductBound` | def_prop | `p15-full-price` | `p15-full-price` | `P15Interpolation.hazardProductBound` | +| `HazardPhiBound` | def_prop | `p15-full-price` | `p15-full-price` | `P15Interpolation.hazardPhiBound` | +| `FullGroundPriceBound` | def_prop | `p15-full-price` | `p15-full-price` | `P15Interpolation.fullGroundPriceBound` | | `PhiAtPStar` | def_prop | `p15-full-price` | `p15-full-price` | `P15Elementary.phiAtPStar` | -| `FullGroundBudgetIff` | def_prop | `p15-full-price` | `p15-full-price` | — | +| `FullGroundBudgetIff` | def_prop | `p15-full-price` | `p15-full-price` | `P15Interpolation.fullGroundBudgetIff` | | `CapacityHazardIsBinomial` | def_prop | `p15-full-price` | `p15-full-price` | `P15Elementary.capacityHazardIsBinomial` | | `OddMajorityIdentity` | def_prop | `p15-full-price` | `p15-full-price` | `P15Elementary.oddMajorityIdentity` | | `CapacityWorstCase` | def_prop | `p15-full-price` | `p15-full-price` | `P15Elementary.capacityWorstCase` | | `HStarExceedsOne` | def_prop | `p15-full-price` | `p15-full-price` | `P15Elementary.hStarExceedsOne` | -| `LocalPriceBoundFull` | def_prop | `p15-full-price` | `p15-full-price` | — | +| `LocalPriceBoundFull` | def_prop | `p15-full-price` | `p15-full-price` | `P15Interpolation.localPriceBoundFull` | | `GlobalAssemblyHazard` | def_prop | `p15-full-price` | `p15-full-price` | `P15Hazard.globalAssemblyHazard` | | `SharpnessOfRhoStar` | def_prop | `p15-full-price` | `p15-full-price`, `math.p15-full-price` | `P15Elementary.sharpnessOfRhoStar` | | `DemandOneBoundary` | def_prop | `p15-full-price` | `p15-full-price` | `P15Elementary.demandOneBoundary` | @@ -229,7 +230,7 @@ ladder; it is `specified`. ## Claims -171 claim rows: 10 `landing_claim`, 33 `graph_node`, 2 `open_obligation`, 95 `proof_index_result`, 7 `existing_lean_package`, 12 `main_experiment_proof`, 12 `exact_certificate`. Claim-level formal progress: 33 `specified` (a `def … : Prop` stating the claim itself is registered), 138 `none`; no research claim is `proved` or `kernel-checked`. 197 statement entries point at the 150 declarations of this package (all `specified`). 132 statement entries carry the label `proved` and are theorems of other packages, listed as the arithmetic skeleton or the Prop-level proof of the claim they sit under and never as the claim: 31 are the 31 Side24 arithmetic targets of main's `formal/` at origin/main `f6deeba7`; 41 are the 28 P15 arithmetic targets of main's `formal/` at `91cffbb5` (main PR #358, not yet on main; kernel evidence the hosted workspace-landing run 38096827443), each listed on every P15 row whose layer 0 source it anchors to; 60 are theorems of the proof packet `specifications/lean_statement_proofs_20261011` whose type is exactly a registered Prop of this package (52 theorems, 51 distinct Props, each listed on every row that registers its Prop; the hosted `lean-specification-proofs.yml` run 38121713840 receipted all of them as kernel-checked and run 38116277597 the first 38; a pull_request run checks out the synthetic merge of the PR head into the base, which the receipt records as checked_commit: run 38121713840 PR head 910809d6, actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; run 38116277597 PR head 00d2ac6e, actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with the same base; run 38122386459 corroborates on PR head d9b8dd33, actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6; same trees as the heads). Exactly one Prop registered as stating a claim itself has such a theorem: `DemandOneRefutation` on rows `p15-price-boundary` and `math.p15-price-boundary`; their claim-level label stays `specified` (the register admits only none/specified at claim level, alignment of the Prop with the source paragraph is PENDING_INDEPENDENT_REVIEW, and a receipt is about the Prop only), as the rows' `not established` cells record. `disposition` is the verbatim LANDING_CLAIMS value or `—` (null). Nothing in these tables is a scientific status, a review verdict or an acceptance; alignment of every statement is `PENDING_INDEPENDENT_REVIEW`. +171 claim rows: 10 `landing_claim`, 33 `graph_node`, 2 `open_obligation`, 95 `proof_index_result`, 7 `existing_lean_package`, 12 `main_experiment_proof`, 12 `exact_certificate`. Claim-level formal progress: 33 `specified` (a `def … : Prop` stating the claim itself is registered), 138 `none`; no research claim is `proved` or `kernel-checked`. 197 statement entries point at the 150 declarations of this package (all `specified`). 142 statement entries carry the label `proved` and are theorems of other packages, listed as the arithmetic skeleton or the Prop-level proof of the claim they sit under and never as the claim: 31 are the 31 Side24 arithmetic targets of main's `formal/` at origin/main `f6deeba7`; 41 are the 28 P15 arithmetic targets of main's `formal/` at `91cffbb5` (main PR #358, not yet on main; kernel evidence the hosted workspace-landing run 38096827443), each listed on every P15 row whose layer 0 source it anchors to; 70 are theorems of the proof packet `specifications/lean_statement_proofs_20261011` whose type is exactly a registered Prop of this package (60 theorems, 59 distinct Props, each listed on every row that registers its Prop; the hosted `lean-specification-proofs.yml` run 38121713840 receipted the 52 theorems of PR head 910809d6 as kernel-checked and run 38116277597 the first 38; a pull_request run checks out the synthetic merge of the PR head into the base, which the receipt records as checked_commit: run 38121713840 PR head 910809d6, actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; run 38116277597 PR head 00d2ac6e, actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with the same base; run 38122386459 corroborates on PR head d9b8dd33, actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6; same trees as the heads; the 8 theorems of `P15Interpolation`, added after PR head 79731b96 (run 38124262242, actual tested merge 318ff194eecc42c39a6b27c1d7bf03f30d6a34d9 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, receipt theorem_count 52), are kernel-checked by the hosted run 38149888699 on PR head 0dcb0016 (actual tested merge 4363b6928c62da242952631c6b0357d096c3b252 with base 79731b961fac555f33be3cd90e379b246a5a80e3, the head of PR #422; receipt theorem_count 60, leanchecker PASS) and were first receipted by run 38149524759 on PR head 88c21058 (actual tested merge 3306233bbdeadb15d9b4b07b94cc52a80ed8caeb with the same base); same trees as the heads). Exactly one Prop registered as stating a claim itself has such a theorem: `DemandOneRefutation` on rows `p15-price-boundary` and `math.p15-price-boundary`; their claim-level label stays `specified` (the register admits only none/specified at claim level, alignment of the Prop with the source paragraph is PENDING_INDEPENDENT_REVIEW, and a receipt is about the Prop only), as the rows' `not established` cells record. `disposition` is the verbatim LANDING_CLAIMS value or `—` (null). Nothing in these tables is a scientific status, a review verdict or an acceptance; alignment of every statement is `PENDING_INDEPENDENT_REVIEW`. | claim_id | kind | disposition (LANDING_CLAIMS, verbatim) | formal_progress | layer 0 source | statements | |---|---|---|---|---|---| @@ -241,7 +242,7 @@ ladder; it is `specified`. | `p15-realized-covers` | landing_claim | HOLD_WITH_DOMAIN | `specified` | `p15-realized-covers` | 27 specified: `RealizedData`, `IsRealizedFamily`, `IsGood`, `IsKDecomposable`, `IsGeneratorCover`, `IsPaletteFeasible`, `PaletteNumberAttained`, `IsMinimalForbidden`, `IsTransversal`, `MinimalForbiddenCharacterisation`, `LocalRestriction`, `LocalDecomposability`, `LocalObstructionIsFullBlock`, `LocalPriceChain`, `IndependentBlockHazard`, `FullBlockCoverIff`, `CoverCostHazardBound`, `WholeGroundChromaticNumber`, `ElementaryPaletteFormula`, `TriangleNeedsThree`, `Benchmark816IsRealized`, `Benchmark816Palette`, `Benchmark816Cover`, `Benchmark816WholeGround`, `Benchmark816MinimalForbiddenCounts`, `Benchmark816Price`, `Benchmark816UnionBound`; 12 proved (main 91cffbb5, PR #358, not on main): `benchmark_block_and_ground_sizes`, `four_block_supports_fifteen`, `minimal_forbidder_counts`, `palette_816_from_two_label_classes`, `palette_815_fails_by_counting`, `whole_ground_chromatic_818`, `elementary_palette_formula_instances`, `macro_triangle_three_colors`, `ceil_block_over_capacity_instances`, `block_occupancy_one_percent`, `low_failure_union_bound_arithmetic`, `cover_price_numerator_and_denominator_positive`; 20 proved (proof packet): `P15Elementary.triangleNeedsThree`, `P15Structure.benchmark816IsRealized`, `P15Structure.benchmark816Price`, `P15Structure.elementaryPaletteFormula`, `P15Structure.triangleNeedsThree`, `P15Structure.benchmark816Palette`, `P15Structure.localDecomposability`, `P15Structure.localObstructionIsFullBlock`, `P15Structure.fullBlockCoverIff`, `P15Structure.wholeGroundChromaticNumber`, `P15Structure.benchmark816WholeGround`, `P15Structure.minimalForbiddenCharacterisation`, `P15Structure.benchmark816MinimalForbiddenCounts`, `P15Hazard.localPriceChain`, `P15Hazard.independentBlockHazard`, `P15Covers.benchmark816Cover`, `P15Covers.localRestriction`, `P15Covers.paletteNumberAttained`, `P15Covers.benchmark816UnionBound`, `P15Budget.coverCostHazardBound` | | `p15-price-boundary` | landing_claim | EXACT_COUNTEREXAMPLE | `specified` | `p15-price-boundary` | 3 specified: `TwoCoordGeneratorPrices`, `DemandOneRefutation`, `LogOnePlusBelowIdentity`; 6 proved (main 91cffbb5, PR #358, not on main): `smallest_member_block_size`, `demand_one_good_sets`, `demand_one_obstruction`, `good_measure_three_quarters`, `generator_prices_ninths`, `minimum_generator_price_exceeds_third`; 3 proved (proof packet): `P15Elementary.twoCoordGeneratorPrices`, `P15Elementary.logOnePlusBelowIdentity`, `P15Elementary.demandOneRefutation` | | `p15-price-budget-restricted` | landing_claim | HOLD_WITH_DOMAIN | `specified` | `p15-price-budget` | 8 specified: `LogRatioBound`, `RatioExponentBound`, `RestrictedLocalBudget`, `RestrictedTransformedPriceBudget`, `RhoTestSufficient`, `CapTestAtTwoThirds`, `Benchmark816TransformedRange`, `Benchmark816RationalPrice`; 3 proved (main 91cffbb5, PR #358, not on main): `t3_ratio_at_minimal_block`, `t3_bound_finite_instances`, `explicit_rational_price_above_p`; 8 proved (proof packet): `P15Elementary.logRatioBound`, `P15Elementary.capTestAtTwoThirds`, `P15Elementary.ratioExponentBound`, `P15Structure.benchmark816RationalPrice`, `P15Budget.restrictedLocalBudget`, `P15Budget.rhoTestSufficient`, `P15Budget.restrictedTransformedPriceBudget`, `P15Budget.benchmark816TransformedRange` | -| `p15-full-price` | landing_claim | REVIEWED_SCOPED | `specified` | `p15-full-price` | 20 specified: `FullTransformedPriceBudget`, `RhoStarEnclosure`, `RhoStarBelowSixSevenths`, `IsProperDownset`, `HazardStarPositive`, `CoordinatewiseConcavity`, `HazardProductBound`, `HazardPhiBound`, `FullGroundPriceBound`, `PhiAtPStar`, `FullGroundBudgetIff`, `CapacityHazardIsBinomial`, `OddMajorityIdentity`, `CapacityWorstCase`, `HStarExceedsOne`, `LocalPriceBoundFull`, `GlobalAssemblyHazard`, `SharpnessOfRhoStar`, `DemandOneBoundary`, `SixSeventhsCertificate`; 7 proved (main 91cffbb5, PR #358, not on main): `rho_star_endpoints_adjacent`, `rho_star_upper_endpoint_below_six_sevenths`, `sixteen_twentysevenths_below_six_sevenths`, `minimal_block_size_instances`, `e_rational_bounds_ordering`, `exp_eleven_sixths_taylor_certificate`, `h_star_rational_certificate_constants`; 11 proved (proof packet): `P15Elementary.rhoStarBelowSixSevenths`, `P15Elementary.sixSeventhsCertificate`, `P15Elementary.hStarExceedsOne`, `P15Elementary.phiAtPStar`, `P15Elementary.hazardStarPositive`, `P15Elementary.oddMajorityIdentity`, `P15Elementary.capacityWorstCase`, `P15Elementary.demandOneBoundary`, `P15Elementary.capacityHazardIsBinomial`, `P15Elementary.sharpnessOfRhoStar`, `P15Hazard.globalAssemblyHazard` | +| `p15-full-price` | landing_claim | REVIEWED_SCOPED | `specified` | `p15-full-price` | 20 specified: `FullTransformedPriceBudget`, `RhoStarEnclosure`, `RhoStarBelowSixSevenths`, `IsProperDownset`, `HazardStarPositive`, `CoordinatewiseConcavity`, `HazardProductBound`, `HazardPhiBound`, `FullGroundPriceBound`, `PhiAtPStar`, `FullGroundBudgetIff`, `CapacityHazardIsBinomial`, `OddMajorityIdentity`, `CapacityWorstCase`, `HStarExceedsOne`, `LocalPriceBoundFull`, `GlobalAssemblyHazard`, `SharpnessOfRhoStar`, `DemandOneBoundary`, `SixSeventhsCertificate`; 7 proved (main 91cffbb5, PR #358, not on main): `rho_star_endpoints_adjacent`, `rho_star_upper_endpoint_below_six_sevenths`, `sixteen_twentysevenths_below_six_sevenths`, `minimal_block_size_instances`, `e_rational_bounds_ordering`, `exp_eleven_sixths_taylor_certificate`, `h_star_rational_certificate_constants`; 19 proved (proof packet): `P15Elementary.rhoStarBelowSixSevenths`, `P15Elementary.sixSeventhsCertificate`, `P15Elementary.hStarExceedsOne`, `P15Elementary.phiAtPStar`, `P15Elementary.hazardStarPositive`, `P15Elementary.oddMajorityIdentity`, `P15Elementary.capacityWorstCase`, `P15Elementary.demandOneBoundary`, `P15Elementary.capacityHazardIsBinomial`, `P15Elementary.sharpnessOfRhoStar`, `P15Hazard.globalAssemblyHazard`, `P15Interpolation.rhoStarEnclosure`, `P15Interpolation.coordinatewiseConcavity`, `P15Interpolation.hazardProductBound`, `P15Interpolation.hazardPhiBound`, `P15Interpolation.fullGroundPriceBound`, `P15Interpolation.fullGroundBudgetIff`, `P15Interpolation.localPriceBoundFull`, `P15Interpolation.fullTransformedPriceBudget` | | `downstream-hard-gate` | landing_claim | ENGINEERING_HOLD | `none` | `downstream-graph` | — | | `math.uniform-matrix-cap-lifetime` | graph_node | — | `specified` | `lifetime-parent` | 32 specified: `IsLPeriodic`, `IsSmooth`, `GaussianFieldInterface`, `IsCriticalPoint`, `HessianHasInertia`, `IsNondegMax`, `IsIndexSaddle`, `IsCandidatePair`, `IsMorseDistinct`, `SuperlevelBarInterface`, `IsFiniteBar`, `IsLifetimeDensityVersion`, `IsLPeriodic`, `IsSmooth`, `GaussianFieldInterface`, `IsCriticalPoint`, `HessianHasInertia`, `IsNondegMax`, `IsIndexSaddle`, `IsCandidatePair`, `IsMorseDistinct`, `SuperlevelBarInterface`, `IsFiniteBar`, `IsLifetimeDensityVersion`, `IsWindowPair`, `IsWindowElderPair`, `IsUnrestrictedPair`, `PairLawInterface`, `ParentUniformSelectionA`, `ParentCompactWindowDensityB`, `IsUnrestrictedLeadingCoefficient`, `ParentUnrestrictedLeadingDensityC` | | `math.d1-component.congruence-erratum` | graph_node | — | `none` | `downstream-graph` | — | @@ -258,7 +259,7 @@ ladder; it is `specified`. | `math.rn-region.intermediate-r-to-rho` | graph_node | — | `specified` | `d5-reconciliation` | 1 specified: `D5eIntermediateShellsI3I4` | | `math.rn-region.witness-collision` | open_obligation | — | `specified` | `d5-reconciliation` | 2 specified: `WitnessCollisionNearPinPairsTarget`, `RemoteCollisionSecondFactorialD` | | `math.rn-mesoscopic-reduction` | graph_node | — | `none` | `downstream-graph` | — | -| `math.p15-full-price` | graph_node | — | `specified` | `p15-full-price` | 3 specified: `FullTransformedPriceBudget`, `RhoStarEnclosure`, `SharpnessOfRhoStar`; 7 proved (main 91cffbb5, PR #358, not on main): `rho_star_endpoints_adjacent`, `rho_star_upper_endpoint_below_six_sevenths`, `sixteen_twentysevenths_below_six_sevenths`, `minimal_block_size_instances`, `e_rational_bounds_ordering`, `exp_eleven_sixths_taylor_certificate`, `h_star_rational_certificate_constants`; 1 proved (proof packet): `P15Elementary.sharpnessOfRhoStar` | +| `math.p15-full-price` | graph_node | — | `specified` | `p15-full-price` | 3 specified: `FullTransformedPriceBudget`, `RhoStarEnclosure`, `SharpnessOfRhoStar`; 7 proved (main 91cffbb5, PR #358, not on main): `rho_star_endpoints_adjacent`, `rho_star_upper_endpoint_below_six_sevenths`, `sixteen_twentysevenths_below_six_sevenths`, `minimal_block_size_instances`, `e_rational_bounds_ordering`, `exp_eleven_sixths_taylor_certificate`, `h_star_rational_certificate_constants`; 3 proved (proof packet): `P15Elementary.sharpnessOfRhoStar`, `P15Interpolation.rhoStarEnclosure`, `P15Interpolation.fullTransformedPriceBudget` | | `math.p15-price-boundary` | graph_node | — | `specified` | `p15-price-boundary` | 2 specified: `TwoCoordGeneratorPrices`, `DemandOneRefutation`; 6 proved (main 91cffbb5, PR #358, not on main): `smallest_member_block_size`, `demand_one_good_sets`, `demand_one_obstruction`, `good_measure_three_quarters`, `generator_prices_ninths`, `minimum_generator_price_exceeds_third`; 2 proved (proof packet): `P15Elementary.twoCoordGeneratorPrices`, `P15Elementary.demandOneRefutation` | | `math.rn-selector-region-crosswalk` | graph_node | — | `none` | `downstream-graph` | — | | `math.rn-fixed-annulus-window` | graph_node | — | `specified` | `rn-fixed-annulus-window` | 1 specified: `FixedAnnulusWindowCandidateA2` | @@ -353,13 +354,15 @@ Packets listed by PROOF_INDEX by id only (82 rows, kind `proof_index_result`, fo * Not a scientific status. Dispositions in the register are transcribed verbatim from `claims/LANDING_CLAIMS.json` at the pinned commit; the checker refuses any other value. * Not changed by the proof packet. `specifications/lean_statement_proofs_20261011` depends on this - packet by path and holds 52 theorems whose type is exactly one of 51 registered Props (P15, Side24 + packet by path and holds 60 theorems whose type is exactly one of 59 registered Props (P15, Side24 and RN families; see the last column of the declaration tables). The register lists those theorems under the claim rows with label `proved`, the label of a committed proof package; `kernel-checked` - appears only in that packet's hosted run receipts (`lean-specification-proofs.yml`; run 38121713840 receipted all of its - theorems and run 38116277597 the first 38; each receipt's checked_commit is the synthetic merge of the PR head into the + appears only in that packet's hosted run receipts (`lean-specification-proofs.yml`; run 38121713840 receipted the 52 + theorems of PR head 910809d6 and run 38116277597 the first 38; each receipt's checked_commit is the synthetic merge of the PR head into the base that a pull_request run checks out, not the head itself: run 38121713840 PR head 910809d6, actual tested merge 5b198699…; run 38116277597 - PR head 00d2ac6e, actual tested merge c4c66bb8…; both with base b2d70d77… and each with the same tree as its head). + PR head 00d2ac6e, actual tested merge c4c66bb8…; both with base b2d70d77… and each with the same tree as its head; the 8 theorems + of `P15Interpolation`, added after PR head 79731b96 (run 38124262242, actual tested merge 318ff194…), are receipted by run 38149888699: PR head 0dcb0016, actual tested + merge 4363b692… with base 79731b96…, the head of PR #422, and first by run 38149524759: PR head 88c21058, actual tested merge 3306233b…, same base). The 150 declarations here remain `specified`; a kernel-checked theorem is evidence about its Prop only, never about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; no claim-level label is `proved`, including the one row (`p15-price-boundary`) whose diff --git a/specifications/lean_statements_20261010/REGISTER.json b/specifications/lean_statements_20261010/REGISTER.json index 42f317888..4bcb02696 100644 --- a/specifications/lean_statements_20261010/REGISTER.json +++ b/specifications/lean_statements_20261010/REGISTER.json @@ -789,7 +789,7 @@ { "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", "receipt_or_workflow": ".github/workflows/lean-specification-proofs.yml; hosted run 38121713840 (PR head 910809d6; actual tested checkout the merge commit 5b198699308e0585904c21d12bf540cf2475d2f0 of that head into base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, the synthetic merge GitHub builds for a pull_request run, whose tree equals the head's and which the receipt records as checked_commit) (job proof-evidence, artifact lean-specification-proofs-38121713840-1, sha256 640682d631d052f4903d66f506740ae8fa91d19185001e70a1502f404eb44175): receipt formalization_status kernel-checked, leanchecker PASS, theorem_count 52, worktree CLEAN; the 38 theorems of PR head 00d2ac6e were first receipted by run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; artifact lean-specification-proofs-38116277597-1); corroborated on PR head d9b8dd33 by run 38122386459 (actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; receipt formalization_status kernel-checked, theorem_count 52, worktree CLEAN; artifact lean-specification-proofs-38122386459-1, sha256 edd52190d6af5828e8229c161c3b77e87a540caf440070d66b1b7f415008ebc3)", - "note": "5 theorem(s) of this row (Side24Elementary.exponentialBounds, Side24Elementary.successiveTermRatio, Side24Elementary.coneMomentD2Algebra, Side24Elementary.referenceCoefficientIdentity, Side24Elementary.elementaryConeIntegral) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 52 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability}.lean, 51 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 5 of them (Side24Elementary.exponentialBounds, Side24Elementary.successiveTermRatio, Side24Elementary.coneMomentD2Algebra, Side24Elementary.referenceCoefficientIdentity, Side24Elementary.elementaryConeIntegral) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1), and again by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2). `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." + "note": "5 theorem(s) of this row (Side24Elementary.exponentialBounds, Side24Elementary.successiveTermRatio, Side24Elementary.coneMomentD2Algebra, Side24Elementary.referenceCoefficientIdentity, Side24Elementary.elementaryConeIntegral) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 60 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability,P15Interpolation}.lean, 59 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 5 of them (Side24Elementary.exponentialBounds, Side24Elementary.successiveTermRatio, Side24Elementary.coneMomentD2Algebra, Side24Elementary.referenceCoefficientIdentity, Side24Elementary.elementaryConeIntegral) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1). `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." } ], "not_established": "Nothing here encloses the coefficient. CoefficientEnclosure and ReferenceComparison are statements for any object satisfying PeriodicCoefficientInterface; the interface takes the cone moment D_u of (15.1) as a GIVEN field, so c_{d,24} is not uniquely determined in Lean and no inhabitant is constructed. The 27 main theorems listed as `proved` are the integer/rational arithmetic skeleton of PROOF.md sections 1-4 (coefficient sums, shell constants, Taylor partial sum, block minors, cone-moment algebra), not the Gaussian conditioning, the Rayleigh cone integration, the Stirling log-gamma step (section 5, not specified), the interval arithmetic of coefficient.py, or the enclosure itself. ExponentialBounds, SuccessiveTermRatio, ConeMomentD2Algebra, ReferenceCoefficientIdentity and ElementaryConeIntegral have theorems of exactly their type in the proof packet specifications/lean_statement_proofs_20261011 (5 entries below, label `proved`; the hosted lean-specification-proofs.yml run 38116277597 (PR head 00d2ac6e; actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) kernel-checked them (receipt formalization_status kernel-checked, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound})): elementary real inequalities, the term ratio, the D2 cone-moment algebra, the reference-coefficient identity as stated (its left side is not identified with the parent formula (15.2) at the reference law: rotational invariance of K_infty is not specified) and the elementary cone integral; none of them is the Gaussian conditioning, ConeMomentD1Identity / ConeMomentD2Identity, RayleighSquareLaw, LatticeImageSumBound or any enclosure of the coefficient, and the claim-level label stays `specified`. The persistence interpretation through the parent Theorem C (eq. 15.2) is conditional on the parent and untouched. Disposition REVIEWED_SCOPED is transcribed, not re-derived. Nonauthor review and acceptance are not claimed by any statement; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet is 0. The interface does not determine c_{d,24}: CoefficientEnclosure and ReferenceComparison are predicates on the interface object, not closed statements; their universal closure over all inhabitants is false whenever the interface is inhabited (scaling the given cone moment by a positive constant scales c24 through eq_15_2 and gives another inhabitant), and `specified` refers to the statement shape at the source's object, which is not constructed.", @@ -953,7 +953,7 @@ { "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", "receipt_or_workflow": ".github/workflows/lean-specification-proofs.yml; hosted run 38121713840 (PR head 910809d6; actual tested checkout the merge commit 5b198699308e0585904c21d12bf540cf2475d2f0 of that head into base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, the synthetic merge GitHub builds for a pull_request run, whose tree equals the head's and which the receipt records as checked_commit) (job proof-evidence, artifact lean-specification-proofs-38121713840-1, sha256 640682d631d052f4903d66f506740ae8fa91d19185001e70a1502f404eb44175): receipt formalization_status kernel-checked, leanchecker PASS, theorem_count 52, worktree CLEAN; the 38 theorems of PR head 00d2ac6e were first receipted by run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; artifact lean-specification-proofs-38116277597-1); corroborated on PR head d9b8dd33 by run 38122386459 (actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; receipt formalization_status kernel-checked, theorem_count 52, worktree CLEAN; artifact lean-specification-proofs-38122386459-1, sha256 edd52190d6af5828e8229c161c3b77e87a540caf440070d66b1b7f415008ebc3)", - "note": "5 theorem(s) of this row (RNProbability.conditionalMeanIdentityN3, RNProbability.holderCountBoundN1, RNProbability.holderConsequenceN2, RNProbability.uniformCounterexampleN4, RNProbability.exponentialTailLayerCakeN5) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 52 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability}.lean, 51 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 5 of them (RNProbability.conditionalMeanIdentityN3, RNProbability.holderCountBoundN1, RNProbability.holderConsequenceN2, RNProbability.uniformCounterexampleN4, RNProbability.exponentialTailLayerCakeN5) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1), and again by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2). `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." + "note": "5 theorem(s) of this row (RNProbability.conditionalMeanIdentityN3, RNProbability.holderCountBoundN1, RNProbability.holderConsequenceN2, RNProbability.uniformCounterexampleN4, RNProbability.exponentialTailLayerCakeN5) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 60 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability,P15Interpolation}.lean, 59 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 5 of them (RNProbability.conditionalMeanIdentityN3, RNProbability.holderCountBoundN1, RNProbability.holderConsequenceN2, RNProbability.uniformCounterexampleN4, RNProbability.exponentialTailLayerCakeN5) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1). `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." } ], "not_established": "No Prop states Theorem N as a whole, so the claim-level label stays none: (N1)-(N5) (Hoelder bound, its power-law consequence, the conditional-mean identity, the uniform counterexample, the exponential-tail layer cake) are stated as abstract probability-space Props and each has a theorem of exactly its type in the proof packet specifications/lean_statement_proofs_20261011 (5 entries below, label `proved`; the hosted lean-specification-proofs.yml run 38116277597 (PR head 00d2ac6e; actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) kernel-checked them (receipt formalization_status kernel-checked, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound})); (N6) (the full-pin weighted Kac-Rice expression for E_Q^W N_B) and (N7) (the enclosure-to-rate implication under Z_r >= z_* r^2) are NOT stated, and they are the Gaussian numerator interface that the disposition reason calls \"a target rather than a discharged global RN theorem\". The five theorems prove the Props for the abstract probability spaces and counts they quantify over: nothing about the Gaussian model is stated or proved; no RN rate, no 24-jet enclosure, no ENV-RESCOV discharge; D3-LEMMA-RN-UNIF stays not closed. Disposition HOLD_WITH_DOMAIN is transcribed, not re-derived. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0.", @@ -1597,7 +1597,7 @@ { "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", "receipt_or_workflow": ".github/workflows/lean-specification-proofs.yml; hosted run 38121713840 (PR head 910809d6; actual tested checkout the merge commit 5b198699308e0585904c21d12bf540cf2475d2f0 of that head into base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, the synthetic merge GitHub builds for a pull_request run, whose tree equals the head's and which the receipt records as checked_commit) (job proof-evidence, artifact lean-specification-proofs-38121713840-1, sha256 640682d631d052f4903d66f506740ae8fa91d19185001e70a1502f404eb44175): receipt formalization_status kernel-checked, leanchecker PASS, theorem_count 52, worktree CLEAN; the 38 theorems of PR head 00d2ac6e were first receipted by run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; artifact lean-specification-proofs-38116277597-1); corroborated on PR head d9b8dd33 by run 38122386459 (actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; receipt formalization_status kernel-checked, theorem_count 52, worktree CLEAN; artifact lean-specification-proofs-38122386459-1, sha256 edd52190d6af5828e8229c161c3b77e87a540caf440070d66b1b7f415008ebc3)", - "note": "20 theorem(s) of this row (P15Elementary.triangleNeedsThree, P15Structure.benchmark816IsRealized, P15Structure.benchmark816Price, P15Structure.elementaryPaletteFormula, P15Structure.triangleNeedsThree, P15Structure.benchmark816Palette, P15Structure.localDecomposability, P15Structure.localObstructionIsFullBlock, P15Structure.fullBlockCoverIff, P15Structure.wholeGroundChromaticNumber, P15Structure.benchmark816WholeGround, P15Structure.minimalForbiddenCharacterisation, P15Structure.benchmark816MinimalForbiddenCounts, P15Hazard.localPriceChain, P15Hazard.independentBlockHazard, P15Covers.benchmark816Cover, P15Covers.localRestriction, P15Covers.paletteNumberAttained, P15Covers.benchmark816UnionBound, P15Budget.coverCostHazardBound) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 52 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability}.lean, 51 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 13 of them (P15Elementary.triangleNeedsThree, P15Structure.benchmark816IsRealized, P15Structure.benchmark816Price, P15Structure.elementaryPaletteFormula, P15Structure.triangleNeedsThree, P15Structure.benchmark816Palette, P15Structure.localDecomposability, P15Structure.localObstructionIsFullBlock, P15Structure.fullBlockCoverIff, P15Structure.wholeGroundChromaticNumber, P15Structure.benchmark816WholeGround, P15Structure.minimalForbiddenCharacterisation, P15Structure.benchmark816MinimalForbiddenCounts) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1), and again by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2). 7 (P15Hazard.localPriceChain, P15Hazard.independentBlockHazard, P15Covers.benchmark816Cover, P15Covers.localRestriction, P15Covers.paletteNumberAttained, P15Covers.benchmark816UnionBound, P15Budget.coverCostHazardBound) were added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN). `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." + "note": "20 theorem(s) of this row (P15Elementary.triangleNeedsThree, P15Structure.benchmark816IsRealized, P15Structure.benchmark816Price, P15Structure.elementaryPaletteFormula, P15Structure.triangleNeedsThree, P15Structure.benchmark816Palette, P15Structure.localDecomposability, P15Structure.localObstructionIsFullBlock, P15Structure.fullBlockCoverIff, P15Structure.wholeGroundChromaticNumber, P15Structure.benchmark816WholeGround, P15Structure.minimalForbiddenCharacterisation, P15Structure.benchmark816MinimalForbiddenCounts, P15Hazard.localPriceChain, P15Hazard.independentBlockHazard, P15Covers.benchmark816Cover, P15Covers.localRestriction, P15Covers.paletteNumberAttained, P15Covers.benchmark816UnionBound, P15Budget.coverCostHazardBound) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 60 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability,P15Interpolation}.lean, 59 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 13 of them (P15Elementary.triangleNeedsThree, P15Structure.benchmark816IsRealized, P15Structure.benchmark816Price, P15Structure.elementaryPaletteFormula, P15Structure.triangleNeedsThree, P15Structure.benchmark816Palette, P15Structure.localDecomposability, P15Structure.localObstructionIsFullBlock, P15Structure.fullBlockCoverIff, P15Structure.wholeGroundChromaticNumber, P15Structure.benchmark816WholeGround, P15Structure.minimalForbiddenCharacterisation, P15Structure.benchmark816MinimalForbiddenCounts) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1). 7 (P15Hazard.localPriceChain, P15Hazard.independentBlockHazard, P15Covers.benchmark816Cover, P15Covers.localRestriction, P15Covers.paletteNumberAttained, P15Covers.benchmark816UnionBound, P15Budget.coverCostHazardBound) were added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN). `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." } ], "not_established": "Props of this row with a theorem of exactly their type in the proof packet specifications/lean_statement_proofs_20261011: PaletteNumberAttained, MinimalForbiddenCharacterisation, LocalRestriction, LocalDecomposability, LocalObstructionIsFullBlock, LocalPriceChain, IndependentBlockHazard, FullBlockCoverIff, CoverCostHazardBound, WholeGroundChromaticNumber, ElementaryPaletteFormula, TriangleNeedsThree, Benchmark816IsRealized, Benchmark816Palette, Benchmark816Cover, Benchmark816WholeGround, Benchmark816MinimalForbiddenCounts, Benchmark816Price, Benchmark816UnionBound (20 entries below, label `proved`; 13 of them (P15Structure.minimalForbiddenCharacterisation, P15Structure.localDecomposability, P15Structure.localObstructionIsFullBlock, P15Structure.fullBlockCoverIff, P15Structure.wholeGroundChromaticNumber, P15Structure.elementaryPaletteFormula, P15Elementary.triangleNeedsThree, P15Structure.triangleNeedsThree, P15Structure.benchmark816IsRealized, P15Structure.benchmark816Palette, P15Structure.benchmark816WholeGround, P15Structure.benchmark816MinimalForbiddenCounts, P15Structure.benchmark816Price) kernel-checked by the hosted run 38116277597 (PR head 00d2ac6e; actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2); 7 of them (P15Covers.paletteNumberAttained, P15Covers.localRestriction, P15Hazard.localPriceChain, P15Hazard.independentBlockHazard, P15Budget.coverCostHazardBound, P15Covers.benchmark816Cover, P15Covers.benchmark816UnionBound) added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN)); among them Proposition P1 (MinimalForbiddenCharacterisation), both halves of Theorem P2 (FullBlockCoverIff, display (P7), and CoverCostHazardBound, display (P8)), the local statements (P2)-(P5) and the benchmark Props including the union bound (P11). Theorem-shaped Props of this row still `specified` with no theorem: none; the parametrised predicates IsRealizedFamily, IsGood, IsKDecomposable, IsGeneratorCover, IsPaletteFeasible, IsMinimalForbidden, IsTransversal are the vocabulary of the other Props, not closed statements (a theorem of their type would assert them for every argument, which is false), and are not targets. Theorem P2 is proved as the two Props state it (for the formal RealizedData record and the formal downset, prices 0 <= c_v <= p_v), which is a statement about those Props, not acceptance of the informal theorem: the claim-level label stays `specified` (this register admits only none/specified at claim level), alignment of RealizedData / IsRealizedFamily / downset / coverCost / mu with the informal objects is PENDING_INDEPENDENT_REVIEW, and the price range p_v < c_v <= phi(p_v) is a different claim row. The 12 main P15 arithmetic theorems listed as `proved` (finite arithmetic of Section 6: 409, 2454, 15, 500616, 419743994415, 816, 815*3 < 2448, 818, 409p = 1/100, the (P11) rational bound, positivity of 6/40900^409, the elementary instances of (P9)) are at commit 91cffbb5 of main PR #358, not on main; they do not count the minimal forbidders, show the palette is 816 or evaluate 6/40900^409, and the proof-packet theorems that do (Benchmark816MinimalForbiddenCounts, Benchmark816Palette, Benchmark816Price) do so for the formal RealizedData record, whose identification with the informal six-block construction is an alignment question. Nothing is asserted for prices p_v < c_v <= phi(p_v) (row p15-price-budget-restricted), for arbitrary P15 inputs or for the prize (original_prize_closed stays false). Disposition HOLD_WITH_DOMAIN is transcribed, not re-derived. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0.", @@ -1732,7 +1732,7 @@ { "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", "receipt_or_workflow": ".github/workflows/lean-specification-proofs.yml; hosted run 38121713840 (PR head 910809d6; actual tested checkout the merge commit 5b198699308e0585904c21d12bf540cf2475d2f0 of that head into base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, the synthetic merge GitHub builds for a pull_request run, whose tree equals the head's and which the receipt records as checked_commit) (job proof-evidence, artifact lean-specification-proofs-38121713840-1, sha256 640682d631d052f4903d66f506740ae8fa91d19185001e70a1502f404eb44175): receipt formalization_status kernel-checked, leanchecker PASS, theorem_count 52, worktree CLEAN; the 38 theorems of PR head 00d2ac6e were first receipted by run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; artifact lean-specification-proofs-38116277597-1); corroborated on PR head d9b8dd33 by run 38122386459 (actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; receipt formalization_status kernel-checked, theorem_count 52, worktree CLEAN; artifact lean-specification-proofs-38122386459-1, sha256 edd52190d6af5828e8229c161c3b77e87a540caf440070d66b1b7f415008ebc3)", - "note": "3 theorem(s) of this row (P15Elementary.twoCoordGeneratorPrices, P15Elementary.logOnePlusBelowIdentity, P15Elementary.demandOneRefutation) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 52 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability}.lean, 51 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 3 of them (P15Elementary.twoCoordGeneratorPrices, P15Elementary.logOnePlusBelowIdentity, P15Elementary.demandOneRefutation) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1), and again by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2). `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." + "note": "3 theorem(s) of this row (P15Elementary.twoCoordGeneratorPrices, P15Elementary.logOnePlusBelowIdentity, P15Elementary.demandOneRefutation) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 60 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability,P15Interpolation}.lean, 59 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 3 of them (P15Elementary.twoCoordGeneratorPrices, P15Elementary.logOnePlusBelowIdentity, P15Elementary.demandOneRefutation) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1). `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." } ], "not_established": "DemandOneRefutation states the refutation (the two-coordinate data form a realized family with K_H(d) = 1, obstruction {X}, admissible prices 2/3, mu_p(D) = 3/4, cover cost 4/9 > 1/3 > log(4/3)). DemandOneRefutation, TwoCoordGeneratorPrices and LogOnePlusBelowIdentity each have a theorem of exactly their type in the proof packet specifications/lean_statement_proofs_20261011 (listed below as `proved`, the label of a committed proof package; the hosted lean-specification-proofs.yml run 38116277597 (PR head 00d2ac6e; actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) kernel-checked them (receipt formalization_status kernel-checked, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound})); the two logarithm inequalities phi(1/2) = log 2 > 2/3 and log(4/3) < 1/3 are conjuncts of DemandOneRefutation and are proved inside its theorem from Mathlib's Real.log bounds. The claim-level label stays `specified`, not `proved`: this register admits only none/specified at claim level (no research claim of this programme is proved), whether DemandOneRefutation says what the source paragraph says is the independent reviewer's alignment question (PENDING_INDEPENDENT_REVIEW), the hosted run 38116277597 (PR head 00d2ac6e; actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) kernel-checked the Prop and nothing more, and a kernel-checked Prop is evidence about that Prop only. This is the one row of the register where a theorem proves the Prop registered as stating the claim itself; it is recorded here for the operator and not acted on. The 6 main P15 arithmetic theorems listed as `proved` (good sets, obstruction, 3/4 over denominator 4, prices 9,6,6,4 over 9, 3*4 > 9) are at commit 91cffbb5 of main PR #358, not on main; they are finite arithmetic, not the refutation. The counterexample does not refute d_i >= 2 successors or original P15-B (the disposition reason; the theorem's docstring says the same). Disposition EXACT_COUNTEREXAMPLE is transcribed, not re-derived. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0.", @@ -1930,7 +1930,7 @@ { "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", "receipt_or_workflow": ".github/workflows/lean-specification-proofs.yml; hosted run 38121713840 (PR head 910809d6; actual tested checkout the merge commit 5b198699308e0585904c21d12bf540cf2475d2f0 of that head into base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, the synthetic merge GitHub builds for a pull_request run, whose tree equals the head's and which the receipt records as checked_commit) (job proof-evidence, artifact lean-specification-proofs-38121713840-1, sha256 640682d631d052f4903d66f506740ae8fa91d19185001e70a1502f404eb44175): receipt formalization_status kernel-checked, leanchecker PASS, theorem_count 52, worktree CLEAN; the 38 theorems of PR head 00d2ac6e were first receipted by run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; artifact lean-specification-proofs-38116277597-1); corroborated on PR head d9b8dd33 by run 38122386459 (actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; receipt formalization_status kernel-checked, theorem_count 52, worktree CLEAN; artifact lean-specification-proofs-38122386459-1, sha256 edd52190d6af5828e8229c161c3b77e87a540caf440070d66b1b7f415008ebc3)", - "note": "8 theorem(s) of this row (P15Elementary.logRatioBound, P15Elementary.capTestAtTwoThirds, P15Elementary.ratioExponentBound, P15Structure.benchmark816RationalPrice, P15Budget.restrictedLocalBudget, P15Budget.rhoTestSufficient, P15Budget.restrictedTransformedPriceBudget, P15Budget.benchmark816TransformedRange) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 52 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability}.lean, 51 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 4 of them (P15Elementary.logRatioBound, P15Elementary.capTestAtTwoThirds, P15Elementary.ratioExponentBound, P15Structure.benchmark816RationalPrice) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1), and again by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2). 4 (P15Budget.restrictedLocalBudget, P15Budget.rhoTestSufficient, P15Budget.restrictedTransformedPriceBudget, P15Budget.benchmark816TransformedRange) were added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN). `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." + "note": "8 theorem(s) of this row (P15Elementary.logRatioBound, P15Elementary.capTestAtTwoThirds, P15Elementary.ratioExponentBound, P15Structure.benchmark816RationalPrice, P15Budget.restrictedLocalBudget, P15Budget.rhoTestSufficient, P15Budget.restrictedTransformedPriceBudget, P15Budget.benchmark816TransformedRange) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 60 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability,P15Interpolation}.lean, 59 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 4 of them (P15Elementary.logRatioBound, P15Elementary.capTestAtTwoThirds, P15Elementary.ratioExponentBound, P15Structure.benchmark816RationalPrice) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1). 4 (P15Budget.restrictedLocalBudget, P15Budget.rhoTestSufficient, P15Budget.restrictedTransformedPriceBudget, P15Budget.benchmark816TransformedRange) were added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN). `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." } ], "not_established": "RestrictedTransformedPriceBudget states (T1) for every realized family with a_i >= 1, d_i >= 2, p_v <= 1/4, c_v <= phi(p_v) and is proved as stated in the proof packet; that is evidence about the Prop (for the formal RealizedData record, downset, coverCost and mu), not acceptance of the informal theorem: the claim-level label stays `specified` (claim-level vocabulary none/specified; alignment PENDING_INDEPENDENT_REVIEW). Props of this row with a theorem of exactly their type in the proof packet specifications/lean_statement_proofs_20261011: LogRatioBound, RatioExponentBound, RestrictedLocalBudget, RestrictedTransformedPriceBudget, RhoTestSufficient, CapTestAtTwoThirds, Benchmark816TransformedRange, Benchmark816RationalPrice (8 entries below, label `proved`; 4 of them (P15Elementary.logRatioBound, P15Elementary.ratioExponentBound, P15Elementary.capTestAtTwoThirds, P15Structure.benchmark816RationalPrice) kernel-checked by the hosted run 38116277597 (PR head 00d2ac6e; actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2); 4 of them (P15Budget.restrictedLocalBudget, P15Budget.restrictedTransformedPriceBudget, P15Budget.rhoTestSufficient, P15Budget.benchmark816TransformedRange) added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN)). Theorem-shaped Props of this row still `specified` with no theorem: none. The intermediate ratio steps of (T3) are proved inside the theorems that use them; the integral representation behind (T2), the admissibility integral and the Section 5 checker program are not specified. The 3 main P15 arithmetic theorems listed as `proved` (the a = 1, n = 3 instance 16/27, finite instances of the (T3) bound and the rational identity 81801/3345620000) are at commit 91cffbb5 of main PR #358, not on main; they are not (T1). The dependency on claim p15-realized-covers is discharged only to the extent that row records. Disposition HOLD_WITH_DOMAIN (\"independent theorem review not yet source-bound in manifest\") is transcribed, not re-derived. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0.", @@ -2288,6 +2288,78 @@ "formal_progress": "proved", "anchor": " sum_i [-log mu_p(D_i)] <= -log mu_p(D). (F13)", "does_not_claim": "the informal display (F13) or its review and acceptance; the local bound (F12) or the full-price theorem (F2); any independence of crossing failures (none is used); the alignment of the formal `mu`, `localGood` with the source's `mu_p(D)`, `mu_p(D_i)` (PENDING_INDEPENDENT_REVIEW); the disposition of `p15-full-price`, which is transcribed in the register, not derived here." + }, + { + "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", + "module": "SpecificationProofs/P15Interpolation.lean", + "declaration": "UniversalLaw.Proofs.P15Interpolation.rhoStarEnclosure", + "kind": "theorem", + "formal_progress": "proved", + "anchor": " 0.84547981724898672067 < rho_star", + "does_not_claim": "the informal display (F3) or its review and acceptance; the alignment of the formal objects with the source's (PENDING_INDEPENDENT_REVIEW); the source's `full_price.py` Fraction procedure (not specified and not reproduced here: the route above is a different certificate of the same enclosure), nor any change to the `specified` status that main's `docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md` records for this target; the disposition of `p15-full-price`, which is transcribed in the register, not derived here." + }, + { + "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", + "module": "SpecificationProofs/P15Interpolation.lean", + "declaration": "UniversalLaw.Proofs.P15Interpolation.coordinatewiseConcavity", + "kind": "theorem", + "formal_progress": "proved", + "anchor": "Only SEPARATE coordinatewise concavity is asserted; joint concavity is not needed or claimed.", + "does_not_claim": "the informal display (F5) or its review and acceptance; the alignment of the formal objects with the source's (PENDING_INDEPENDENT_REVIEW); joint concavity, or the derivative formulas (F4)-(F5) themselves as registered statements (not specified; concavity is their consequence); the disposition of `p15-full-price`, which is transcribed in the register, not derived here." + }, + { + "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", + "module": "SpecificationProofs/P15Interpolation.lean", + "declaration": "UniversalLaw.Proofs.P15Interpolation.hazardProductBound", + "kind": "theorem", + "formal_progress": "proved", + "anchor": " F_A(t) >= (product_i t_i) H_A. (F6)", + "does_not_claim": "the informal display (F6) or its review and acceptance; the alignment of the formal objects with the source's (PENDING_INDEPENDENT_REVIEW); the inequality as an informal statement (the Prop is statement only); the disposition of `p15-full-price`, which is transcribed in the register, not derived here." + }, + { + "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", + "module": "SpecificationProofs/P15Interpolation.lean", + "declaration": "UniversalLaw.Proofs.P15Interpolation.hazardPhiBound", + "kind": "theorem", + "formal_progress": "proved", + "anchor": " -log mu_p(A) >= H_A product_i phi(p_i). (F7)", + "does_not_claim": "the informal display (F7) or its review and acceptance; the alignment of the formal objects with the source's (PENDING_INDEPENDENT_REVIEW); the inequality as an informal statement (the Prop is statement only), nor anything at `mu_p(A) = 0`, where the source reads the inequality as an extended one and the Prop states nothing; the disposition of `p15-full-price`, which is transcribed in the register, not derived here." + }, + { + "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", + "module": "SpecificationProofs/P15Interpolation.lean", + "declaration": "UniversalLaw.Proofs.P15Interpolation.fullGroundPriceBound", + "kind": "theorem", + "formal_progress": "proved", + "anchor": " product_i c_i <= min(1, [-log mu_p(A)]/H_A). (F8)", + "does_not_claim": "the informal display (F8) or its review and acceptance; the alignment of the formal objects with the source's (PENDING_INDEPENDENT_REVIEW); that the full-ground generator covers any obstruction (the source: \"It does not assert that this generator alone covers an arbitrary obstruction\"); the disposition of `p15-full-price`, which is transcribed in the register, not derived here." + }, + { + "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", + "module": "SpecificationProofs/P15Interpolation.lean", + "declaration": "UniversalLaw.Proofs.P15Interpolation.fullGroundBudgetIff", + "kind": "theorem", + "formal_progress": "proved", + "anchor": "a full-ground generator universally meets the capped hazard budget precisely when H_A>=1", + "does_not_claim": "the informal display (F8) or its review and acceptance; the alignment of the formal objects with the source's (PENDING_INDEPENDENT_REVIEW); coverage of arbitrary `A` (the source: \"it does not infer coverage of arbitrary A\"); the disposition of `p15-full-price`, which is transcribed in the register, not derived here." + }, + { + "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", + "module": "SpecificationProofs/P15Interpolation.lean", + "declaration": "UniversalLaw.Proofs.P15Interpolation.localPriceBoundFull", + "kind": "theorem", + "formal_progress": "proved", + "anchor": " price({X_i}) <= rho_star [-log mu_p(D_i)], (F12)", + "does_not_claim": "the informal display (F12) or its review and acceptance; the alignment of the formal objects with the source's (PENDING_INDEPENDENT_REVIEW); the stronger inequality `price ≤ q_i` (\"The inequality price<=q_i is NOT required and is in general stronger than what is proved here\"); the disposition of `p15-full-price`, which is transcribed in the register, not derived here." + }, + { + "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", + "module": "SpecificationProofs/P15Interpolation.lean", + "declaration": "UniversalLaw.Proofs.P15Interpolation.fullTransformedPriceBudget", + "kind": "theorem", + "formal_progress": "proved", + "anchor": " covercost_c(O_K(D)) <= min(1,rho_star[-log mu_p(D)]). (F2)", + "does_not_claim": "the informal display (F2) or its review and acceptance; the alignment of the formal objects with the source's (PENDING_INDEPENDENT_REVIEW); optimality of `rho_star` (that is `SharpnessOfRhoStar`); any unrestricted downset or prize statement (the source: \"palette size remains K_H(d), which can depend on H and d\"); the nonauthor review recorded in LANDING_CLAIMS (REVIEWED_SCOPED), which is not reproduced or extended here; the disposition of `p15-full-price`, which is transcribed in the register, not derived here." } ], "kernel_evidence": [ @@ -2298,12 +2370,12 @@ }, { "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", - "receipt_or_workflow": ".github/workflows/lean-specification-proofs.yml; hosted run 38121713840 (PR head 910809d6; actual tested checkout the merge commit 5b198699308e0585904c21d12bf540cf2475d2f0 of that head into base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, the synthetic merge GitHub builds for a pull_request run, whose tree equals the head's and which the receipt records as checked_commit) (job proof-evidence, artifact lean-specification-proofs-38121713840-1, sha256 640682d631d052f4903d66f506740ae8fa91d19185001e70a1502f404eb44175): receipt formalization_status kernel-checked, leanchecker PASS, theorem_count 52, worktree CLEAN; the 38 theorems of PR head 00d2ac6e were first receipted by run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; artifact lean-specification-proofs-38116277597-1); corroborated on PR head d9b8dd33 by run 38122386459 (actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; receipt formalization_status kernel-checked, theorem_count 52, worktree CLEAN; artifact lean-specification-proofs-38122386459-1, sha256 edd52190d6af5828e8229c161c3b77e87a540caf440070d66b1b7f415008ebc3)", - "note": "11 theorem(s) of this row (P15Elementary.rhoStarBelowSixSevenths, P15Elementary.sixSeventhsCertificate, P15Elementary.hStarExceedsOne, P15Elementary.phiAtPStar, P15Elementary.hazardStarPositive, P15Elementary.oddMajorityIdentity, P15Elementary.capacityWorstCase, P15Elementary.demandOneBoundary, P15Elementary.capacityHazardIsBinomial, P15Elementary.sharpnessOfRhoStar, P15Hazard.globalAssemblyHazard) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 52 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability}.lean, 51 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 8 of them (P15Elementary.rhoStarBelowSixSevenths, P15Elementary.sixSeventhsCertificate, P15Elementary.hStarExceedsOne, P15Elementary.phiAtPStar, P15Elementary.hazardStarPositive, P15Elementary.oddMajorityIdentity, P15Elementary.capacityWorstCase, P15Elementary.demandOneBoundary) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1), and again by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2). 3 (P15Elementary.capacityHazardIsBinomial, P15Elementary.sharpnessOfRhoStar, P15Hazard.globalAssemblyHazard) were added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN). `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." + "receipt_or_workflow": ".github/workflows/lean-specification-proofs.yml; hosted run 38121713840 (PR head 910809d6; actual tested checkout the merge commit 5b198699308e0585904c21d12bf540cf2475d2f0 of that head into base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, the synthetic merge GitHub builds for a pull_request run, whose tree equals the head's and which the receipt records as checked_commit) (job proof-evidence, artifact lean-specification-proofs-38121713840-1, sha256 640682d631d052f4903d66f506740ae8fa91d19185001e70a1502f404eb44175): receipt formalization_status kernel-checked, leanchecker PASS, theorem_count 52, worktree CLEAN; the 38 theorems of PR head 00d2ac6e were first receipted by run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; artifact lean-specification-proofs-38116277597-1); corroborated on PR head d9b8dd33 by run 38122386459 (actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; receipt formalization_status kernel-checked, theorem_count 52, worktree CLEAN; artifact lean-specification-proofs-38122386459-1, sha256 edd52190d6af5828e8229c161c3b77e87a540caf440070d66b1b7f415008ebc3); the theorems added after PR head 79731b96 (module P15Interpolation) are receipted by run 38149888699 (PR head 0dcb0016; actual tested merge 4363b6928c62da242952631c6b0357d096c3b252 with base 79731b961fac555f33be3cd90e379b246a5a80e3) (artifact lean-specification-proofs-38149888699-1, sha256 cdeb5c73aa03124ed0db16fa14d25fb03a8fa842457fce1e0c6565dbc5ee7ca8; receipt formalization_status kernel-checked, leanchecker PASS, theorem_count 60, worktree CLEAN) and were first receipted by run 38149524759 (PR head 88c21058; actual tested merge 3306233bbdeadb15d9b4b07b94cc52a80ed8caeb with base 79731b961fac555f33be3cd90e379b246a5a80e3) (artifact lean-specification-proofs-38149524759-1, sha256 ddefbdcc63223d05fd8ed34addbeebc199e271525d87dead01109cddc529e836); base 79731b961fac555f33be3cd90e379b246a5a80e3 is the head of PR #422; same trees as the heads", + "note": "19 theorem(s) of this row (P15Elementary.rhoStarBelowSixSevenths, P15Elementary.sixSeventhsCertificate, P15Elementary.hStarExceedsOne, P15Elementary.phiAtPStar, P15Elementary.hazardStarPositive, P15Elementary.oddMajorityIdentity, P15Elementary.capacityWorstCase, P15Elementary.demandOneBoundary, P15Elementary.capacityHazardIsBinomial, P15Elementary.sharpnessOfRhoStar, P15Hazard.globalAssemblyHazard, P15Interpolation.rhoStarEnclosure, P15Interpolation.coordinatewiseConcavity, P15Interpolation.hazardProductBound, P15Interpolation.hazardPhiBound, P15Interpolation.fullGroundPriceBound, P15Interpolation.fullGroundBudgetIff, P15Interpolation.localPriceBoundFull, P15Interpolation.fullTransformedPriceBudget) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 60 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability,P15Interpolation}.lean, 59 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 8 of them (P15Elementary.rhoStarBelowSixSevenths, P15Elementary.sixSeventhsCertificate, P15Elementary.hStarExceedsOne, P15Elementary.phiAtPStar, P15Elementary.hazardStarPositive, P15Elementary.oddMajorityIdentity, P15Elementary.capacityWorstCase, P15Elementary.demandOneBoundary) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1). 3 (P15Elementary.capacityHazardIsBinomial, P15Elementary.sharpnessOfRhoStar, P15Hazard.globalAssemblyHazard) were added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN). 8 (P15Interpolation.rhoStarEnclosure, P15Interpolation.coordinatewiseConcavity, P15Interpolation.hazardProductBound, P15Interpolation.hazardPhiBound, P15Interpolation.fullGroundPriceBound, P15Interpolation.fullGroundBudgetIff, P15Interpolation.localPriceBoundFull, P15Interpolation.fullTransformedPriceBudget) were added after PR head 79731b96 and kernel-checked by the hosted run 38149888699 (PR head 0dcb0016; actual tested merge 4363b6928c62da242952631c6b0357d096c3b252 with base 79731b961fac555f33be3cd90e379b246a5a80e3) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, theorem_count 60, worktree CLEAN; artifact lean-specification-proofs-38149888699-1, sha256 cdeb5c73aa03124ed0db16fa14d25fb03a8fa842457fce1e0c6565dbc5ee7ca8); they were first receipted by run 38149524759 (PR head 88c21058; actual tested merge 3306233bbdeadb15d9b4b07b94cc52a80ed8caeb with base 79731b961fac555f33be3cd90e379b246a5a80e3) (same Lean bytes; artifact lean-specification-proofs-38149524759-1, sha256 ddefbdcc63223d05fd8ed34addbeebc199e271525d87dead01109cddc529e836); base 79731b961fac555f33be3cd90e379b246a5a80e3 is the head of PR #422, and each merge has the same tree as its head. `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." } ], - "not_established": "FullTransformedPriceBudget states (F2), not proved; RhoStarEnclosure states (F3), not proved; SharpnessOfRhoStar states the attainment clause and is proved as stated. The claim-level label stays `specified` (claim-level vocabulary none/specified; a theorem of a Prop is evidence about that Prop, for the formal objects, not acceptance of Theorem F; alignment PENDING_INDEPENDENT_REVIEW). Props of this row with a theorem of exactly their type in the proof packet specifications/lean_statement_proofs_20261011: RhoStarBelowSixSevenths, HazardStarPositive, PhiAtPStar, CapacityHazardIsBinomial, OddMajorityIdentity, CapacityWorstCase, HStarExceedsOne, GlobalAssemblyHazard, SharpnessOfRhoStar, DemandOneBoundary, SixSeventhsCertificate (11 entries below, label `proved`; 8 of them (P15Elementary.rhoStarBelowSixSevenths, P15Elementary.hazardStarPositive, P15Elementary.phiAtPStar, P15Elementary.oddMajorityIdentity, P15Elementary.capacityWorstCase, P15Elementary.hStarExceedsOne, P15Elementary.demandOneBoundary, P15Elementary.sixSeventhsCertificate) kernel-checked by the hosted run 38116277597 (PR head 00d2ac6e; actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2); 3 of them (P15Elementary.capacityHazardIsBinomial, P15Hazard.globalAssemblyHazard, P15Elementary.sharpnessOfRhoStar) added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN)). Theorem-shaped Props of this row still `specified` with no theorem: FullTransformedPriceBudget, RhoStarEnclosure, CoordinatewiseConcavity, HazardProductBound, HazardPhiBound, FullGroundPriceBound, FullGroundBudgetIff, LocalPriceBoundFull; the parametrised predicates IsProperDownset are the vocabulary of the other Props, not closed statements (a theorem of their type would assert them for every argument, which is false), and are not targets. The derivative formulas (F4)-(F5) are not specified. SixSeventhsCertificate uses Mathlib's decimal bound on e in place of the source's series argument. The 7 main P15 arithmetic theorems listed as `proved` (finite arithmetic of the Section 6 certificate chain: adjacent 20-digit endpoints as Nat, 16/27 < 6/7, n >= 2a+1 instances, the rational orderings and the degree-5 Taylor partial sum) are at commit 91cffbb5 of main PR #358, not on main; they do not place rho_star = 1/(3 - log(3e - 2)) between the endpoints (nothing does: RhoStarEnclosure is specified only), do not prove e < 87/32 or 197/32 < exp(11/6) as real-number facts (the SixSeventhsCertificate theorem does, as that Prop states them), and are not Theorem F. The full_price.py Fraction procedure is not a kernel proof and is not specified. No arbitrary-downset or unrestricted P15 prize statement (original_prize_closed stays false). Disposition REVIEWED_SCOPED is transcribed, not re-derived. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0.", - "next_step": "Math- Mathlib lane: FullTransformedPriceBudget, RhoStarEnclosure, CoordinatewiseConcavity, HazardProductBound, HazardPhiBound, FullGroundPriceBound, FullGroundBudgetIff, LocalPriceBoundFull remain the targets of this row (RhoStarEnclosure ((F3), 20 digits) needs proof-producing exp/log enclosures; (F6)-(F8), (F12) and (F2) need the coordinatewise concavity (F4)-(F5), which is not specified); every theorem of this row has a hosted receipt (run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2)). Independent reviewer: alignment of FullTransformedPriceBudget with (F2), in particular the quantification over ALL p in [0,1]^X and the SAME palette K >= K_H(d). main: PR #358 merge (operator) so the 7 arithmetic theorems are on main." + "not_established": "FullTransformedPriceBudget states (F2) and is proved as stated; RhoStarEnclosure states (F3) and is proved as stated; SharpnessOfRhoStar states the attainment clause and is proved as stated. The claim-level label stays `specified` (claim-level vocabulary none/specified; a theorem of a Prop is evidence about that Prop, for the formal objects, not acceptance of Theorem F; alignment PENDING_INDEPENDENT_REVIEW). Theorem F is proved as FullTransformedPriceBudget states it: for the formal RealizedData record with a_i >= 1, d_i >= 2, every p in [0,1]^X, every 0 <= c_v <= phi(p_v) and the same K >= K_H(d), coverCost <= cappedHazard rho_star mu, through the coordinatewise concavity (CoordinatewiseConcavity, a theorem of exactly that Prop), (F6)-(F8), (F12) and (F13); that is evidence about those Props, not acceptance of the informal theorem. RhoStarEnclosure is proved by a rational certificate (Real.exp_bound series enclosures for e and for exp with explicit remainders, compared by norm_num), not by the source's full_price.py Fraction procedure, which remains unspecified. Props of this row with a theorem of exactly their type in the proof packet specifications/lean_statement_proofs_20261011: FullTransformedPriceBudget, RhoStarEnclosure, RhoStarBelowSixSevenths, HazardStarPositive, CoordinatewiseConcavity, HazardProductBound, HazardPhiBound, FullGroundPriceBound, PhiAtPStar, FullGroundBudgetIff, CapacityHazardIsBinomial, OddMajorityIdentity, CapacityWorstCase, HStarExceedsOne, LocalPriceBoundFull, GlobalAssemblyHazard, SharpnessOfRhoStar, DemandOneBoundary, SixSeventhsCertificate (19 entries below, label `proved`; 8 of them (P15Elementary.rhoStarBelowSixSevenths, P15Elementary.hazardStarPositive, P15Elementary.phiAtPStar, P15Elementary.oddMajorityIdentity, P15Elementary.capacityWorstCase, P15Elementary.hStarExceedsOne, P15Elementary.demandOneBoundary, P15Elementary.sixSeventhsCertificate) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1); 3 of them (P15Elementary.capacityHazardIsBinomial, P15Hazard.globalAssemblyHazard, P15Elementary.sharpnessOfRhoStar) were added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN); 8 of them (P15Interpolation.fullTransformedPriceBudget, P15Interpolation.rhoStarEnclosure, P15Interpolation.coordinatewiseConcavity, P15Interpolation.hazardProductBound, P15Interpolation.hazardPhiBound, P15Interpolation.fullGroundPriceBound, P15Interpolation.fullGroundBudgetIff, P15Interpolation.localPriceBoundFull) were added after PR head 79731b96 and kernel-checked by the hosted run 38149888699 (PR head 0dcb0016; actual tested merge 4363b6928c62da242952631c6b0357d096c3b252 with base 79731b961fac555f33be3cd90e379b246a5a80e3) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, theorem_count 60, worktree CLEAN; artifact lean-specification-proofs-38149888699-1, sha256 cdeb5c73aa03124ed0db16fa14d25fb03a8fa842457fce1e0c6565dbc5ee7ca8); they were first receipted by run 38149524759 (PR head 88c21058; actual tested merge 3306233bbdeadb15d9b4b07b94cc52a80ed8caeb with base 79731b961fac555f33be3cd90e379b246a5a80e3) (same Lean bytes; artifact lean-specification-proofs-38149524759-1, sha256 ddefbdcc63223d05fd8ed34addbeebc199e271525d87dead01109cddc529e836); base 79731b961fac555f33be3cd90e379b246a5a80e3 is the head of PR #422, and each merge has the same tree as its head). Theorem-shaped Props of this row still `specified` with no theorem: none; the parametrised predicates IsProperDownset are the vocabulary of the other Props, not closed statements (a theorem of their type would assert them for every argument, which is false), and are not targets. The derivative formulas (F4)-(F5) are not specified; CoordinatewiseConcavity, their consequence, is proved from the one-coordinate split of mu_p(A) (display (F4): affine in exp(-t_i) with coefficients 0 <= S_in <= S_out for a downset) and the second-derivative criterion for s |-> -log(a + b exp(-s)). SixSeventhsCertificate uses Mathlib's decimal bound on e in place of the source's series argument. The 7 main P15 arithmetic theorems listed as `proved` (finite arithmetic of the Section 6 certificate chain: adjacent 20-digit endpoints as Nat, 16/27 < 6/7, n >= 2a+1 instances, the rational orderings and the degree-5 Taylor partial sum) are at commit 91cffbb5 of main PR #358, not on main; they do not place rho_star = 1/(3 - log(3e - 2)) between the endpoints, do not prove e < 87/32 or 197/32 < exp(11/6) as real-number facts (the SixSeventhsCertificate theorem does, as that Prop states them), and are not Theorem F. The full_price.py Fraction procedure is not a kernel proof and is not specified. No arbitrary-downset or unrestricted P15 prize statement (original_prize_closed stays false). Disposition REVIEWED_SCOPED is transcribed, not re-derived. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0.", + "next_step": "Math- Mathlib lane: every theorem-shaped Prop of this row has a theorem (the parametrised predicates IsProperDownset are vocabulary, not targets); every theorem of this row has a hosted receipt: the 8 added after PR head 79731b96 (P15Interpolation.rhoStarEnclosure, P15Interpolation.coordinatewiseConcavity, P15Interpolation.hazardProductBound, P15Interpolation.hazardPhiBound, P15Interpolation.fullGroundPriceBound, P15Interpolation.fullGroundBudgetIff, P15Interpolation.localPriceBoundFull, P15Interpolation.fullTransformedPriceBudget) by run 38149888699 (PR head 0dcb0016; actual tested merge 4363b6928c62da242952631c6b0357d096c3b252 with base 79731b961fac555f33be3cd90e379b246a5a80e3) and first by run 38149524759 (PR head 88c21058; actual tested merge 3306233bbdeadb15d9b4b07b94cc52a80ed8caeb with base 79731b961fac555f33be3cd90e379b246a5a80e3), the others by run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2). Independent reviewer: alignment of FullTransformedPriceBudget with (F2), in particular the quantification over ALL p in [0,1]^X and the SAME palette K >= K_H(d), and of the proved interpolation chain (CoordinatewiseConcavity through LocalPriceBoundFull) with Sections 2-3 of the source. main: PR #358 merge (operator) so the 7 arithmetic theorems are on main." }, { "claim_id": "downstream-hard-gate", @@ -2870,7 +2942,7 @@ { "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", "receipt_or_workflow": ".github/workflows/lean-specification-proofs.yml; hosted run 38121713840 (PR head 910809d6; actual tested checkout the merge commit 5b198699308e0585904c21d12bf540cf2475d2f0 of that head into base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, the synthetic merge GitHub builds for a pull_request run, whose tree equals the head's and which the receipt records as checked_commit) (job proof-evidence, artifact lean-specification-proofs-38121713840-1, sha256 640682d631d052f4903d66f506740ae8fa91d19185001e70a1502f404eb44175): receipt formalization_status kernel-checked, leanchecker PASS, theorem_count 52, worktree CLEAN; the 38 theorems of PR head 00d2ac6e were first receipted by run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; artifact lean-specification-proofs-38116277597-1); corroborated on PR head d9b8dd33 by run 38122386459 (actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; receipt formalization_status kernel-checked, theorem_count 52, worktree CLEAN; artifact lean-specification-proofs-38122386459-1, sha256 edd52190d6af5828e8229c161c3b77e87a540caf440070d66b1b7f415008ebc3)", - "note": "5 theorem(s) of this row (RNProbability.conditionalMeanIdentityN3, RNProbability.holderCountBoundN1, RNProbability.holderConsequenceN2, RNProbability.uniformCounterexampleN4, RNProbability.exponentialTailLayerCakeN5) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 52 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability}.lean, 51 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 5 of them (RNProbability.conditionalMeanIdentityN3, RNProbability.holderCountBoundN1, RNProbability.holderConsequenceN2, RNProbability.uniformCounterexampleN4, RNProbability.exponentialTailLayerCakeN5) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1), and again by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2). `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." + "note": "5 theorem(s) of this row (RNProbability.conditionalMeanIdentityN3, RNProbability.holderCountBoundN1, RNProbability.holderConsequenceN2, RNProbability.uniformCounterexampleN4, RNProbability.exponentialTailLayerCakeN5) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 60 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability,P15Interpolation}.lean, 59 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 5 of them (RNProbability.conditionalMeanIdentityN3, RNProbability.holderCountBoundN1, RNProbability.holderConsequenceN2, RNProbability.uniformCounterexampleN4, RNProbability.exponentialTailLayerCakeN5) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1). `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." } ], "not_established": "See row rn-count-interface: (N1)-(N5) stated and each proved as a theorem of the proof packet (5 entries below, `proved`; kernel-checked by the hosted run 38116277597 (PR head 00d2ac6e; actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2)), (N6)-(N7) not stated, so no Prop states the interface as a whole and the node stays none; nothing about the Gaussian model is proved. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0.", @@ -3213,6 +3285,24 @@ "formal_progress": "proved", "anchor": "Replacing rho_star by any smaller constant in (F2) would make its right side strictly less than one.", "does_not_claim": "the informal sharpness claim's review or acceptance; the alignment of the Lean `tripleBlock`, `obstruction`, `coverCost` and `cappedHazard` with the source's objects (PENDING_INDEPENDENT_REVIEW); sharpness for any family other than the triple block; the budget (F2) itself; any necessity claim for multi-block families with some demand one (\"other constraints may change its budget\")." + }, + { + "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", + "module": "SpecificationProofs/P15Interpolation.lean", + "declaration": "UniversalLaw.Proofs.P15Interpolation.rhoStarEnclosure", + "kind": "theorem", + "formal_progress": "proved", + "anchor": " 0.84547981724898672067 < rho_star", + "does_not_claim": "the informal display (F3) or its review and acceptance; the alignment of the formal objects with the source's (PENDING_INDEPENDENT_REVIEW); the source's `full_price.py` Fraction procedure (not specified and not reproduced here: the route above is a different certificate of the same enclosure), nor any change to the `specified` status that main's `docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md` records for this target; the disposition of `p15-full-price`, which is transcribed in the register, not derived here." + }, + { + "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", + "module": "SpecificationProofs/P15Interpolation.lean", + "declaration": "UniversalLaw.Proofs.P15Interpolation.fullTransformedPriceBudget", + "kind": "theorem", + "formal_progress": "proved", + "anchor": " covercost_c(O_K(D)) <= min(1,rho_star[-log mu_p(D)]). (F2)", + "does_not_claim": "the informal display (F2) or its review and acceptance; the alignment of the formal objects with the source's (PENDING_INDEPENDENT_REVIEW); optimality of `rho_star` (that is `SharpnessOfRhoStar`); any unrestricted downset or prize statement (the source: \"palette size remains K_H(d), which can depend on H and d\"); the nonauthor review recorded in LANDING_CLAIMS (REVIEWED_SCOPED), which is not reproduced or extended here; the disposition of `p15-full-price`, which is transcribed in the register, not derived here." } ], "kernel_evidence": [ @@ -3223,11 +3313,11 @@ }, { "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", - "receipt_or_workflow": ".github/workflows/lean-specification-proofs.yml; hosted run 38121713840 (PR head 910809d6; actual tested checkout the merge commit 5b198699308e0585904c21d12bf540cf2475d2f0 of that head into base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, the synthetic merge GitHub builds for a pull_request run, whose tree equals the head's and which the receipt records as checked_commit) (job proof-evidence, artifact lean-specification-proofs-38121713840-1, sha256 640682d631d052f4903d66f506740ae8fa91d19185001e70a1502f404eb44175): receipt formalization_status kernel-checked, leanchecker PASS, theorem_count 52, worktree CLEAN; the 38 theorems of PR head 00d2ac6e were first receipted by run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; artifact lean-specification-proofs-38116277597-1); corroborated on PR head d9b8dd33 by run 38122386459 (actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; receipt formalization_status kernel-checked, theorem_count 52, worktree CLEAN; artifact lean-specification-proofs-38122386459-1, sha256 edd52190d6af5828e8229c161c3b77e87a540caf440070d66b1b7f415008ebc3)", - "note": "1 theorem(s) of this row (P15Elementary.sharpnessOfRhoStar) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 52 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability}.lean, 51 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 1 (P15Elementary.sharpnessOfRhoStar) were added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN). `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." + "receipt_or_workflow": ".github/workflows/lean-specification-proofs.yml; hosted run 38121713840 (PR head 910809d6; actual tested checkout the merge commit 5b198699308e0585904c21d12bf540cf2475d2f0 of that head into base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, the synthetic merge GitHub builds for a pull_request run, whose tree equals the head's and which the receipt records as checked_commit) (job proof-evidence, artifact lean-specification-proofs-38121713840-1, sha256 640682d631d052f4903d66f506740ae8fa91d19185001e70a1502f404eb44175): receipt formalization_status kernel-checked, leanchecker PASS, theorem_count 52, worktree CLEAN; the 38 theorems of PR head 00d2ac6e were first receipted by run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; artifact lean-specification-proofs-38116277597-1); corroborated on PR head d9b8dd33 by run 38122386459 (actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; receipt formalization_status kernel-checked, theorem_count 52, worktree CLEAN; artifact lean-specification-proofs-38122386459-1, sha256 edd52190d6af5828e8229c161c3b77e87a540caf440070d66b1b7f415008ebc3); the theorems added after PR head 79731b96 (module P15Interpolation) are receipted by run 38149888699 (PR head 0dcb0016; actual tested merge 4363b6928c62da242952631c6b0357d096c3b252 with base 79731b961fac555f33be3cd90e379b246a5a80e3) (artifact lean-specification-proofs-38149888699-1, sha256 cdeb5c73aa03124ed0db16fa14d25fb03a8fa842457fce1e0c6565dbc5ee7ca8; receipt formalization_status kernel-checked, leanchecker PASS, theorem_count 60, worktree CLEAN) and were first receipted by run 38149524759 (PR head 88c21058; actual tested merge 3306233bbdeadb15d9b4b07b94cc52a80ed8caeb with base 79731b961fac555f33be3cd90e379b246a5a80e3) (artifact lean-specification-proofs-38149524759-1, sha256 ddefbdcc63223d05fd8ed34addbeebc199e271525d87dead01109cddc529e836); base 79731b961fac555f33be3cd90e379b246a5a80e3 is the head of PR #422; same trees as the heads", + "note": "3 theorem(s) of this row (P15Elementary.sharpnessOfRhoStar, P15Interpolation.rhoStarEnclosure, P15Interpolation.fullTransformedPriceBudget) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 60 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability,P15Interpolation}.lean, 59 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 1 (P15Elementary.sharpnessOfRhoStar) were added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN). 2 (P15Interpolation.rhoStarEnclosure, P15Interpolation.fullTransformedPriceBudget) were added after PR head 79731b96 and kernel-checked by the hosted run 38149888699 (PR head 0dcb0016; actual tested merge 4363b6928c62da242952631c6b0357d096c3b252 with base 79731b961fac555f33be3cd90e379b246a5a80e3) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, theorem_count 60, worktree CLEAN; artifact lean-specification-proofs-38149888699-1, sha256 cdeb5c73aa03124ed0db16fa14d25fb03a8fa842457fce1e0c6565dbc5ee7ca8); they were first receipted by run 38149524759 (PR head 88c21058; actual tested merge 3306233bbdeadb15d9b4b07b94cc52a80ed8caeb with base 79731b961fac555f33be3cd90e379b246a5a80e3) (same Lean bytes; artifact lean-specification-proofs-38149524759-1, sha256 ddefbdcc63223d05fd8ed34addbeebc199e271525d87dead01109cddc529e836); base 79731b961fac555f33be3cd90e379b246a5a80e3 is the head of PR #422, and each merge has the same tree as its head. `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." } ], - "not_established": "See row p15-full-price. Of the three Props of this node, with a theorem of exactly their type in the proof packet: SharpnessOfRhoStar (1 entries below, label `proved`; 1 of them (P15Elementary.sharpnessOfRhoStar) added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN)); stated, not proved: FullTransformedPriceBudget, RhoStarEnclosure. A theorem of SharpnessOfRhoStar is about the formal triple block and the formal cover cost; none of this is Theorem F, and the node-level label stays `specified`. The 7 main P15 arithmetic theorems of source p15-full-price (at commit 91cffbb5 of main PR #358, not on main) are listed here as the arithmetic skeleton, never as the node. The price-boundary refutation is a scope boundary (GRAPH edge boundary_counterexample_not_required_premise), not a hypothesis. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0.", + "not_established": "See row p15-full-price. Of the three Props of this node, with a theorem of exactly their type in the proof packet: FullTransformedPriceBudget, RhoStarEnclosure, SharpnessOfRhoStar (3 entries below, label `proved`; 1 of them (P15Elementary.sharpnessOfRhoStar) were added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN); 2 of them (P15Interpolation.fullTransformedPriceBudget, P15Interpolation.rhoStarEnclosure) were added after PR head 79731b96 and kernel-checked by the hosted run 38149888699 (PR head 0dcb0016; actual tested merge 4363b6928c62da242952631c6b0357d096c3b252 with base 79731b961fac555f33be3cd90e379b246a5a80e3) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, theorem_count 60, worktree CLEAN; artifact lean-specification-proofs-38149888699-1, sha256 cdeb5c73aa03124ed0db16fa14d25fb03a8fa842457fce1e0c6565dbc5ee7ca8); they were first receipted by run 38149524759 (PR head 88c21058; actual tested merge 3306233bbdeadb15d9b4b07b94cc52a80ed8caeb with base 79731b961fac555f33be3cd90e379b246a5a80e3) (same Lean bytes; artifact lean-specification-proofs-38149524759-1, sha256 ddefbdcc63223d05fd8ed34addbeebc199e271525d87dead01109cddc529e836); base 79731b961fac555f33be3cd90e379b246a5a80e3 is the head of PR #422, and each merge has the same tree as its head); none of the three is left unproved. A theorem of SharpnessOfRhoStar is about the formal triple block and the formal cover cost; a theorem of FullTransformedPriceBudget is about the formal RealizedData record, downset, coverCost and mu; none of this is Theorem F, and the node-level label stays `specified`. The 7 main P15 arithmetic theorems of source p15-full-price (at commit 91cffbb5 of main PR #358, not on main) are listed here as the arithmetic skeleton, never as the node. The price-boundary refutation is a scope boundary (GRAPH edge boundary_counterexample_not_required_premise), not a hypothesis. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0.", "next_step": "As for row p15-full-price." }, { @@ -3341,7 +3431,7 @@ { "package": "d6g8k5htny-coder/Math- specifications/lean_statement_proofs_20261011", "receipt_or_workflow": ".github/workflows/lean-specification-proofs.yml; hosted run 38121713840 (PR head 910809d6; actual tested checkout the merge commit 5b198699308e0585904c21d12bf540cf2475d2f0 of that head into base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, the synthetic merge GitHub builds for a pull_request run, whose tree equals the head's and which the receipt records as checked_commit) (job proof-evidence, artifact lean-specification-proofs-38121713840-1, sha256 640682d631d052f4903d66f506740ae8fa91d19185001e70a1502f404eb44175): receipt formalization_status kernel-checked, leanchecker PASS, theorem_count 52, worktree CLEAN; the 38 theorems of PR head 00d2ac6e were first receipted by run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; artifact lean-specification-proofs-38116277597-1); corroborated on PR head d9b8dd33 by run 38122386459 (actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, same tree as the head; receipt formalization_status kernel-checked, theorem_count 52, worktree CLEAN; artifact lean-specification-proofs-38122386459-1, sha256 edd52190d6af5828e8229c161c3b77e87a540caf440070d66b1b7f415008ebc3)", - "note": "2 theorem(s) of this row (P15Elementary.twoCoordGeneratorPrices, P15Elementary.demandOneRefutation) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 52 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability}.lean, 51 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 2 of them (P15Elementary.twoCoordGeneratorPrices, P15Elementary.demandOneRefutation) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1), and again by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2). `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." + "note": "2 theorem(s) of this row (P15Elementary.twoCoordGeneratorPrices, P15Elementary.demandOneRefutation) are inventoried by the proof packet's check.py (source mode SOURCE_CHECK_PASS: 60 inventory theorems over SpecificationProofs/{P15Elementary,P15Structure,P15Hazard,P15Covers,P15Budget,Side24Elementary,RNProbability,P15Interpolation}.lean, 59 distinct registered Props, each theorem typed exactly as its registered Prop, applied to its own parameters). 2 of them (P15Elementary.twoCoordGeneratorPrices, P15Elementary.demandOneRefutation) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1). `proved` is the label of a committed proof package; `kernel-checked` appears only in a run receipt. Evidence about the registered Props only: not about the informal claim, its alignment (PENDING_INDEPENDENT_REVIEW), review or acceptance; the claim-level label is unchanged; organizational-independence credit 0 (Anthropic / Claude)." } ], "not_established": "See row p15-price-boundary: TwoCoordGeneratorPrices and DemandOneRefutation (the two Props of this node) have theorems of exactly their type in the proof packet (listed as `proved`; kernel-checked by the hosted run 38116277597 (PR head 00d2ac6e; actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2)), the two logarithm inequalities included; the claim-level label stays `specified` for the reasons given there (claim-level vocabulary none/specified, alignment PENDING_INDEPENDENT_REVIEW, a Prop-level proof is evidence about the Prop only, whatever the hosted run 38116277597 receipted). The 6 main P15 arithmetic theorems of source p15-price-boundary (at commit 91cffbb5 of main PR #358, not on main) are listed as the arithmetic skeleton, never as the node. REFUTED is the graph classification of the extension, transcribed as source identity. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0.", diff --git a/specifications/lean_statements_20261010/SCOPE.md b/specifications/lean_statements_20261010/SCOPE.md index ca462675a..5e809d269 100644 --- a/specifications/lean_statements_20261010/SCOPE.md +++ b/specifications/lean_statements_20261010/SCOPE.md @@ -6,7 +6,7 @@ Scientific effect: **NONE**. Formal progress: `specified` for every declaration. ## Boundary This package states; it does not prove. Proofs of some of its Props live in the sibling proof packet -`specifications/lean_statement_proofs_20261011` (52 theorems typed exactly as 51 of the 141 Props; +`specifications/lean_statement_proofs_20261011` (60 theorems typed exactly as 59 of the 141 Props; the last column of the declaration tables and the `proved (proof packet …)` entries of the claims table); that packet depends on this one by path, never edits it, and its theorems change no label here and no claim-level label. The five modules under `Specifications/` declare, as @@ -59,11 +59,11 @@ a theorem between string literals, an indented Prop definition, a proof written ## Declarations -150 registered declarations (141 `def … : Prop`, 9 interface `structure`), every one with formal progress `specified` in this package; the 123 auxiliary definitions and abbreviations of the modules are inventory only and are not register statements. Names are given without the module namespace `UniversalLaw.Spec..`; the source column is the pinned source named by the docstring's `Source:` line. Anchors and "Not established" cells are copied verbatim from the Lean docstrings (`Anchor:` and `Does not claim:` lines) through REGISTER.json. The last column names the theorems of the sibling proof packet `specifications/lean_statement_proofs_20261011` whose type is exactly the declaration (namespace `UniversalLaw.Proofs..`): 51 of the 141 Props have one (52 theorems; `TriangleNeedsThree` is proved twice), each listed in the register under the claim rows as a statement entry of kind `theorem` with label `proved` (the label of a committed proof package; `kernel-checked` appears only in a run receipt: the hosted `lean-specification-proofs.yml` run 38121713840 receipted all of them and run 38116277597 the first 38; a pull_request run checks out the synthetic merge of the PR head into the base, so each receipt records as checked_commit that merge and not the head: run 38121713840 PR head 910809d6, actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; run 38116277597 PR head 00d2ac6e, actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with the same base; run 38122386459 corroborates on PR head d9b8dd33, actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6; each merge has the same tree as its head). That label belongs to the theorem, not to the declaration here, which stays `specified`, and not to any claim row; a kernel-checked theorem is evidence about its Prop only, and alignment of every statement is `PENDING_INDEPENDENT_REVIEW`. +150 registered declarations (141 `def … : Prop`, 9 interface `structure`), every one with formal progress `specified` in this package; the 123 auxiliary definitions and abbreviations of the modules are inventory only and are not register statements. Names are given without the module namespace `UniversalLaw.Spec..`; the source column is the pinned source named by the docstring's `Source:` line. Anchors and "Not established" cells are copied verbatim from the Lean docstrings (`Anchor:` and `Does not claim:` lines) through REGISTER.json. The last column names the theorems of the sibling proof packet `specifications/lean_statement_proofs_20261011` whose type is exactly the declaration (namespace `UniversalLaw.Proofs..`): 59 of the 141 Props have one (60 theorems; `TriangleNeedsThree` is proved twice), each listed in the register under the claim rows as a statement entry of kind `theorem` with label `proved` (the label of a committed proof package; `kernel-checked` appears only in a run receipt: the hosted `lean-specification-proofs.yml` run 38121713840 receipted the 52 theorems of PR head 910809d6 and run 38116277597 the first 38; a pull_request run checks out the synthetic merge of the PR head into the base, so each receipt records as checked_commit that merge and not the head: run 38121713840 PR head 910809d6, actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; run 38116277597 PR head 00d2ac6e, actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with the same base; run 38122386459 corroborates on PR head d9b8dd33, actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6; each merge has the same tree as its head; the 8 theorems of `P15Interpolation`, added after PR head 79731b96 (run 38124262242, actual tested merge 318ff194eecc42c39a6b27c1d7bf03f30d6a34d9 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, receipt theorem_count 52), are kernel-checked by the hosted run 38149888699 on PR head 0dcb0016 (actual tested merge 4363b6928c62da242952631c6b0357d096c3b252 with base 79731b961fac555f33be3cd90e379b246a5a80e3, the head of PR #422; receipt theorem_count 60, leanchecker PASS) and were first receipted by run 38149524759 on PR head 88c21058 (actual tested merge 3306233bbdeadb15d9b4b07b94cc52a80ed8caeb with the same base); same trees as the heads). That label belongs to the theorem, not to the declaration here, which stays `specified`, and not to any claim row; a kernel-checked theorem is evidence about its Prop only, and alignment of every statement is `PENDING_INDEPENDENT_REVIEW`. ### `Specifications/Field.lean` (12 registered declarations) -| declaration | kind | source | exact coverage (verbatim anchor) | Not established (verbatim `Does not claim:`) | proved by (proof packet, `proved`; kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…, same tree as the head) | +| declaration | kind | source | exact coverage (verbatim anchor) | Not established (verbatim `Does not claim:`) | proved by (proof packet, `proved`; 52 kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…; the 8 of P15Interpolation by run 38149888699: PR head 0dcb0016, actual tested merge 4363b692… with base 79731b96… (the head of PR #422); same trees as the heads) | |---|---|---|---|---|---| | `IsLPeriodic` | def_prop | `lifetime-parent` | On the flat torus X = R^d/(L Z^d), let f be the centered stationary Gaussian field of variance one with covariance | anything about the field. | — | | `IsSmooth` | def_prop | `lifetime-parent` | In particular the field has a smooth version and all finite moments of its global derivative suprema exist. | existence of a smooth version, or moment bounds on derivative suprema. | — | @@ -80,7 +80,7 @@ a theorem between string literals, an indented Prop definition, a proof written ### `Specifications/Lifetime.lean` (24 registered declarations) -| declaration | kind | source | exact coverage (verbatim anchor) | Not established (verbatim `Does not claim:`) | proved by (proof packet, `proved`; kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…, same tree as the head) | +| declaration | kind | source | exact coverage (verbatim anchor) | Not established (verbatim `Does not claim:`) | proved by (proof packet, `proved`; 52 kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…; the 8 of P15Interpolation by run 38149888699: PR head 0dcb0016, actual tested merge 4363b692… with base 79731b96… (the head of PR #422); same trees as the heads) | |---|---|---|---|---|---| | `IsLPeriodic` | def_prop | `lifetime-parent` | On the flat torus X = R^d/(L Z^d), let f be the centered stationary Gaussian field of variance one with covariance | anything about the field. | — | | `IsSmooth` | def_prop | `lifetime-parent` | In particular the field has a smooth version and all finite moments of its global derivative suprema exist. | existence of a smooth version, or moment bounds on derivative suprema. | — | @@ -109,7 +109,7 @@ a theorem between string literals, an indented Prop definition, a proof written ### `Specifications/Side24.lean` (28 registered declarations) -| declaration | kind | source | exact coverage (verbatim anchor) | Not established (verbatim `Does not claim:`) | proved by (proof packet, `proved`; kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…, same tree as the head) | +| declaration | kind | source | exact coverage (verbatim anchor) | Not established (verbatim `Does not claim:`) | proved by (proof packet, `proved`; 52 kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…; the 8 of P15Interpolation by run 38149888699: PR head 0dcb0016, actual tested merge 4363b692… with base 79731b96… (the head of PR #422); same trees as the heads) | |---|---|---|---|---|---| | `ThetaSummable` | def_prop | `side24-proof` | K_24(z) = sum_{n in Z^d} exp(-\|z+24n\|^2/2) | that the family is summable (true, but not shown here). | — | | `IsUnitTuple` | def_prop | `side24-proof` | For q<=6 unit directional differentiations of phi(x)=exp(-\|x\|^2/2), product-rule | anything. | — | @@ -142,7 +142,7 @@ a theorem between string literals, an indented Prop definition, a proof written ### `Specifications/RN.lean` (28 registered declarations) -| declaration | kind | source | exact coverage (verbatim anchor) | Not established (verbatim `Does not claim:`) | proved by (proof packet, `proved`; kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…, same tree as the head) | +| declaration | kind | source | exact coverage (verbatim anchor) | Not established (verbatim `Does not claim:`) | proved by (proof packet, `proved`; 52 kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…; the 8 of P15Interpolation by run 38149888699: PR head 0dcb0016, actual tested merge 4363b692… with base 79731b96… (the head of PR #422); same trees as the heads) | |---|---|---|---|---|---| | `IsCriticalPoint` | def_prop | `lifetime-parent` | grad f(M)=grad f(S)=0. | differentiability of `g` at `x` (if `g` is not differentiable, `fderiv` is `0`). | — | | `HessianHasInertia` | def_prop | `lifetime-parent` | The index counts negative eigenvalues. | equivalence with an eigenvalue count for a non-symmetric form. | — | @@ -175,7 +175,7 @@ a theorem between string literals, an indented Prop definition, a proof written ### `Specifications/P15.lean` (58 registered declarations) -| declaration | kind | source | exact coverage (verbatim anchor) | Not established (verbatim `Does not claim:`) | proved by (proof packet, `proved`; kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…, same tree as the head) | +| declaration | kind | source | exact coverage (verbatim anchor) | Not established (verbatim `Does not claim:`) | proved by (proof packet, `proved`; 52 kernel-checked by hosted run 38121713840: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…; the 8 of P15Interpolation by run 38149888699: PR head 0dcb0016, actual tested merge 4363b692… with base 79731b96… (the head of PR #422); same trees as the heads) | |---|---|---|---|---|---| | `RealizedData` | structure | `p15-realized-covers` | Choose positive integers a_i,d_i and disjoint original-coordinate blocks X_i with | that the data satisfy the sources' side conditions (that is `IsRealizedFamily`). | — | | `IsRealizedFamily` | def_prop | `p15-realized-covers` | n_i=\|X_i\|=a_i d_i+1. | that any particular data record satisfies it. | — | @@ -215,22 +215,22 @@ a theorem between string literals, an indented Prop definition, a proof written | `CapTestAtTwoThirds` | def_prop | `p15-price-budget` | or if q>=2/3 (then phi(q)=1, since log3>1) | the statement (statement only); the integral proof of `log 3 > 1` is not specified; the checker program of that section is not specified. | `P15Elementary.capTestAtTwoThirds` | | `Benchmark816TransformedRange` | def_prop | `p15-price-budget` | 0<=c_v<=log(40900/40899), | the statement (statement only); "No large witness enumeration" is involved, nor any claim about earlier P15 inputs. | `P15Budget.benchmark816TransformedRange` | | `Benchmark816RationalPrice` | def_prop | `p15-price-budget` | 6*log(40900/40899)^409 <=6/(40899^409). (T7) | the statements (statement only); the rational identity `1/40900 + (1/40900)^2/2 = 81801/3345620000` is exact arithmetic not re-proved here; admissibility rests on `integral_0^p 1/(1-t) dt > integral_0^p (1+t) dt`, which is not specified. | `P15Structure.benchmark816RationalPrice` | -| `FullTransformedPriceBudget` | def_prop | `p15-full-price` | covercost_c(O_K(D)) <= min(1,rho_star[-log mu_p(D)]). (F2) | the bound (statement only); optimality of `rho_star` (that is `SharpnessOfRhoStar`); any unrestricted downset or prize statement (the source: "palette size remains K_H(d), which can depend on H and d"); the nonauthor review recorded in LANDING_CLAIMS (REVIEWED_SCOPED) is not reproduced or extended here. | — | -| `RhoStarEnclosure` | def_prop | `p15-full-price` | 0.84547981724898672067 < rho_star | the enclosure (statement only; the source's `full_price.py` Fraction procedure is not a kernel proof and is not specified); this is the next full-result target named in main's `docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md`, still at `specified`. | — | +| `FullTransformedPriceBudget` | def_prop | `p15-full-price` | covercost_c(O_K(D)) <= min(1,rho_star[-log mu_p(D)]). (F2) | the bound (statement only); optimality of `rho_star` (that is `SharpnessOfRhoStar`); any unrestricted downset or prize statement (the source: "palette size remains K_H(d), which can depend on H and d"); the nonauthor review recorded in LANDING_CLAIMS (REVIEWED_SCOPED) is not reproduced or extended here. | `P15Interpolation.fullTransformedPriceBudget` | +| `RhoStarEnclosure` | def_prop | `p15-full-price` | 0.84547981724898672067 < rho_star | the enclosure (statement only; the source's `full_price.py` Fraction procedure is not a kernel proof and is not specified); this is the next full-result target named in main's `docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md`, still at `specified`. | `P15Interpolation.rhoStarEnclosure` | | `RhoStarBelowSixSevenths` | def_prop | `p15-full-price` | Thus 6/7 is a simpler valid rational factor. | the inequality (statement only); `16/27 < 6/7` is a core-Lean target on main. | `P15Elementary.rhoStarBelowSixSevenths` | | `IsProperDownset` | def_prop | `p15-full-price` | Let A be any proper decreasing family on n>=1 coordinates containing the empty set. | anything. | — | | `HazardStarPositive` | def_prop | `p15-full-price` | The probability is positive on this compact cube because the empty set is admitted and every p_i(t)<1. | the statement (statement only). | `P15Elementary.hazardStarPositive` | -| `CoordinatewiseConcavity` | def_prop | `p15-full-price` | Only SEPARATE coordinatewise concavity is asserted; joint concavity is not needed or claimed. | the statement (statement only); joint concavity; the derivative formulas (F4)-(F5) themselves (not specified; concavity is their consequence). | — | -| `HazardProductBound` | def_prop | `p15-full-price` | F_A(t) >= (product_i t_i) H_A. (F6) | the inequality (statement only). | — | -| `HazardPhiBound` | def_prop | `p15-full-price` | -log mu_p(A) >= H_A product_i phi(p_i). (F7) | the inequality (statement only). | — | -| `FullGroundPriceBound` | def_prop | `p15-full-price` | product_i c_i <= min(1, [-log mu_p(A)]/H_A). (F8) | the inequality (statement only); that the full-ground generator covers any obstruction ("It does not assert that this generator alone covers an arbitrary obstruction"). | — | +| `CoordinatewiseConcavity` | def_prop | `p15-full-price` | Only SEPARATE coordinatewise concavity is asserted; joint concavity is not needed or claimed. | the statement (statement only); joint concavity; the derivative formulas (F4)-(F5) themselves (not specified; concavity is their consequence). | `P15Interpolation.coordinatewiseConcavity` | +| `HazardProductBound` | def_prop | `p15-full-price` | F_A(t) >= (product_i t_i) H_A. (F6) | the inequality (statement only). | `P15Interpolation.hazardProductBound` | +| `HazardPhiBound` | def_prop | `p15-full-price` | -log mu_p(A) >= H_A product_i phi(p_i). (F7) | the inequality (statement only). | `P15Interpolation.hazardPhiBound` | +| `FullGroundPriceBound` | def_prop | `p15-full-price` | product_i c_i <= min(1, [-log mu_p(A)]/H_A). (F8) | the inequality (statement only); that the full-ground generator covers any obstruction ("It does not assert that this generator alone covers an arbitrary obstruction"). | `P15Interpolation.fullGroundPriceBound` | | `PhiAtPStar` | def_prop | `p15-full-price` | at every p_i=p_star and every c_i=1, the two sides of (F7) are equal | the identity (statement only). | `P15Elementary.phiAtPStar` | -| `FullGroundBudgetIff` | def_prop | `p15-full-price` | a full-ground generator universally meets the capped hazard budget precisely when H_A>=1 | the equivalence (statement only); coverage of arbitrary `A` ("it does not infer coverage of arbitrary A"). | — | +| `FullGroundBudgetIff` | def_prop | `p15-full-price` | a full-ground generator universally meets the capped hazard budget precisely when H_A>=1 | the equivalence (statement only); coverage of arbitrary `A` ("it does not infer coverage of arbitrary A"). | `P15Interpolation.fullGroundBudgetIff` | | `CapacityHazardIsBinomial` | def_prop | `p15-full-price` | H_(n,a)=-log P(Bin(n,p_star)<=a). (F9) | the identity (statement only; a finite identity for each `n`, general in `n`). | `P15Elementary.capacityHazardIsBinomial` | | `OddMajorityIdentity` | def_prop | `p15-full-price` | =p(1-2p)P(S=a)<0. (F10) | the identities (statement only; polynomial identities in `p`, a future kernel target for each fixed `a` and by induction in general). | `P15Elementary.oddMajorityIdentity` | | `CapacityWorstCase` | def_prop | `p15-full-price` | =3-log(3e-2)=h_star>1. (F11) | the statements (statement only); the source stresses "it is not a finite-grid extrapolation". | `P15Elementary.capacityWorstCase` | | `HStarExceedsOne` | def_prop | `p15-full-price` | e^2-(3e-2)=(e-1)(e-2)>0, | the statements (statement only). | `P15Elementary.hStarExceedsOne` | -| `LocalPriceBoundFull` | def_prop | `p15-full-price` | price({X_i}) <= rho_star [-log mu_p(D_i)], (F12) | the bound (statement only); `price <= q_i` ("The inequality price<=q_i is NOT required and is in general stronger than what is proved here"). | — | +| `LocalPriceBoundFull` | def_prop | `p15-full-price` | price({X_i}) <= rho_star [-log mu_p(D_i)], (F12) | the bound (statement only); `price <= q_i` ("The inequality price<=q_i is NOT required and is in general stronger than what is proved here"). | `P15Interpolation.localPriceBoundFull` | | `GlobalAssemblyHazard` | def_prop | `p15-full-price` | sum_i [-log mu_p(D_i)] <= -log mu_p(D). (F13) | the inequalities (statement only; "without independence of crossing failures"). | `P15Hazard.globalAssemblyHazard` | | `SharpnessOfRhoStar` | def_prop | `p15-full-price` | Replacing rho_star by any smaller constant in (F2) would make its right side strictly less than one. | the statements (statement only; the finite parts are decidable in principle); a necessity claim for multi-block families with some demand one (the source: "other constraints may change its budget"). | `P15Elementary.sharpnessOfRhoStar` | | `DemandOneBoundary` | def_prop | `p15-full-price` | mu_p(D)=1-p_star^(a+1)>1-p_star=exp(-1), | the statements (statement only); any retraction of original P15-B ("whose local-budget premise is missing in that case"). | `P15Elementary.demandOneBoundary` | @@ -238,7 +238,7 @@ a theorem between string literals, an indented Prop definition, a proof written ## Claims and what is not established -171 claim rows: 10 `landing_claim`, 33 `graph_node`, 2 `open_obligation`, 95 `proof_index_result`, 7 `existing_lean_package`, 12 `main_experiment_proof`, 12 `exact_certificate`. Claim-level formal progress: 33 `specified` (a `def … : Prop` stating the claim itself is registered), 138 `none`; no research claim is `proved` or `kernel-checked`. 197 statement entries point at the 150 declarations of this package (all `specified`). 132 statement entries carry the label `proved` and are theorems of other packages, listed as the arithmetic skeleton or the Prop-level proof of the claim they sit under and never as the claim: 31 are the 31 Side24 arithmetic targets of main's `formal/` at origin/main `f6deeba7`; 41 are the 28 P15 arithmetic targets of main's `formal/` at `91cffbb5` (main PR #358, not yet on main; kernel evidence the hosted workspace-landing run 38096827443), each listed on every P15 row whose layer 0 source it anchors to; 60 are theorems of the proof packet `specifications/lean_statement_proofs_20261011` whose type is exactly a registered Prop of this package (52 theorems, 51 distinct Props, each listed on every row that registers its Prop; the hosted `lean-specification-proofs.yml` run 38121713840 receipted all of them as kernel-checked and run 38116277597 the first 38; a pull_request run checks out the synthetic merge of the PR head into the base, which the receipt records as checked_commit: run 38121713840 PR head 910809d6, actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; run 38116277597 PR head 00d2ac6e, actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with the same base; run 38122386459 corroborates on PR head d9b8dd33, actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6; same trees as the heads). Exactly one Prop registered as stating a claim itself has such a theorem: `DemandOneRefutation` on rows `p15-price-boundary` and `math.p15-price-boundary`; their claim-level label stays `specified` (the register admits only none/specified at claim level, alignment of the Prop with the source paragraph is PENDING_INDEPENDENT_REVIEW, and a receipt is about the Prop only), as the rows' `not established` cells record. `disposition` is the verbatim LANDING_CLAIMS value or `—` (null). Nothing in these tables is a scientific status, a review verdict or an acceptance; alignment of every statement is `PENDING_INDEPENDENT_REVIEW`. +171 claim rows: 10 `landing_claim`, 33 `graph_node`, 2 `open_obligation`, 95 `proof_index_result`, 7 `existing_lean_package`, 12 `main_experiment_proof`, 12 `exact_certificate`. Claim-level formal progress: 33 `specified` (a `def … : Prop` stating the claim itself is registered), 138 `none`; no research claim is `proved` or `kernel-checked`. 197 statement entries point at the 150 declarations of this package (all `specified`). 142 statement entries carry the label `proved` and are theorems of other packages, listed as the arithmetic skeleton or the Prop-level proof of the claim they sit under and never as the claim: 31 are the 31 Side24 arithmetic targets of main's `formal/` at origin/main `f6deeba7`; 41 are the 28 P15 arithmetic targets of main's `formal/` at `91cffbb5` (main PR #358, not yet on main; kernel evidence the hosted workspace-landing run 38096827443), each listed on every P15 row whose layer 0 source it anchors to; 70 are theorems of the proof packet `specifications/lean_statement_proofs_20261011` whose type is exactly a registered Prop of this package (60 theorems, 59 distinct Props, each listed on every row that registers its Prop; the hosted `lean-specification-proofs.yml` run 38121713840 receipted the 52 theorems of PR head 910809d6 as kernel-checked and run 38116277597 the first 38; a pull_request run checks out the synthetic merge of the PR head into the base, which the receipt records as checked_commit: run 38121713840 PR head 910809d6, actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; run 38116277597 PR head 00d2ac6e, actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with the same base; run 38122386459 corroborates on PR head d9b8dd33, actual tested merge 866136cca66b46e6dbd3186b47c9340f7e93b4f6; same trees as the heads; the 8 theorems of `P15Interpolation`, added after PR head 79731b96 (run 38124262242, actual tested merge 318ff194eecc42c39a6b27c1d7bf03f30d6a34d9 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2, receipt theorem_count 52), are kernel-checked by the hosted run 38149888699 on PR head 0dcb0016 (actual tested merge 4363b6928c62da242952631c6b0357d096c3b252 with base 79731b961fac555f33be3cd90e379b246a5a80e3, the head of PR #422; receipt theorem_count 60, leanchecker PASS) and were first receipted by run 38149524759 on PR head 88c21058 (actual tested merge 3306233bbdeadb15d9b4b07b94cc52a80ed8caeb with the same base); same trees as the heads). Exactly one Prop registered as stating a claim itself has such a theorem: `DemandOneRefutation` on rows `p15-price-boundary` and `math.p15-price-boundary`; their claim-level label stays `specified` (the register admits only none/specified at claim level, alignment of the Prop with the source paragraph is PENDING_INDEPENDENT_REVIEW, and a receipt is about the Prop only), as the rows' `not established` cells record. `disposition` is the verbatim LANDING_CLAIMS value or `—` (null). Nothing in these tables is a scientific status, a review verdict or an acceptance; alignment of every statement is `PENDING_INDEPENDENT_REVIEW`. | claim_id | kind | disposition | formal_progress | statements | not established | next step | |---|---|---|---|---|---|---| @@ -250,7 +250,7 @@ a theorem between string literals, an indented Prop definition, a proof written | `p15-realized-covers` | landing_claim | HOLD_WITH_DOMAIN | `specified` | 27 specified: `RealizedData`, `IsRealizedFamily`, `IsGood`, `IsKDecomposable`, `IsGeneratorCover`, `IsPaletteFeasible`, `PaletteNumberAttained`, `IsMinimalForbidden`, `IsTransversal`, `MinimalForbiddenCharacterisation`, `LocalRestriction`, `LocalDecomposability`, `LocalObstructionIsFullBlock`, `LocalPriceChain`, `IndependentBlockHazard`, `FullBlockCoverIff`, `CoverCostHazardBound`, `WholeGroundChromaticNumber`, `ElementaryPaletteFormula`, `TriangleNeedsThree`, `Benchmark816IsRealized`, `Benchmark816Palette`, `Benchmark816Cover`, `Benchmark816WholeGround`, `Benchmark816MinimalForbiddenCounts`, `Benchmark816Price`, `Benchmark816UnionBound`; 12 proved (main 91cffbb5, PR #358, not on main): `benchmark_block_and_ground_sizes`, `four_block_supports_fifteen`, `minimal_forbidder_counts`, `palette_816_from_two_label_classes`, `palette_815_fails_by_counting`, `whole_ground_chromatic_818`, `elementary_palette_formula_instances`, `macro_triangle_three_colors`, `ceil_block_over_capacity_instances`, `block_occupancy_one_percent`, `low_failure_union_bound_arithmetic`, `cover_price_numerator_and_denominator_positive`; 20 proved (proof packet): `P15Elementary.triangleNeedsThree`, `P15Structure.benchmark816IsRealized`, `P15Structure.benchmark816Price`, `P15Structure.elementaryPaletteFormula`, `P15Structure.triangleNeedsThree`, `P15Structure.benchmark816Palette`, `P15Structure.localDecomposability`, `P15Structure.localObstructionIsFullBlock`, `P15Structure.fullBlockCoverIff`, `P15Structure.wholeGroundChromaticNumber`, `P15Structure.benchmark816WholeGround`, `P15Structure.minimalForbiddenCharacterisation`, `P15Structure.benchmark816MinimalForbiddenCounts`, `P15Hazard.localPriceChain`, `P15Hazard.independentBlockHazard`, `P15Covers.benchmark816Cover`, `P15Covers.localRestriction`, `P15Covers.paletteNumberAttained`, `P15Covers.benchmark816UnionBound`, `P15Budget.coverCostHazardBound` | Props of this row with a theorem of exactly their type in the proof packet specifications/lean_statement_proofs_20261011: PaletteNumberAttained, MinimalForbiddenCharacterisation, LocalRestriction, LocalDecomposability, LocalObstructionIsFullBlock, LocalPriceChain, IndependentBlockHazard, FullBlockCoverIff, CoverCostHazardBound, WholeGroundChromaticNumber, ElementaryPaletteFormula, TriangleNeedsThree, Benchmark816IsRealized, Benchmark816Palette, Benchmark816Cover, Benchmark816WholeGround, Benchmark816MinimalForbiddenCounts, Benchmark816Price, Benchmark816UnionBound (20 entries below, label `proved`; 13 of them (P15Structure.minimalForbiddenCharacterisation, P15Structure.localDecomposability, P15Structure.localObstructionIsFullBlock, P15Structure.fullBlockCoverIff, P15Structure.wholeGroundChromaticNumber, P15Structure.elementaryPaletteFormula, P15Elementary.triangleNeedsThree, P15Structure.triangleNeedsThree, P15Structure.benchmark816IsRealized, P15Structure.benchmark816Palette, P15Structure.benchmark816WholeGround, P15Structure.benchmark816MinimalForbiddenCounts, P15Structure.benchmark816Price) kernel-checked by the hosted run 38116277597 (PR head 00d2ac6e; actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2); 7 of them (P15Covers.paletteNumberAttained, P15Covers.localRestriction, P15Hazard.localPriceChain, P15Hazard.independentBlockHazard, P15Budget.coverCostHazardBound, P15Covers.benchmark816Cover, P15Covers.benchmark816UnionBound) added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN)); among them Proposition P1 (MinimalForbiddenCharacterisation), both halves of Theorem P2 (FullBlockCoverIff, display (P7), and CoverCostHazardBound, display (P8)), the local statements (P2)-(P5) and the benchmark Props including the union bound (P11). Theorem-shaped Props of this row still `specified` with no theorem: none; the parametrised predicates IsRealizedFamily, IsGood, IsKDecomposable, IsGeneratorCover, IsPaletteFeasible, IsMinimalForbidden, IsTransversal are the vocabulary of the other Props, not closed statements (a theorem of their type would assert them for every argument, which is false), and are not targets. Theorem P2 is proved as the two Props state it (for the formal RealizedData record and the formal downset, prices 0 <= c_v <= p_v), which is a statement about those Props, not acceptance of the informal theorem: the claim-level label stays `specified` (this register admits only none/specified at claim level), alignment of RealizedData / IsRealizedFamily / downset / coverCost / mu with the informal objects is PENDING_INDEPENDENT_REVIEW, and the price range p_v < c_v <= phi(p_v) is a different claim row. The 12 main P15 arithmetic theorems listed as `proved` (finite arithmetic of Section 6: 409, 2454, 15, 500616, 419743994415, 816, 815*3 < 2448, 818, 409p = 1/100, the (P11) rational bound, positivity of 6/40900^409, the elementary instances of (P9)) are at commit 91cffbb5 of main PR #358, not on main; they do not count the minimal forbidders, show the palette is 816 or evaluate 6/40900^409, and the proof-packet theorems that do (Benchmark816MinimalForbiddenCounts, Benchmark816Palette, Benchmark816Price) do so for the formal RealizedData record, whose identification with the informal six-block construction is an alignment question. Nothing is asserted for prices p_v < c_v <= phi(p_v) (row p15-price-budget-restricted), for arbitrary P15 inputs or for the prize (original_prize_closed stays false). Disposition HOLD_WITH_DOMAIN is transcribed, not re-derived. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0. | Proof lane: every theorem-shaped Prop of this row has a theorem (the parametrised predicates IsRealizedFamily, IsGood, IsKDecomposable, IsGeneratorCover, IsPaletteFeasible, IsMinimalForbidden, IsTransversal are vocabulary, not targets); every theorem of this row has a hosted receipt (run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2)). Independent reviewer: alignment of MinimalForbiddenCharacterisation with Proposition P1 (completeness clause), of FullBlockCoverIff with (P7), of CoverCostHazardBound with (P8) (the sInf cover cost, the cappedHazard endpoint convention) and of the Benchmark816 data record with the Section 6 construction. main: PR #358 merge (operator) so the 12 arithmetic theorems are on main. | | `p15-price-boundary` | landing_claim | EXACT_COUNTEREXAMPLE | `specified` | 3 specified: `TwoCoordGeneratorPrices`, `DemandOneRefutation`, `LogOnePlusBelowIdentity`; 6 proved (main 91cffbb5, PR #358, not on main): `smallest_member_block_size`, `demand_one_good_sets`, `demand_one_obstruction`, `good_measure_three_quarters`, `generator_prices_ninths`, `minimum_generator_price_exceeds_third`; 3 proved (proof packet): `P15Elementary.twoCoordGeneratorPrices`, `P15Elementary.logOnePlusBelowIdentity`, `P15Elementary.demandOneRefutation` | DemandOneRefutation states the refutation (the two-coordinate data form a realized family with K_H(d) = 1, obstruction {X}, admissible prices 2/3, mu_p(D) = 3/4, cover cost 4/9 > 1/3 > log(4/3)). DemandOneRefutation, TwoCoordGeneratorPrices and LogOnePlusBelowIdentity each have a theorem of exactly their type in the proof packet specifications/lean_statement_proofs_20261011 (listed below as `proved`, the label of a committed proof package; the hosted lean-specification-proofs.yml run 38116277597 (PR head 00d2ac6e; actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) kernel-checked them (receipt formalization_status kernel-checked, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound})); the two logarithm inequalities phi(1/2) = log 2 > 2/3 and log(4/3) < 1/3 are conjuncts of DemandOneRefutation and are proved inside its theorem from Mathlib's Real.log bounds. The claim-level label stays `specified`, not `proved`: this register admits only none/specified at claim level (no research claim of this programme is proved), whether DemandOneRefutation says what the source paragraph says is the independent reviewer's alignment question (PENDING_INDEPENDENT_REVIEW), the hosted run 38116277597 (PR head 00d2ac6e; actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) kernel-checked the Prop and nothing more, and a kernel-checked Prop is evidence about that Prop only. This is the one row of the register where a theorem proves the Prop registered as stating the claim itself; it is recorded here for the operator and not acted on. The 6 main P15 arithmetic theorems listed as `proved` (good sets, obstruction, 3/4 over denominator 4, prices 9,6,6,4 over 9, 3*4 > 9) are at commit 91cffbb5 of main PR #358, not on main; they are finite arithmetic, not the refutation. The counterexample does not refute d_i >= 2 successors or original P15-B (the disposition reason; the theorem's docstring says the same). Disposition EXACT_COUNTEREXAMPLE is transcribed, not re-derived. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0. | The hosted lean-specification-proofs.yml run 38116277597 (PR head 00d2ac6e; actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) produced the first receipt (`kernel-checked` appears only there); later commits need their own run. Independent (non-Anthropic) reviewer: alignment of DemandOneRefutation with the source paragraph (same two-coordinate family, prices, cover cost and the "does not contradict original P15-B" scope); any claim-level label beyond none/specified is a register-schema decision for the operator after that review, which no receipt produces. main: PR #358 merge (operator) so the 6 arithmetic theorems are on main. | | `p15-price-budget-restricted` | landing_claim | HOLD_WITH_DOMAIN | `specified` | 8 specified: `LogRatioBound`, `RatioExponentBound`, `RestrictedLocalBudget`, `RestrictedTransformedPriceBudget`, `RhoTestSufficient`, `CapTestAtTwoThirds`, `Benchmark816TransformedRange`, `Benchmark816RationalPrice`; 3 proved (main 91cffbb5, PR #358, not on main): `t3_ratio_at_minimal_block`, `t3_bound_finite_instances`, `explicit_rational_price_above_p`; 8 proved (proof packet): `P15Elementary.logRatioBound`, `P15Elementary.capTestAtTwoThirds`, `P15Elementary.ratioExponentBound`, `P15Structure.benchmark816RationalPrice`, `P15Budget.restrictedLocalBudget`, `P15Budget.rhoTestSufficient`, `P15Budget.restrictedTransformedPriceBudget`, `P15Budget.benchmark816TransformedRange` | RestrictedTransformedPriceBudget states (T1) for every realized family with a_i >= 1, d_i >= 2, p_v <= 1/4, c_v <= phi(p_v) and is proved as stated in the proof packet; that is evidence about the Prop (for the formal RealizedData record, downset, coverCost and mu), not acceptance of the informal theorem: the claim-level label stays `specified` (claim-level vocabulary none/specified; alignment PENDING_INDEPENDENT_REVIEW). Props of this row with a theorem of exactly their type in the proof packet specifications/lean_statement_proofs_20261011: LogRatioBound, RatioExponentBound, RestrictedLocalBudget, RestrictedTransformedPriceBudget, RhoTestSufficient, CapTestAtTwoThirds, Benchmark816TransformedRange, Benchmark816RationalPrice (8 entries below, label `proved`; 4 of them (P15Elementary.logRatioBound, P15Elementary.ratioExponentBound, P15Elementary.capTestAtTwoThirds, P15Structure.benchmark816RationalPrice) kernel-checked by the hosted run 38116277597 (PR head 00d2ac6e; actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2); 4 of them (P15Budget.restrictedLocalBudget, P15Budget.restrictedTransformedPriceBudget, P15Budget.rhoTestSufficient, P15Budget.benchmark816TransformedRange) added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN)). Theorem-shaped Props of this row still `specified` with no theorem: none. The intermediate ratio steps of (T3) are proved inside the theorems that use them; the integral representation behind (T2), the admissibility integral and the Section 5 checker program are not specified. The 3 main P15 arithmetic theorems listed as `proved` (the a = 1, n = 3 instance 16/27, finite instances of the (T3) bound and the rational identity 81801/3345620000) are at commit 91cffbb5 of main PR #358, not on main; they are not (T1). The dependency on claim p15-realized-covers is discharged only to the extent that row records. Disposition HOLD_WITH_DOMAIN ("independent theorem review not yet source-bound in manifest") is transcribed, not re-derived. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0. | Math- Mathlib lane: every theorem-shaped Prop of this row has a theorem; every theorem of this row has a hosted receipt (run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2)). Independent reviewer: alignment of RestrictedTransformedPriceBudget with (T1) including the per-coordinate price hypothesis, the K >= K_H(d) palette and the cappedHazard endpoint convention. main: PR #358 merge (operator) so the 3 arithmetic theorems are on main. | -| `p15-full-price` | landing_claim | REVIEWED_SCOPED | `specified` | 20 specified: `FullTransformedPriceBudget`, `RhoStarEnclosure`, `RhoStarBelowSixSevenths`, `IsProperDownset`, `HazardStarPositive`, `CoordinatewiseConcavity`, `HazardProductBound`, `HazardPhiBound`, `FullGroundPriceBound`, `PhiAtPStar`, `FullGroundBudgetIff`, `CapacityHazardIsBinomial`, `OddMajorityIdentity`, `CapacityWorstCase`, `HStarExceedsOne`, `LocalPriceBoundFull`, `GlobalAssemblyHazard`, `SharpnessOfRhoStar`, `DemandOneBoundary`, `SixSeventhsCertificate`; 7 proved (main 91cffbb5, PR #358, not on main): `rho_star_endpoints_adjacent`, `rho_star_upper_endpoint_below_six_sevenths`, `sixteen_twentysevenths_below_six_sevenths`, `minimal_block_size_instances`, `e_rational_bounds_ordering`, `exp_eleven_sixths_taylor_certificate`, `h_star_rational_certificate_constants`; 11 proved (proof packet): `P15Elementary.rhoStarBelowSixSevenths`, `P15Elementary.sixSeventhsCertificate`, `P15Elementary.hStarExceedsOne`, `P15Elementary.phiAtPStar`, `P15Elementary.hazardStarPositive`, `P15Elementary.oddMajorityIdentity`, `P15Elementary.capacityWorstCase`, `P15Elementary.demandOneBoundary`, `P15Elementary.capacityHazardIsBinomial`, `P15Elementary.sharpnessOfRhoStar`, `P15Hazard.globalAssemblyHazard` | FullTransformedPriceBudget states (F2), not proved; RhoStarEnclosure states (F3), not proved; SharpnessOfRhoStar states the attainment clause and is proved as stated. The claim-level label stays `specified` (claim-level vocabulary none/specified; a theorem of a Prop is evidence about that Prop, for the formal objects, not acceptance of Theorem F; alignment PENDING_INDEPENDENT_REVIEW). Props of this row with a theorem of exactly their type in the proof packet specifications/lean_statement_proofs_20261011: RhoStarBelowSixSevenths, HazardStarPositive, PhiAtPStar, CapacityHazardIsBinomial, OddMajorityIdentity, CapacityWorstCase, HStarExceedsOne, GlobalAssemblyHazard, SharpnessOfRhoStar, DemandOneBoundary, SixSeventhsCertificate (11 entries below, label `proved`; 8 of them (P15Elementary.rhoStarBelowSixSevenths, P15Elementary.hazardStarPositive, P15Elementary.phiAtPStar, P15Elementary.oddMajorityIdentity, P15Elementary.capacityWorstCase, P15Elementary.hStarExceedsOne, P15Elementary.demandOneBoundary, P15Elementary.sixSeventhsCertificate) kernel-checked by the hosted run 38116277597 (PR head 00d2ac6e; actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2); 3 of them (P15Elementary.capacityHazardIsBinomial, P15Hazard.globalAssemblyHazard, P15Elementary.sharpnessOfRhoStar) added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN)). Theorem-shaped Props of this row still `specified` with no theorem: FullTransformedPriceBudget, RhoStarEnclosure, CoordinatewiseConcavity, HazardProductBound, HazardPhiBound, FullGroundPriceBound, FullGroundBudgetIff, LocalPriceBoundFull; the parametrised predicates IsProperDownset are the vocabulary of the other Props, not closed statements (a theorem of their type would assert them for every argument, which is false), and are not targets. The derivative formulas (F4)-(F5) are not specified. SixSeventhsCertificate uses Mathlib's decimal bound on e in place of the source's series argument. The 7 main P15 arithmetic theorems listed as `proved` (finite arithmetic of the Section 6 certificate chain: adjacent 20-digit endpoints as Nat, 16/27 < 6/7, n >= 2a+1 instances, the rational orderings and the degree-5 Taylor partial sum) are at commit 91cffbb5 of main PR #358, not on main; they do not place rho_star = 1/(3 - log(3e - 2)) between the endpoints (nothing does: RhoStarEnclosure is specified only), do not prove e < 87/32 or 197/32 < exp(11/6) as real-number facts (the SixSeventhsCertificate theorem does, as that Prop states them), and are not Theorem F. The full_price.py Fraction procedure is not a kernel proof and is not specified. No arbitrary-downset or unrestricted P15 prize statement (original_prize_closed stays false). Disposition REVIEWED_SCOPED is transcribed, not re-derived. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0. | Math- Mathlib lane: FullTransformedPriceBudget, RhoStarEnclosure, CoordinatewiseConcavity, HazardProductBound, HazardPhiBound, FullGroundPriceBound, FullGroundBudgetIff, LocalPriceBoundFull remain the targets of this row (RhoStarEnclosure ((F3), 20 digits) needs proof-producing exp/log enclosures; (F6)-(F8), (F12) and (F2) need the coordinatewise concavity (F4)-(F5), which is not specified); every theorem of this row has a hosted receipt (run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2)). Independent reviewer: alignment of FullTransformedPriceBudget with (F2), in particular the quantification over ALL p in [0,1]^X and the SAME palette K >= K_H(d). main: PR #358 merge (operator) so the 7 arithmetic theorems are on main. | +| `p15-full-price` | landing_claim | REVIEWED_SCOPED | `specified` | 20 specified: `FullTransformedPriceBudget`, `RhoStarEnclosure`, `RhoStarBelowSixSevenths`, `IsProperDownset`, `HazardStarPositive`, `CoordinatewiseConcavity`, `HazardProductBound`, `HazardPhiBound`, `FullGroundPriceBound`, `PhiAtPStar`, `FullGroundBudgetIff`, `CapacityHazardIsBinomial`, `OddMajorityIdentity`, `CapacityWorstCase`, `HStarExceedsOne`, `LocalPriceBoundFull`, `GlobalAssemblyHazard`, `SharpnessOfRhoStar`, `DemandOneBoundary`, `SixSeventhsCertificate`; 7 proved (main 91cffbb5, PR #358, not on main): `rho_star_endpoints_adjacent`, `rho_star_upper_endpoint_below_six_sevenths`, `sixteen_twentysevenths_below_six_sevenths`, `minimal_block_size_instances`, `e_rational_bounds_ordering`, `exp_eleven_sixths_taylor_certificate`, `h_star_rational_certificate_constants`; 19 proved (proof packet): `P15Elementary.rhoStarBelowSixSevenths`, `P15Elementary.sixSeventhsCertificate`, `P15Elementary.hStarExceedsOne`, `P15Elementary.phiAtPStar`, `P15Elementary.hazardStarPositive`, `P15Elementary.oddMajorityIdentity`, `P15Elementary.capacityWorstCase`, `P15Elementary.demandOneBoundary`, `P15Elementary.capacityHazardIsBinomial`, `P15Elementary.sharpnessOfRhoStar`, `P15Hazard.globalAssemblyHazard`, `P15Interpolation.rhoStarEnclosure`, `P15Interpolation.coordinatewiseConcavity`, `P15Interpolation.hazardProductBound`, `P15Interpolation.hazardPhiBound`, `P15Interpolation.fullGroundPriceBound`, `P15Interpolation.fullGroundBudgetIff`, `P15Interpolation.localPriceBoundFull`, `P15Interpolation.fullTransformedPriceBudget` | FullTransformedPriceBudget states (F2) and is proved as stated; RhoStarEnclosure states (F3) and is proved as stated; SharpnessOfRhoStar states the attainment clause and is proved as stated. The claim-level label stays `specified` (claim-level vocabulary none/specified; a theorem of a Prop is evidence about that Prop, for the formal objects, not acceptance of Theorem F; alignment PENDING_INDEPENDENT_REVIEW). Theorem F is proved as FullTransformedPriceBudget states it: for the formal RealizedData record with a_i >= 1, d_i >= 2, every p in [0,1]^X, every 0 <= c_v <= phi(p_v) and the same K >= K_H(d), coverCost <= cappedHazard rho_star mu, through the coordinatewise concavity (CoordinatewiseConcavity, a theorem of exactly that Prop), (F6)-(F8), (F12) and (F13); that is evidence about those Props, not acceptance of the informal theorem. RhoStarEnclosure is proved by a rational certificate (Real.exp_bound series enclosures for e and for exp with explicit remainders, compared by norm_num), not by the source's full_price.py Fraction procedure, which remains unspecified. Props of this row with a theorem of exactly their type in the proof packet specifications/lean_statement_proofs_20261011: FullTransformedPriceBudget, RhoStarEnclosure, RhoStarBelowSixSevenths, HazardStarPositive, CoordinatewiseConcavity, HazardProductBound, HazardPhiBound, FullGroundPriceBound, PhiAtPStar, FullGroundBudgetIff, CapacityHazardIsBinomial, OddMajorityIdentity, CapacityWorstCase, HStarExceedsOne, LocalPriceBoundFull, GlobalAssemblyHazard, SharpnessOfRhoStar, DemandOneBoundary, SixSeventhsCertificate (19 entries below, label `proved`; 8 of them (P15Elementary.rhoStarBelowSixSevenths, P15Elementary.hazardStarPositive, P15Elementary.phiAtPStar, P15Elementary.oddMajorityIdentity, P15Elementary.capacityWorstCase, P15Elementary.hStarExceedsOne, P15Elementary.demandOneBoundary, P15Elementary.sixSeventhsCertificate) are among the 38 theorems of PR head 00d2ac6e kernel-checked by the hosted run 38116277597 (actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2; job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound} for each, receipt formalization_status kernel-checked, worktree CLEAN; artifact lean-specification-proofs-38116277597-1); 3 of them (P15Elementary.capacityHazardIsBinomial, P15Hazard.globalAssemblyHazard, P15Elementary.sharpnessOfRhoStar) were added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN); 8 of them (P15Interpolation.fullTransformedPriceBudget, P15Interpolation.rhoStarEnclosure, P15Interpolation.coordinatewiseConcavity, P15Interpolation.hazardProductBound, P15Interpolation.hazardPhiBound, P15Interpolation.fullGroundPriceBound, P15Interpolation.fullGroundBudgetIff, P15Interpolation.localPriceBoundFull) were added after PR head 79731b96 and kernel-checked by the hosted run 38149888699 (PR head 0dcb0016; actual tested merge 4363b6928c62da242952631c6b0357d096c3b252 with base 79731b961fac555f33be3cd90e379b246a5a80e3) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, theorem_count 60, worktree CLEAN; artifact lean-specification-proofs-38149888699-1, sha256 cdeb5c73aa03124ed0db16fa14d25fb03a8fa842457fce1e0c6565dbc5ee7ca8); they were first receipted by run 38149524759 (PR head 88c21058; actual tested merge 3306233bbdeadb15d9b4b07b94cc52a80ed8caeb with base 79731b961fac555f33be3cd90e379b246a5a80e3) (same Lean bytes; artifact lean-specification-proofs-38149524759-1, sha256 ddefbdcc63223d05fd8ed34addbeebc199e271525d87dead01109cddc529e836); base 79731b961fac555f33be3cd90e379b246a5a80e3 is the head of PR #422, and each merge has the same tree as its head). Theorem-shaped Props of this row still `specified` with no theorem: none; the parametrised predicates IsProperDownset are the vocabulary of the other Props, not closed statements (a theorem of their type would assert them for every argument, which is false), and are not targets. The derivative formulas (F4)-(F5) are not specified; CoordinatewiseConcavity, their consequence, is proved from the one-coordinate split of mu_p(A) (display (F4): affine in exp(-t_i) with coefficients 0 <= S_in <= S_out for a downset) and the second-derivative criterion for s \|-> -log(a + b exp(-s)). SixSeventhsCertificate uses Mathlib's decimal bound on e in place of the source's series argument. The 7 main P15 arithmetic theorems listed as `proved` (finite arithmetic of the Section 6 certificate chain: adjacent 20-digit endpoints as Nat, 16/27 < 6/7, n >= 2a+1 instances, the rational orderings and the degree-5 Taylor partial sum) are at commit 91cffbb5 of main PR #358, not on main; they do not place rho_star = 1/(3 - log(3e - 2)) between the endpoints, do not prove e < 87/32 or 197/32 < exp(11/6) as real-number facts (the SixSeventhsCertificate theorem does, as that Prop states them), and are not Theorem F. The full_price.py Fraction procedure is not a kernel proof and is not specified. No arbitrary-downset or unrestricted P15 prize statement (original_prize_closed stays false). Disposition REVIEWED_SCOPED is transcribed, not re-derived. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0. | Math- Mathlib lane: every theorem-shaped Prop of this row has a theorem (the parametrised predicates IsProperDownset are vocabulary, not targets); every theorem of this row has a hosted receipt: the 8 added after PR head 79731b96 (P15Interpolation.rhoStarEnclosure, P15Interpolation.coordinatewiseConcavity, P15Interpolation.hazardProductBound, P15Interpolation.hazardPhiBound, P15Interpolation.fullGroundPriceBound, P15Interpolation.fullGroundBudgetIff, P15Interpolation.localPriceBoundFull, P15Interpolation.fullTransformedPriceBudget) by run 38149888699 (PR head 0dcb0016; actual tested merge 4363b6928c62da242952631c6b0357d096c3b252 with base 79731b961fac555f33be3cd90e379b246a5a80e3) and first by run 38149524759 (PR head 88c21058; actual tested merge 3306233bbdeadb15d9b4b07b94cc52a80ed8caeb with base 79731b961fac555f33be3cd90e379b246a5a80e3), the others by run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2). Independent reviewer: alignment of FullTransformedPriceBudget with (F2), in particular the quantification over ALL p in [0,1]^X and the SAME palette K >= K_H(d), and of the proved interpolation chain (CoordinatewiseConcavity through LocalPriceBoundFull) with Sections 2-3 of the source. main: PR #358 merge (operator) so the 7 arithmetic theorems are on main. | | `downstream-hard-gate` | landing_claim | ENGINEERING_HOLD | `none` | — | An engineering control, not a mathematical claim: there is no theorem to state in Lean and none is stated. The gate's terminal classifications and non-discharge tokens are transcribed in the graph_node rows of this register only as source identity. Disposition ENGINEERING_HOLD ("repository-wide external controlling-source binding remains unresolved") is transcribed, not re-derived. | No Lean target. The control's semantics live in Math- frontiers/downstream_gate_20260925 and its workflow; the register only records that every GRAPH math.* node has a row here. | | `math.uniform-matrix-cap-lifetime` | graph_node | — | `specified` | 32 specified: `IsLPeriodic`, `IsSmooth`, `GaussianFieldInterface`, `IsCriticalPoint`, `HessianHasInertia`, `IsNondegMax`, `IsIndexSaddle`, `IsCandidatePair`, `IsMorseDistinct`, `SuperlevelBarInterface`, `IsFiniteBar`, `IsLifetimeDensityVersion`, `IsLPeriodic`, `IsSmooth`, `GaussianFieldInterface`, `IsCriticalPoint`, `HessianHasInertia`, `IsNondegMax`, `IsIndexSaddle`, `IsCandidatePair`, `IsMorseDistinct`, `SuperlevelBarInterface`, `IsFiniteBar`, `IsLifetimeDensityVersion`, `IsWindowPair`, `IsWindowElderPair`, `IsUnrestrictedPair`, `PairLawInterface`, `ParentUniformSelectionA`, `ParentCompactWindowDensityB`, `IsUnrestrictedLeadingCoefficient`, `ParentUnrestrictedLeadingDensityC` | ParentUniformSelectionA, ParentCompactWindowDensityB and ParentUnrestrictedLeadingDensityC state the shapes of (1.1), (1.2), (1.3) for every object satisfying the interfaces; nothing is proved. The identification of the interface structures (GaussianFieldInterface, SuperlevelBarInterface, PairLawInterface) with the source's field, elder rule and weighted regression law is not established: the Props hold for every object satisfying the interface, and no inhabitant is constructed. The reading rule that the GRAPH binds to this node (congruence erratum E1, Section 9 replacement v1.1, marked-cylinder cap sections 1-5, reconciliation record with W1 and the embedding radius r < L/(4 sqrt 2)) is NOT transcribed into any hypothesis; the Props are stated from the parent bytes alone. Not stated: the regression law Q_{r,b,k,R}, the typed weight W_r, the full normalizer Z_r and Q^W (p_r is a primitive interface field), the marked Kac-Rice representation (Sections 9-10, radial ledger (10.2)), the Gaussian/angular representation (15.2) of c_{d,L} and (11.3) of c_{B,K}, (12.1)-(12.3), (14.1), (5.5), Sections 2-8. No numerical r_*, C, z_*, c_{B,K}, c_{d,L}; no lower bound for d >= 3. The GRAPH classification PROVED_REVIEWED and the review disposition ACCEPT_AT_EXISTENTIAL_SCOPE are source identity, not re-derived; the five validity premises of the hardening-branch claim graph are not touched. Nonauthor review and acceptance are not claimed by any statement; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet is 0. The interface does not determine p or the field: the parent-shape Props are predicates on the interface objects, not closed statements; the universal closure of ParentUniformSelectionA over all inhabitants is false whenever the interfaces are inhabited (take p identically 0), and `specified` refers to the statement shape at the source's object, which is not constructed. | Pin ERRATUM_CONGRUENCE.md, REPAIR.md (Section 9 v1.1) and the reconciliation record, and add the reading rule as explicit hypotheses or separate Props; state (15.2) as a Prop over an explicit Gaussian conditional law; independent reviewer: alignment of the three parent Props against (1.1)-(1.3) with the honesty checklist (quantifier order, existential constants outside the universal quantifiers, "versions", compact marks, all frames). | | `math.d1-component.congruence-erratum` | graph_node | — | `none` | — | No Lean statement: the erratum's source bytes are not pinned in this packet and no Prop states the corrected congruence D_r H_i D_r or det(D_r H_i D_r) = det(H_i)/r. The parent Props of this register do not transcribe section 5 at all, so the amendment has nothing to attach to yet. | Pin ERRATUM_CONGRUENCE.md (blob 213594d6, 1782 B); state the corrected congruence as a matrix identity over Matrix (Fin d) (Fin d) R (a candidate kernel-proof target: block-matrix algebra). | @@ -267,7 +267,7 @@ a theorem between string literals, an indented Prop definition, a proof written | `math.rn-region.intermediate-r-to-rho` | graph_node | — | `specified` | 1 specified: `D5eIntermediateShellsI3I4` | D5eIntermediateShellsI3I4 states the window-only bound E N <= C r^3 (A_0^(-2) + rho^2) on {A_0 r <= \|X\| <= rho} with side conditions taken from dimension-lift (1.6); not proved. The I3/I4 source (frontiers/intermediate_window_20260928) is not pinned here; no all-height intermediate count exists or is claimed; no numerical constants. Nonauthor review and acceptance are not claimed by any statement; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet is 0. | Pin intermediate_window_20260928/PROOF.md and anchor the single-shell display there; independent reviewer: alignment of D5eIntermediateShellsI3I4 with row D5-e and with dimension-lift (1.6). | | `math.rn-region.witness-collision` | open_obligation | — | `specified` | 2 specified: `WitnessCollisionNearPinPairsTarget`, `RemoteCollisionSecondFactorialD` | WitnessCollisionNearPinPairsTarget states the OPEN obligation as a target Prop, not as a result: nothing asserts that the target holds, is attainable, or follows from any reviewed source. RemoteCollisionSecondFactorialD states only the fixed-remote, fixed-eta part (Corollary D of remote_collision), which the GRAPH records as reviewed evidence and NOT as a proof of this node. The Palm route's Theorem Q (q = 2) would imply the target but is an author-side candidate stated separately (PalmRouteFactorialMomentsQ) and not consumed here; the c6_witness_collision reconciliation's proposed discharge is declarative with execution pending. The node stays OPEN_ACTIVE; this register cannot and does not change that. Nonauthor review and acceptance are not claimed by any statement; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet is 0. | None for Lean beyond the target statement: the obligation needs a source-bound proof and nonauthor review in Math-; if Theorem Q is folded, re-anchor the target to the fold record. | | `math.rn-mesoscopic-reduction` | graph_node | — | `none` | — | No Lean statement: the PR7 route's bytes (frontiers/rn_mesoscopic_20260925/PROOF.md) are not pinned here and its Lemma A (positive-definite covariance of the rows of (U_0, J_0(y)) on K_AB) is not stated. The supersession is a graph classification, not mathematics. | Pin rn_mesoscopic_20260925/PROOF.md and state Lemma A (Matrix.PosDef lower bound on a compact annulus) if the route is ever revived; otherwise none. | -| `math.p15-full-price` | graph_node | — | `specified` | 3 specified: `FullTransformedPriceBudget`, `RhoStarEnclosure`, `SharpnessOfRhoStar`; 7 proved (main 91cffbb5, PR #358, not on main): `rho_star_endpoints_adjacent`, `rho_star_upper_endpoint_below_six_sevenths`, `sixteen_twentysevenths_below_six_sevenths`, `minimal_block_size_instances`, `e_rational_bounds_ordering`, `exp_eleven_sixths_taylor_certificate`, `h_star_rational_certificate_constants`; 1 proved (proof packet): `P15Elementary.sharpnessOfRhoStar` | See row p15-full-price. Of the three Props of this node, with a theorem of exactly their type in the proof packet: SharpnessOfRhoStar (1 entries below, label `proved`; 1 of them (P15Elementary.sharpnessOfRhoStar) added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN)); stated, not proved: FullTransformedPriceBudget, RhoStarEnclosure. A theorem of SharpnessOfRhoStar is about the formal triple block and the formal cover cost; none of this is Theorem F, and the node-level label stays `specified`. The 7 main P15 arithmetic theorems of source p15-full-price (at commit 91cffbb5 of main PR #358, not on main) are listed here as the arithmetic skeleton, never as the node. The price-boundary refutation is a scope boundary (GRAPH edge boundary_counterexample_not_required_premise), not a hypothesis. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0. | As for row p15-full-price. | +| `math.p15-full-price` | graph_node | — | `specified` | 3 specified: `FullTransformedPriceBudget`, `RhoStarEnclosure`, `SharpnessOfRhoStar`; 7 proved (main 91cffbb5, PR #358, not on main): `rho_star_endpoints_adjacent`, `rho_star_upper_endpoint_below_six_sevenths`, `sixteen_twentysevenths_below_six_sevenths`, `minimal_block_size_instances`, `e_rational_bounds_ordering`, `exp_eleven_sixths_taylor_certificate`, `h_star_rational_certificate_constants`; 3 proved (proof packet): `P15Elementary.sharpnessOfRhoStar`, `P15Interpolation.rhoStarEnclosure`, `P15Interpolation.fullTransformedPriceBudget` | See row p15-full-price. Of the three Props of this node, with a theorem of exactly their type in the proof packet: FullTransformedPriceBudget, RhoStarEnclosure, SharpnessOfRhoStar (3 entries below, label `proved`; 1 of them (P15Elementary.sharpnessOfRhoStar) were added after commit 00d2ac6e and kernel-checked by the hosted run 38121713840 (PR head 910809d6; actual tested merge 5b198699308e0585904c21d12bf540cf2475d2f0 with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, worktree CLEAN); 2 of them (P15Interpolation.fullTransformedPriceBudget, P15Interpolation.rhoStarEnclosure) were added after PR head 79731b96 and kernel-checked by the hosted run 38149888699 (PR head 0dcb0016; actual tested merge 4363b6928c62da242952631c6b0357d096c3b252 with base 79731b961fac555f33be3cd90e379b246a5a80e3) (job proof-evidence: fresh build, leanchecker PASS, `#print axioms` within {propext, Classical.choice, Quot.sound}, receipt formalization_status kernel-checked, theorem_count 60, worktree CLEAN; artifact lean-specification-proofs-38149888699-1, sha256 cdeb5c73aa03124ed0db16fa14d25fb03a8fa842457fce1e0c6565dbc5ee7ca8); they were first receipted by run 38149524759 (PR head 88c21058; actual tested merge 3306233bbdeadb15d9b4b07b94cc52a80ed8caeb with base 79731b961fac555f33be3cd90e379b246a5a80e3) (same Lean bytes; artifact lean-specification-proofs-38149524759-1, sha256 ddefbdcc63223d05fd8ed34addbeebc199e271525d87dead01109cddc529e836); base 79731b961fac555f33be3cd90e379b246a5a80e3 is the head of PR #422, and each merge has the same tree as its head); none of the three is left unproved. A theorem of SharpnessOfRhoStar is about the formal triple block and the formal cover cost; a theorem of FullTransformedPriceBudget is about the formal RealizedData record, downset, coverCost and mu; none of this is Theorem F, and the node-level label stays `specified`. The 7 main P15 arithmetic theorems of source p15-full-price (at commit 91cffbb5 of main PR #358, not on main) are listed here as the arithmetic skeleton, never as the node. The price-boundary refutation is a scope boundary (GRAPH edge boundary_counterexample_not_required_premise), not a hypothesis. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0. | As for row p15-full-price. | | `math.p15-price-boundary` | graph_node | — | `specified` | 2 specified: `TwoCoordGeneratorPrices`, `DemandOneRefutation`; 6 proved (main 91cffbb5, PR #358, not on main): `smallest_member_block_size`, `demand_one_good_sets`, `demand_one_obstruction`, `good_measure_three_quarters`, `generator_prices_ninths`, `minimum_generator_price_exceeds_third`; 2 proved (proof packet): `P15Elementary.twoCoordGeneratorPrices`, `P15Elementary.demandOneRefutation` | See row p15-price-boundary: TwoCoordGeneratorPrices and DemandOneRefutation (the two Props of this node) have theorems of exactly their type in the proof packet (listed as `proved`; kernel-checked by the hosted run 38116277597 (PR head 00d2ac6e; actual tested merge c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c with base b2d70d77876a10c365f5db5d3b6cafcf180af4e2)), the two logarithm inequalities included; the claim-level label stays `specified` for the reasons given there (claim-level vocabulary none/specified, alignment PENDING_INDEPENDENT_REVIEW, a Prop-level proof is evidence about the Prop only, whatever the hosted run 38116277597 receipted). The 6 main P15 arithmetic theorems of source p15-price-boundary (at commit 91cffbb5 of main PR #358, not on main) are listed as the arithmetic skeleton, never as the node. REFUTED is the graph classification of the extension, transcribed as source identity. Nonauthor review and acceptance are not claimed by any statement or theorem; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet and of the proof packet is 0. | As for row p15-price-boundary. | | `math.rn-selector-region-crosswalk` | graph_node | — | `none` | — | An engineering inventory, not a mathematical claim; nothing to state in Lean and nothing stated. | No Lean target. | | `math.rn-fixed-annulus-window` | graph_node | — | `specified` | 1 specified: `FixedAnnulusWindowCandidateA2` | See row rn-fixed-annulus-window: (A2) stated, not proved; no global D5/RN/JETMOD, k -> 0, d >= 3, pin-neighbourhood, intermediate-scale, collision or elder-selection closure. Nonauthor review and acceptance are not claimed by any statement; alignment of every statement with its anchor is PENDING_INDEPENDENT_REVIEW; organizational-independence credit of this packet is 0. | As for row rn-fixed-annulus-window. | @@ -439,5 +439,6 @@ Nothing under this directory may be cited as evidence that a research claim is p closed or certified. A `proved` statement entry of another package listed in the register is evidence about the registered Prop it names (and, for main's `formal/` targets, about a finite arithmetic identity), never about the claim row it sits under; `kernel-checked` is a run-receipt word (the proof packet's -hosted run 38121713840 receipted all of its theorems: PR head 910809d6, actual tested merge 5b198699… with base b2d70d77…, the -synthetic merge a pull_request run checks out, same tree as the head). +hosted run 38121713840 receipted the 52 theorems of PR head 910809d6: actual tested merge 5b198699… with base b2d70d77…, the +synthetic merge a pull_request run checks out, same tree as the head; the 8 of `P15Interpolation` by run 38149888699: PR head 0dcb0016, actual tested merge 4363b692… with base +79731b96…, the head of PR #422).