Lean verification specification: environment, statement-register table and 28 kernel-proved P15 arithmetic targets

docs/FORMAL_VERIFICATION.md

@@ -38,6 +38,8 @@ The controls include false fold and power inequalities, a `sorry` proof, an indi
 
 Use #95 and PR92 to claim work and avoid duplicate writers. The OpenAI implementation author does not supply independent review credit. Read the exact head before reviewing; changed source, scope or dependencies invalidate the prior alignment record.
 
+The [Lean verification specification](LEAN_VERIFICATION_SPECIFICATION.md) (2026-10-10) records, for every registered claim, which Lean statement exists and at which formal-progress label, together with the pinned environment and the exact gate commands; it adds no vocabulary to this guide, carries zero organizational-independence credit and moves no status.
+
 | Work offer | Required output | Boundary |
 |---|---|---|
 | Non-OpenAI statement/alignment reviewer | Source-pinned review of all 13 declarations, definitions and hypotheses; explicit lineage | Do not infer parent closure from scalar implications |

docs/RESEARCH_INDEX.md

@@ -127,7 +127,7 @@ Each row gives a front's current label and what remains open; the topic sections
 | RN shrinking witness pairs | Separate results, each at its own scope: the September note (upper bound only), remote-collision Theorem C, the planar moving cutoff and the sub-pin corollary (see [RN counting](#rn-counting)). Open: mixed inner/outer pairs, an exact kernel, small-gap uniformity and higher dimensions for the moving cutoff | [Note](rn_d5_shrinking_witness_20260926.md), [remote collision](https://github.com/d6g8k5htny-coder/Math-/blob/79cb314d5b9f6b8b410bfd0df200414314f6b8c7/frontiers/remote_collision_20260928/PROOF.md), [off-pin review](https://github.com/d6g8k5htny-coder/Math-/blob/79cb314d5b9f6b8b410bfd0df200414314f6b8c7/reviews/d5_offpin_second_moment_20260928/REVIEW.md), [moving cutoff](https://github.com/d6g8k5htny-coder/Math-/blob/79cb314d5b9f6b8b410bfd0df200414314f6b8c7/frontiers/moving_remote_collision_20261003/README.md), [sub-pin corollary](https://github.com/d6g8k5htny-coder/Math-/blob/79cb314d5b9f6b8b410bfd0df200414314f6b8c7/frontiers/subpin_collision_20261002/README.md) |
 | RN collision register | [Math- #160](https://github.com/d6g8k5htny-coder/Math-/pull/160) and [Math- #173](https://github.com/d6g8k5htny-coder/Math-/pull/173): merged, reviewed and declarative; neither has been executed, so `math.rn-region.witness-collision` stays `OPEN_ACTIVE` (see [RN counting](#rn-counting)). Open: execution of both records by a non-Claude lane; no source defines another meaning for the node (Math- #173 §5), and the records establish no rate of convergence, no numerical constants, no uniformity as `k -> 0` or in `L` or `d`, no all-height statement and no elder selection of the extra points (§4 lists the rest) | [C6 reconciliation](https://github.com/d6g8k5htny-coder/Math-/blob/79cb314d5b9f6b8b410bfd0df200414314f6b8c7/reviews/c6_witness_collision_reconciliation_20260929/RECONCILIATION.md), [residual closure](https://github.com/d6g8k5htny-coder/Math-/blob/79cb314d5b9f6b8b410bfd0df200414314f6b8c7/reviews/c6_residual_closure_20260930/RECONCILIATION.md) |
 | P15 | Theorem F, the full-range price theorem (OpenAI author), has an xAI/Grok nonauthor ACCEPT, reconciled on #74 for the realized disjoint family with demands `d_i >= 2`, every independent probability, `c_v <= phi(p_v)` and the same palette. The bipartite-overlap/even-capacity and tail/weighted-load successors (OpenAI authors) have an Anthropic/Claude scoped ACCEPT and landed through [Math- #124](https://github.com/d6g8k5htny-coder/Math-/pull/124). Open: arbitrary downsets and any unrestricted prize statement; demand one remains an obstruction | [Full-price review](https://github.com/d6g8k5htny-coder/Math-/blob/79cb314d5b9f6b8b410bfd0df200414314f6b8c7/reviews/p15_full_price_nonauthor_20260926/REVIEW.md), [overlap/tail review](https://github.com/d6g8k5htny-coder/Math-/blob/79cb314d5b9f6b8b410bfd0df200414314f6b8c7/reviews/p15_overlap_tail_claude_20260928/REVIEW.md), [integration record](https://github.com/d6g8k5htny-coder/Math-/blob/79cb314d5b9f6b8b410bfd0df200414314f6b8c7/docs/integration/2026-09-28-reviewed-mathematics.md), [#74](https://github.com/d6g8k5htny-coder/main/issues/74), [#67](https://github.com/d6g8k5htny-coder/main/issues/67) (closed review discussions) |
-| Formalization (Layer 1) | Independent alignment review of the 13 Math- pilot targets and the 31 main-side SIDE24 targets (cross-provider); the remaining "Numerical formalizer" steps — exact `c_{d,ref}` definition and a proof-producing enclosure — in the Mathlib package; D6 Theorem F's constant `ρ*` as the next full-theorem target | [Guide](FORMAL_VERIFICATION.md), [work item #95](https://github.com/d6g8k5htny-coder/main/issues/95), [Formal README](../formal/README.md), [review lane](../formal/REVIEW_LANE.md), [rollout record](FORMAL_VERIFICATION_ROLLOUT_20260927.md) |
+| Formalization (Layer 1) | Independent alignment review of the 13 Math- pilot targets and the 31 main-side SIDE24 targets (cross-provider); the remaining "Numerical formalizer" steps — exact `c_{d,ref}` definition and a proof-producing enclosure — in the Mathlib package; D6 Theorem F's constant `ρ*` as the next full-theorem target; the statement register of 2026-10-10 ([Lean verification specification](LEAN_VERIFICATION_SPECIFICATION.md): 171 claims, 33 `specified`, 138 `none`, no claim `proved`, alignment `PENDING_INDEPENDENT_REVIEW`) awaiting that independent review | [Guide](FORMAL_VERIFICATION.md), [work item #95](https://github.com/d6g8k5htny-coder/main/issues/95), [Formal README](../formal/README.md), [review lane](../formal/REVIEW_LANE.md), [rollout record](FORMAL_VERIFICATION_ROLLOUT_20260927.md) |
 
 Check current claims on #275 and #307 before writing, and release completed work. Offered reviews are not accepted tasks or evidence of active agents. This table routes to source and review records; it is not a status register.
 

formal/ALIGNMENT.md

@@ -39,3 +39,31 @@ reports `kernel-checked`. Nothing here is a Layer 0 review outcome.
 | `UniversalLaw.Side24.d3_endpoints_adjacent` | Published d=3 endpoints are adjacent 20-digit decimals | `"3": { "lower": "0.04177593184059834334", "upper": "0.04177593184059834335"` | side24-enclosure | that c_3,24 lies between them |
 | `UniversalLaw.Side24.d3_below_d2` | Published d=3 interval lies below the d=2 interval | `"scientific_acceptance": false` | side24-enclosure | anything about the true coefficients |
 | `UniversalLaw.Side24.endpoints_in_unit_tenth` | Published endpoints lie in (0, 1/10) | `"relative_periodization_bound": "1e-106"` | side24-enclosure | anything about the true coefficients |
+| `UniversalLaw.P15.smallest_member_block_size` | Smallest one-block member has block size 1·1+1 = 2 | `one-block member: a_1=d_1=1, X={x,y}` | p15-price-boundary | the realized-cover theorem or its family; the probability or price semantics; the two log inequalities; Theorem F; prize status |
+| `UniversalLaw.P15.demand_one_good_sets` | Good sets of the demand-one block are ∅, {x}, {y} (finite enumeration) | `Its good sets are the empty set and singletons` | p15-price-boundary | the downset D beyond the four enumerated subsets; the log inequalities phi(1/2)=log 2>2/3 and log(4/3)<1/3; Theorem F; prize status |
+| `UniversalLaw.P15.demand_one_obstruction` | One-piece obstruction O_1(D) is exactly {X} (finite enumeration) | `its one-piece obstruction is exactly {X}` | p15-price-boundary | the identity I_1(D)=D in general; cover semantics; the log inequalities; Theorem F; prize status |
+| `UniversalLaw.P15.good_measure_three_quarters` | mu_p(D) = 3/4 at p = 1/2 as 3 of 4 quarter-weights (total 4 = 2^2) | `Nevertheless mu_p(D)=3/4` | p15-price-boundary | the product-measure semantics of mu_p; the identity min(1,-log mu_p(D))=log(4/3); the inequality log(4/3)<1/3; Theorem F; prize status |
+| `UniversalLaw.P15.generator_prices_ninths` | Generator costs 1, 2/3, 2/3, 4/9 over denominator 9: 9, 6, 6, 4 | `The possible generator costs are1,2/3,2/3,4/9` | p15-price-boundary | admissibility of c=2/3 as a transformed price (phi(1/2)=log 2>2/3 is a log inequality); that extra generators cannot lower the minimum; Theorem F; prize status |
+| `UniversalLaw.P15.minimum_generator_price_exceeds_third` | Minimum displayed generator cost 4/9, and 4/9 > 1/3 (1·9 < 4·3) | `covercost_c(O_1(D))=4/9 > 1/3 > log(4/3)` | p15-price-boundary | that the minimum over the four subsets is the exact optimal cover price (every cover of {X} containing a generator inside X, and extra nonnegative-price generators not lowering it, are set-theoretic steps of the source); the inequality 1/3 > log(4/3); that the same-palette extension to c<=phi(p) is false in general; Theorem F; prize status |
+| `UniversalLaw.P15.benchmark_block_and_ground_sizes` | Benchmark sizes: 1·408+1 = 409 per block, 6·409 = 2454 vertices | `EACH original block has409 vertices and the original ground set has2454 vertices` | p15-realized-covers | the construction (P1)–(P2), Proposition P1, probability semantics; Theorem P2; prize status |
+| `UniversalLaw.P15.four_block_supports_fifteen` | C(6,4) = 15 four-block supports | `H consists of all15 four-block subsets` | p15-realized-covers | the clutter structure of H or Proposition P1; Theorem P2; prize status |
+| `UniversalLaw.P15.minimal_forbidder_counts` | (P10) 6·C(409,2) = 500616 and 15·409^4 = 419743994415 | `6*binom(409,2)=500616 internal pairs, 15*409^4=419743994415 crossing transversal quadruples.` | p15-realized-covers | that these numbers count the minimal forbidders (Proposition P1); Theorem P2; prize status |
+| `UniversalLaw.P15.palette_816_from_two_label_classes` | K_H(408,…,408) = 816 as 408 + 408 | `K_H(408,...,408)=816` | p15-realized-covers | that the two label classes satisfy (P6) or that no smaller palette does (the palette optimum); Theorem P2; prize status |
+| `UniversalLaw.P15.palette_815_fails_by_counting` | 2454−6 = 2448, 815·3 < 2448, 6·408 = 2448 | `omitting one vertex from each block leaves2448 vertices, each color holds at most3, and815*3<2448` | p15-realized-covers | that each colour class holds at most three vertices (the combinatorial step); Theorem P2; prize status |
+| `UniversalLaw.P15.whole_ground_chromatic_818` | 2454/3 = 818 exactly (818·3 = 2454) | `needs818 colors, since2454/3=818` | p15-realized-covers | the chromatic number of the ground set (K_H(d+1)) or the palette argument; Theorem P2; prize status |
+| `UniversalLaw.P15.elementary_palette_formula_instances` | (P9) right-hand side at the benchmark: max(408,⌈2448/3⌉) = 816, max(409,⌈2454/3⌉) = 818; 3+1 = 4 | `K_H(d)=max(max_i d_i, ceil(sum_i d_i/s))` | p15-realized-covers | the formula (P9) itself (cyclic-word construction and lower bounds); that K_H of the section-6 benchmark equals the (P9) value; Theorem P2; prize status |
+| `UniversalLaw.P15.macro_triangle_three_colors` | (P9) right-hand side for the macro triangle at unit demands: max(1,⌈3/1⌉) = 3 | `The macro triangle at unit demands needs3 colors` | p15-realized-covers | that the triangle needs 3 colours (the formula (P9) and its applicability); the comparison with a size-two edge-load formula; Theorem P2; prize status |
+| `UniversalLaw.P15.ceil_block_over_capacity_instances` | ⌈(a·d+1)/a⌉ = d+1 at five (a,d) instances including (1,408) | `ceil(n_i/a_i)=d_i+1` | p15-realized-covers | the identity for all a_i >= 1; that the whole-ground chromatic number is K_H(d+1); Theorem P2; prize status |
+| `UniversalLaw.P15.block_occupancy_one_percent` | 409·100 = 40900 behind 409p = 1/100 at p = 1/40900 | `each block's occupancy probability is at most409p=1/100` | p15-realized-covers | the union bound giving occupancy probability at most 409p; probability semantics; Theorem P2; prize status |
+| `UniversalLaw.P15.low_failure_union_bound_arithmetic` | (P11) 500616/40900^2 + 15/100^4 = 2449227/8180000000 < 3/10000, cross-multiplied; 10000−3 = 9997 | `=2449227/8180000000 < 3/10000` | p15-realized-covers | the union bound Q <= ..., the independence of block occupancies, that Q = 1 - mu_p(D) is the global bad probability, probability semantics, display (P8); Theorem P2; prize status |
+| `UniversalLaw.P15.cover_price_numerator_and_denominator_positive` | 6/(40900^409) > 0 as 0 < 6 and 0 < 40900^409 (core Nat.pow_pos) | `6/(40900^409)>0` | p15-realized-covers | the price identity 6/(40900^409) for the six-generator cover (the kernel does not evaluate the power, only its positivity); probability semantics; Theorem P2; prize status |
+| `UniversalLaw.P15.rho_star_endpoints_adjacent` | Published rho_star endpoints are adjacent 20-digit decimals | `0.84547981724898672067 < rho_star` | p15-full-price | that rho_star = 1/(3 - log(3e - 2)) lies between them (needs Real.exp/Real.log; Mathlib lane); Theorem F; prize status |
+| `UniversalLaw.P15.rho_star_upper_endpoint_below_six_sevenths` | Upper endpoint below 6/7: …68·7 < 6·10^20 | `< 0.84547981724898672068 < 6/7` | p15-full-price | rho_star < 6/7 as a statement about the real number; h_star > 7/6; Theorem F; prize status |
+| `UniversalLaw.P15.sixteen_twentysevenths_below_six_sevenths` | 16/27 < 6/7 (16·7 < 6·27) and 16/27 below the published lower endpoint | `gives the stronger factor16/27 on its smaller domain` | p15-full-price | Theorem (T1) or its domain p_v <= 1/4; that 16/27 < rho_star as a real-number statement; Theorem F; prize status |
+| `UniversalLaw.P15.minimal_block_size_instances` | 1·2+1 = 3 and 2a+1 <= ad+1 at five (a,d) instances with d >= 2 | `Our n=ad+1 and d>=2 imply n>=2a+1.` | p15-full-price | the implication for all a >= 1, d >= 2; the binomial tail comparison (F9)–(F11); the sharpness argument of section 5; Theorem F; prize status |
+| `UniversalLaw.P15.e_rational_bounds_ordering` | 31967/11760 < 87/32 and 87/32 − 31967/11760 = 11/23520, cross-multiplied | `e < 31967/11760 < 87/32, 87/32-31967/11760=11/23520.` | p15-full-price | e < 31967/11760 (exponential series plus geometric tail); any statement about e; Theorem F; prize status |
+| `UniversalLaw.P15.exp_eleven_sixths_taylor_certificate` | Degree-5 Taylor partial sum of exp(11/6) minus 197/32 equals 26081/933120 > 0 | `sum_(j=0)^5 (11/6)^j/j! -197/32=26081/933120>0` | p15-full-price | that the partial sum is below exp(11/6) (positivity of the omitted terms is analysis); 197/32 < exp(11/6); Theorem F; prize status |
+| `UniversalLaw.P15.h_star_rational_certificate_constants` | 3·87 − 2·32 = 197 and 3·6 − 11 = 7 behind 3e−2 < 197/32 and h_star > 7/6 | `Therefore 3e-2<197/32<exp(11/6), giving h_star>7/6 and rho_star<6/7.` | p15-full-price | e < 87/32, 197/32 < exp(11/6), monotonicity of log, h_star > 7/6 and rho_star < 6/7 as real-number statements; Theorem F; prize status |
+| `UniversalLaw.P15.t3_ratio_at_minimal_block` | (T3) at a = 1, n = 3: 4^3 = 4^1·4^2, 4^2 = 16, 3^3 = 27, (4/3)(4/9)^1 = 16/27 | `= (4^(a+1))/(3^n) <= (4/3)*(4/9)^a <=16/27.` | p15-price-budget | the ratio chain (T3) (which uses (T2), p_v <= 1/4 and independence); Theorem (T1); the demand-one counterexample's applicability at a = d = 1; prize status |
+| `UniversalLaw.P15.t3_bound_finite_instances` | (T3) final inequalities at seven (a,n) pairs with n >= 2a+1 and at a = 1..6 | `<= (4/3)*(4/9)^a <=16/27` | p15-price-budget | the inequalities for all a >= 1, n >= 2a+1; (T2); Theorem (T1); prize status |
+| `UniversalLaw.P15.explicit_rational_price_above_p` | c = p + p^2/2 = 81801/3345620000 at p = 1/40900, and c > p | `c=p+p^2/2=81801/3345620000` | p15-price-budget | admissibility c <= phi(p) (the integral inequality); the price bound (T7); that the 816-label cover is valid at these prices; prize status |