diff --git a/docs/FORMAL_VERIFICATION.md b/docs/FORMAL_VERIFICATION.md index 741bfdd73..ec35e3d95 100644 --- a/docs/FORMAL_VERIFICATION.md +++ b/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 | diff --git a/docs/LEAN_VERIFICATION_SPECIFICATION.md b/docs/LEAN_VERIFICATION_SPECIFICATION.md new file mode 100644 index 000000000..7aefb0822 --- /dev/null +++ b/docs/LEAN_VERIFICATION_SPECIFICATION.md @@ -0,0 +1,906 @@ +# Lean verification specification + +Scientific effect: **NONE.** This document specifies how every piece of mathematical work in this +programme can be stated, and where possible checked, in Lean 4, with exact versions, install +commands, gates and receipts. It is a specification and an inventory of formal *statements*. It is +not a status register: no entry here is an acceptance, and no label here moves a Layer 0 verdict +(`STATUS.md`, `PROOF_INDEX.md`, `claims/LANDING_CLAIMS.json`, the D0–D7 graph). Author: Anthropic / +Claude (Claude Code cloud session `session_01Cz7WZybv8znP64SpPj6sWY`, 2026-10-10, updated 2026-10-11, 2026-10-12 and 2026-10-13), same GitHub +account as every other lane: organizational-independence credit **0**. + +Read first: [docs/FORMAL_VERIFICATION.md](FORMAL_VERIFICATION.md) (the lane contract), +[formal/README.md](../formal/README.md) (the main-side package), +[docs/agents/LEAN_AUDIT_OWNER.md](agents/LEAN_AUDIT_OWNER.md) (the coverage map and the missing +interfaces I1–I4). This document adds no vocabulary to that contract. + +## 1. What "verified in Lean" can and cannot mean here + +The lane separates five questions (guide §"One proof, several separate questions"). Only the +third is answered by Lean: + +| Question | Answered by | Label | +|---|---|---| +| Are these the intended bytes? | repository + commit + path + SHA-256, bound in a manifest | — | +| What is the formal statement? | a Lean declaration whose docstring quotes the informal anchor | `specified` | +| Does the proof establish that statement? | pinned build + `leanchecker` + transitive axiom audit + negative controls, in a trusted run | `proved` at source, `kernel-checked` only in a run receipt | +| Is the formalization faithful? | an independent statement/alignment review (different provider, family and agent) | `PENDING_INDEPENDENT_REVIEW` until one exists | +| May the scientific claim be promoted? | the existing controlling acceptance machinery | never by this document | + +Formal-progress labels are exactly `none`, `specified`, `proved`, `kernel-checked`. In the ladder of +work item #95 (GitHub issue, closed 2026-09-27) (L0 prose … L5 proof-assistant checked), a target with a trusted +`kernel-checked` receipt is L5 evidence **for exactly that target**; a `specified` statement is not +evidence of truth at all — it is a precise question. Allowed transitive axioms of every proof: +`propext`, `Classical.choice`, `Quot.sound`. `sorryAx`, `Lean.ofReduceBool` (`native_decide`) and +custom axioms are refused by every gate. Unformalised parents enter as explicit hypotheses or as +fields of interface structures, never as axioms. + +Four things follow, and the claim table below is read with them in mind: + +1. **A statement is not a proof.** The new statement-only package (§3.6) moves a claim's formal-progress + label from `none` to `specified`, a label about the existence of a Lean sentence, not about the + claim's status; it proves nothing. Its value is that each informal theorem now has one exact + Lean sentence that an independent reviewer can compare with the source and that a future + prover can target. +2. **An arithmetic skeleton is not the theorem.** The integer identities on `main` + (§3.1; `proved` at source, `kernel-checked` only where a trusted receipt exists) establish the + displayed numbers, not the analysis around them. A claim whose skeleton is + kernel-checked stays `none` or `specified` as a claim. +3. **Nothing here is alignment-reviewed.** Every Lean object in this programme is author-side until a + reviewer with a different provider, family and agent records an alignment through the + existing validators (`tools/formal_gate_check.py --alignment`, Math- `formal/gate.py --alignment`); the bounded + same-account nonauthor reviews and the engineering integrations recorded in §3, §5.1 and §8 are technical records at + organizational-independence credit 0, not alignment records. +4. **A proved Prop is not an accepted claim.** The proof packet (§3.7) proves 77 of the 143 registered + Props exactly as stated, and all 78 of its theorems carry a hosted kernel receipt: 60 as before (the 8 of module + `P15Interpolation`, PR #423, by run 38149888699: PR head `0dcb0016`, actual tested merge `4363b692…`; all 60 corroborated on + PR #423 head `12e072d6` by run 38150363063, actual tested merge `86a6e8c8…`), the 13 of the round-4 modules + `Side24Analysis`, `Side24Interfaces` and `RNCluster` (branch `claude/lean-statement-proofs-round4-20261011`, PR #434) by run 38180705952 on + that PR: PR head `48bfcbae`, actual tested merge `9833d6d9…` with base `12e072d6…` (then the head of #423), receipt theorem_count 73 + (their first receipt; the same run receipts all 73 theorems of that head), and the 2 of the round-5 modules `Side24Covariance` + and `Side24ConeMoment` (branch `claude/lean-statement-proofs-round5-20261012`, PR #439) by run 38195810463 on that PR: PR head `c6ce0256`, + actual tested merge `1320c5b2…` with base `be014794…` (then the head of #434), receipt theorem_count 75 (their first receipt; the + same run receipts all 75 theorems of that head), and the 3 of the round-6 module `Side24Images` (branch + `claude/lean-statement-proofs-round6-20261012`, PR #441, based on Math- main) by run 38277458954 on that PR: PR head `9e305ea5`, actual tested merge + `1376175c…` with base `a0323b94…` (Math- main at the merge of #440; this tested merge differs from the head only outside both packets), + receipt theorem_count 78 (their first receipt; the same run receipts all 78 theorems of that head). The whole packet is on Math- main + (rounds 1-5 since 2026-10-12, cut `4afcca6a`; round 6 since 2026-10-12T18:41:41Z, merge `aef861eb`; the statement register's round 7 since + 2026-10-13, final cut `7f5f1c82`, §3); + landing there is an engineering integration, not an acceptance and not an alignment, and it moves no label. Each receipted theorem is L5 + evidence for that Prop, for the formal objects it is stated about; a theorem without a hosted receipt + is `proved` as a packet label and not kernel evidence until a receipt names it; and the claim beneath it stays + `specified` or `none` (the register admits no other claim-level label) until an independent alignment + review and the controlling acceptance machinery say otherwise. + +## 2. Environment specification (exact versions) + +| Component | Pinned value | Where pinned | +|---|---|---| +| Lean | `leanprover/lean4:v4.34.1`, release commit `5045d0056413266e57c625dcd7c365b10e377c52` | every `lean-toolchain`; Math- `formal/gate.py` refuses any other `lean --version` string | +| Lake | `5.0.0-src+5045d00` (ships with the toolchain) | — | +| elan | CI: v4.2.4 init script `https://raw.githubusercontent.com/leanprover/elan/v4.2.4/elan-init.sh`, SHA-256 `a620ff1641616222c8d37c54845492004bb84d6877cdbc944dd65c1aa685bf53` | `.github/workflows/formal-verification.yml` | +| Mathlib | `d13f23b723b8a846827a245b89c10fc7d3f11612` | Math- `formal/lakefile.toml`, `lake-manifest.json`; the new packet copies the same lock | +| Mathlib's lock | plausible `118aa17ee84656b8bd727fef7c458ee8c833385c`, LeanSearchClient `ddf04cf3949fa556442341e87d47f9f6e6074707`, importGraph `e928b72544873815af278d38681b31c0293588e3`, proofwidgets `106ff4fafc74ef4ac99d81dbf3ab399118f497a5`, aesop `355695d523e41d0554926416cba2a2b3544fbbc9`, Qq `6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259`, batteries `f2effa3d803fda822b1f97b806c47cf2adfbcbc2`, Cli `e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204` | Math- `formal/manifest.json` `dependency_revisions`; the gate refuses lock drift | +| main `formal/` dependencies | none (`dependency_revisions: {}`) | `formal/manifest.json` | +| Python | 3.11, standard library only; tests with `unittest` in normal and `-O` modes | repository convention | +| GitHub actions | `actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1`, `actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97`, `leanprover/lean-action@f061402b660e0c34644504b324e830f2991d4865` (`use-mathlib-cache: 'true'`, `use-github-cache: 'false'`), `actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a` | the formal workflows | +| OS used for the measurements below | Ubuntu 24.04.4 LTS, x86_64, 4 CPUs, 15 GB RAM | this session's sandbox | + +### 2.1 Install (standard route, needs `release.lean-lang.org` and GitHub) + +```sh +curl -sSfL https://raw.githubusercontent.com/leanprover/elan/v4.2.4/elan-init.sh -o /tmp/elan-init.sh +echo 'a620ff1641616222c8d37c54845492004bb84d6877cdbc944dd65c1aa685bf53 /tmp/elan-init.sh' | sha256sum -c - +sh /tmp/elan-init.sh -y --default-toolchain none +export PATH="$HOME/.elan/bin:$PATH" +elan toolchain install leanprover/lean4:v4.34.1 +lean --version # Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release) +``` + +### 2.2 Install (restricted network: only GitHub release downloads reachable) + +This is the route that worked in the sandbox used for this document, where +`release.lean-lang.org` (elan's toolchain host) is blocked: + +```sh +# elan binary from its GitHub release (sha256 observed here: f81c2e48c1588d4612cd2c8851947898a45ac8d72748a07dff3a5694f1cf589b) +curl -sSfL https://github.com/leanprover/elan/releases/download/v4.1.2/elan-x86_64-unknown-linux-gnu.tar.gz -o elan.tgz +mkdir -p elan && tar -xzf elan.tgz -C elan && ./elan/elan-init -y --default-toolchain none +export PATH="$HOME/.elan/bin:$PATH" +# Lean release tarball (580 MB; sha256 observed here: 47bf4bbd78f70c2e9670598ab7124d92b6efb7330ff33e5fbb4030f6fd72e4e4; unpacks to 3.0 GB) +curl -sSfL https://github.com/leanprover/lean4/releases/download/v4.34.1/lean-4.34.1-linux.tar.zst -o lean-4.34.1-linux.tar.zst +mkdir -p toolchain && tar --zstd -xf lean-4.34.1-linux.tar.zst -C toolchain +elan toolchain link leanprover/lean4:v4.34.1 "$PWD/toolchain/lean-4.34.1-linux" +elan default leanprover/lean4:v4.34.1 +``` + +The two hashes above were computed on the files downloaded in this session; they are not an +official checksum publication and should be re-verified against the release assets. + +### 2.3 Mathlib: cache or source + +Every Mathlib-dependent package here (`Math-` `formal/`, the companions, `CapFirstExit`, the new +specifications packet) is built with the Mathlib olean cache: + +```sh +cd # e.g. Math-/formal +lake exe cache get # needs https://cache.mathlib.org (Mathlib's olean cache) +lake build +``` + +Hosts a build machine must reach: `github.com` (git clones, release assets), `raw.githubusercontent.com` +(elan script), `release.lean-lang.org` (toolchain downloads via elan), `cache.mathlib.org` (Mathlib +olean cache; `lake exe cache get` fails closed without it), `reservoir.lean-lang.org` (Lake's +package index, consulted on `lake update`; not needed for a locked build). GitHub-hosted CI reaches +all of them; `lean-action` restores the cache in minutes. + +Without the cache, Mathlib is built from source: `lake build` in the package directory compiles the +import closure. The `Math-` `formal/` package imports all of Mathlib (`import Mathlib` in two +modules), i.e. 8,529 modules at this revision. Measured in the 4-CPU / 15 GB sandbox: `lake build ResearchFormalCoreR1` in a copy of Math- `formal/` started at 17:24:45Z on 2026-10-10 and ended with +`Build completed successfully (8939 jobs)` at 20:42:15Z, i.e. **3 h 17 min 30 s** of wall clock on four cores that +other agents were competing for during most of that time (this session's 5,603-line Lake log, not part of any +repository; the intermediate readings were 539 of 8,529 module oleans after 7 min and 1,389 after 23 min). Re-counted after the +build, at 22:06Z: `find .lake/packages/mathlib/.lake -name '*.olean' | wc -l` gives 8,548 (the 8,529 +`Mathlib/**/*.lean` modules of this revision plus generated modules), and `du -sh .lake` gives 7.5 GB after the +Lake `*.setup.json` files (7.4 GB) and the generated C sources (0.4 GB) were deleted; the tree peaked at 15 GB at +completion (1.8 GB of oleans, 0.3 GB of ileans), so a from-source build needs at least 16 GB free and the cache +route about 6 GB. Elaborating the five statement-only modules against the built Mathlib +(`lake env lean -DwarningAsError=true`) took 41 s for `Field` (cold), 10 s `Lifetime`, 9 s `Side24`, 10 s `RN`, +9 s `P15`, each exiting 0 with zero warnings; the injected-type-error control exits 1. The proof packet +(§3.7) rebuilt its five P15 modules in 76 s after the change at `910809d6` (`lake build`, 8,936 jobs, the rest +up to date); its `leanchecker` replay of the Mathlib-importing environment needs about 14 GB and was +memcg-killed in this 15 GB sandbox, so that receipt comes from the hosted run only. +The dependency-free main package needs no cache and runs its full gate in about 12 s. + +### 2.4 Allowed hosts to request for a restricted sandbox + +If a cloud sandbox's egress policy is an allow-list, add: `cache.mathlib.org`, `release.lean-lang.org`, +`reservoir.lean-lang.org`, and (if Lake's own remote cache is to be used) `lakecache.blob.core.windows.net`. +In the sandbox used here all four were refused at CONNECT, and `codeload.github.com` and GitHub HTML +pages returned 403; `github.com///releases/download/...` and `git clone` over HTTPS worked. + +## 3. Packages, gates, receipts + +Each package has its own source-bound gate. A gate in source mode checks identities and refuses +self-awarded labels without running Lean; in execution mode it rebuilds from scratch, runs +`leanchecker`, audits `#print axioms` for every target, executes negative controls that must fail, +and writes a receipt. A receipt is evidence for exactly the targets it names at the commit it names. + +| # | Package | Repository / path | Backend | Targets | Gate (source / execute) | Receipt | +|---|---|---|---|---|---|---| +| 3.1 | SIDE24 arithmetic skeleton + P15 exact arithmetic | main `formal/` | core Lean, no deps | 59 theorems (31 SIDE24 at origin/main `f6deeba7` + 28 P15 at commit `91cffbb5` of main PR #358, not yet on main), by `decide` except one positivity conjunct by core `Nat.pow_pos` | `python3 tools/formal_gate_check.py` / `--run-lean` | `formal/.lake/formal-evidence/receipt.json`; bound to the required check `verify` by `tools/required_formal_check.py` | +| 3.2 | GP-FOR-192 scalar companions + measure bridge + weighted law + moment tail + generality + perturbation + D2 Schur | Math- `formal/` | Lean + Mathlib | 63 theorems | `python3 formal/gate.py` / `--execute` | `formal/.lake/formal-evidence/receipt.json`; bound to `math-downstream-gates` | +| 3.3 | D2 companions (moment bridge 16, atom integral 6, square Schur 4) | Math- `companions/d2_*_20261006/` | Lean + Mathlib, compiled against the hash-pinned core | 26 theorems | `bash companions//replay.sh` | `.lake/d2-moment-evidence/`, `.lake/d2-atom-integral-evidence/`, `.lake/d2-square-schur-evidence/` (`receipt.json` in each) | +| 3.4 | Cap first exit (D1 component III, topological global step) | Math- `frontiers/cap_first_exit_lean_20261002/` | Lean + Mathlib | 152 declarations (own gate) | `python3 gate.py` / `--execute` | `.lake/evidence/` | +| 3.5 | W3 SIDE24 source proposal | Math- `reviews/w3_side24_source_proposal_20261008/W3Scratch/` | Lean + Mathlib | 101 declarations, **unregistered**, built by no workflow | none | none | +| 3.6 | **Lean statement register** (this programme) | Math- `specifications/lean_statements_20261010/` (PR #419, on Math- main since its merge `d6f2c325`, 2026-10-12; round 7, the successor interface `PeriodicCoefficientInterface2` with `CoefficientEnclosure2` and `ReferenceComparison2` appended to `Side24.lean` and a Frontier section classifying the Props without a theorem, by PRs #445 and #447, merged `6b5b9a5d` and `7f5f1c82` on 2026-10-13) | Lean + Mathlib, statement-only | 153 registered declarations (143 `def … : Prop`, 10 interface `structure`s; the modules' other 132 declarations are non-Prop definitions), 0 theorems | `python3 check.py` / `--execute` | `.lake/evidence/receipt.json` with `formalization_status: "specified"` — never `proved` | +| 3.7 | **Lean statement proofs** (this programme) | Math- `specifications/lean_statement_proofs_20261011/` (rounds 1-2 in PR #422, round 3 in PR #423, round 4 in PR #434 on branch `claude/lean-statement-proofs-round4-20261011`, round 5 in PR #439 on branch `claude/lean-statement-proofs-round5-20261012`, round 6 in PR #441 on branch `claude/lean-statement-proofs-round6-20261012`; each of the first five PRs was stacked on its predecessor, #422 on #419, and all five landed on Math- main by normal protected merge commits on 2026-10-12, cut `4afcca6a`; #441 was based on Math- main and landed by the same route at 2026-10-12T18:41:41Z, merge `aef861eb`: see the landing paragraphs below this table) | Lean + Mathlib, path dependency on 3.6 | 78 theorems whose types are exactly 77 registered Props of 3.6 (`P15Elementary` 17, `P15Structure` 13, `P15Hazard` 3, `P15Covers` 4, `P15Budget` 5, `P15Interpolation` 8, `Side24Elementary` 5, `Side24Analysis` 9, `Side24Interfaces` 3, `Side24Covariance` 1, `Side24ConeMoment` 1, `Side24Images` 3, `RNProbability` 5, `RNCluster` 1); axioms exactly `propext`, `Classical.choice`, `Quot.sound` | `python3 check.py` / `--execute` | `.lake/evidence/receipt.json` with `formalization_status: "kernel-checked"` (source mode says `proved`); 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, recorded as `checked_commit`), run 38116277597 the first 38 (PR head `00d2ac6e`; actual tested merge `c4c66bb8…`), run 38122386459 corroborates (PR head `d9b8dd33`; actual tested merge `866136cc…`), run 38124262242 the same 52 on PR head `79731b96` (actual tested merge `318ff194…`); run 38149888699 receipted all 60 on PR #423 head `0dcb0016` (actual tested merge `4363b692…` with base `79731b96…`, then the head of #422; `leanchecker` PASS; artifact `lean-specification-proofs-38149888699-1`) after run 38149524759 on head `88c21058` (actual tested merge `3306233b…`, same base) first receipted the 8 `P15Interpolation` theorems; run 38150363063 corroborates the same 60 on PR #423 head `12e072d6` (actual tested merge `86a6e8c8…`, same base; theorem_count 60; artifact `lean-specification-proofs-38150363063-1`); run 38180705952 receipted all 73 on PR #434 head `48bfcbae` (actual tested merge `9833d6d9…` with base `12e072d6…`, then the head of #423; `leanchecker` PASS; theorem_count 73; artifact `lean-specification-proofs-38180705952-1`, sha256 `87309efa…`), the first receipt of the 13 theorems of the round-4 modules (`Side24Analysis` 9, `Side24Interfaces` 3, `RNCluster` 1; branch `claude/lean-statement-proofs-round4-20261011`, then stacked on #423); run 38195810463 receipted all 75 on PR #439 head `c6ce0256` (actual tested merge `1320c5b2…` with base `be014794…`, then the head of #434; `leanchecker` PASS; theorem_count 75; artifact `lean-specification-proofs-38195810463-1`, sha256 `d8abd42b…`), the first receipt of the 2 theorems of the round-5 modules (`Side24Covariance` 1, `Side24ConeMoment` 1; branch `claude/lean-statement-proofs-round5-20261012`, then stacked on #434); run 38198716748 corroborates the same 75 on PR #439 head `32fc9845` (actual tested merge `37e0f1d8…`, same base; theorem_count 75); at the cut `4afcca6a` the integrator's pre-merge run 38205232428 receipted 75 theorems over 74 Props on PR #439's head at merge `de732f1e`, the integration candidate (actual tested merge `8fe0759e…`, whose tree is the landing tree of `4afcca6a`); run 38277458954 receipted all 78 on PR #441 head `9e305ea5` (actual tested merge `1376175c…` with base `a0323b94…`, Math- main at the merge of #440; `leanchecker` PASS; theorem_count 78; artifact `lean-specification-proofs-38277458954-1`, sha256 `1f32d60e…`), the first receipt of the 3 theorems of the round-6 module (`Side24Images` 3; branch `claude/lean-statement-proofs-round6-20261012`); run 38285814238 corroborates on PR #441 head `4a3fbadf` (actual tested merge `0017d0ce…`, same base) and run 38291534116 on the integrator's carry `f42491e1` (actual tested merge `fc139a56…`, same base; 78 theorems over 77 Props per the integrator's readback), whose tree `141dc082…` is the landing tree of `aef861eb` | + +The main-side gate in detail (`tools/formal_gate_check.py`): manifest shape and self-award refusal; +SHA-256 of every bound file; toolchain and lock; the root module imports exactly the registered +modules; no `sorry`, `native_decide` or `axiom` outside comments; the target inventory equals the +`theorem` declarations in order; every informal anchor is a verbatim substring of its byte-pinned +source; every package file is bound or declared unbound; `ALIGNMENT.md` matches the manifest. With +`--run-lean`: fresh `lake build`, `lake env leanchecker UniversalLaw`, `#print axioms` for every +target restricted to the three allowed axioms, elaborated types, the manifest's textual mutation +controls (each must fail in Lean), the `sorry` / imported-axiom / `native_decide` controls (each must +be caught by the axiom audit), Lean version check, receipt. The Math- gates follow the same shape; +their differences are recorded in [docs/agents/LEAN_AUDIT_OWNER.md](agents/LEAN_AUDIT_OWNER.md). + +The statement-register gate (3.6) additionally refuses any `theorem`, `lemma`, `example`, +`instance`, `axiom`, `opaque`, `unsafe`, `partial`, `macro` or `set_option` in the packet, requires +every top-level `def … : Prop` and `structure` to be registered in `REGISTER.json` (and vice +versa), requires every anchor to be verbatim in the pinned bytes under `sources/`, and refuses a +register row or receipt that says `proved` or `kernel-checked`: a statement package cannot +self-award a proof label. + +The proof-packet gate (3.7) requires every inventoried theorem's type to be exactly a registered Prop of 3.6 +applied to the theorem's own binders (a theorem with an extra hypothesis, an implication `P → P`, a narrowed +argument or an unregistered type is refused, first by a source scan and then by a Lean-side audit of the +elaborated `ConstantInfo`), refuses `sorry`, `axiom`, `native_decide`, `unsafe`, `opaque`, metaprogramming +and `#` commands lexically, audits the transitive axioms of every constant the modules add, replays the +build with `leanchecker`, runs negative controls (a `sorry` caught by the axiom audit, a custom axiom, an +unregistered type, a smuggled hypothesis, a false arithmetic statement rejected by Lean) and writes the only +record that may say `kernel-checked`. Helpers live in `Aux` namespaces and are audited but not inventoried; +a module may import a sibling proof module of the packet. + +**Landing on Math- main (2026-10-12).** The statement register (3.6) and the proof packet (3.7) landed on Math- main through five normal +protected merge commits (no squash, rebase or force push), in stack order (times are GitHub `merged_at`; each merge commit's own committer date is at most one second earlier): #419 (statement register) by `d6f2c325c55b78002a113e827d23539df90cad88` at 2026-10-12T03:57:27Z; #422 (proof packet, rounds 1-2) by `8a61d5fb59fa8fa18bddcfc7d8f8bb88b12a46c0` at 04:10:53Z; #423 (round 3) by `6e366697546ad2afadb84150e0d4c609d0918945` at 04:24:30Z; #434 (round 4) by `7fd045a6677bc27b95c05c4149bbf51e86c364b9` at 04:40:46Z; #439 (round 5) by `4afcca6a79a8a0acef251ae73988a7914c8080e7` at 04:57:01Z, the cut whose `REGISTER.json` (blob `05cc80c1`, 599,058 bytes, +sha256 `d185a292c20084d6f12e56a4ed76f7d6b9294b0d224830e47885934b1869f87c`) this document rendered until 2026-10-13. Each merge was made by a distinct +OpenAI/Codex engineering integrator under the same project account (organizational-independence credit 0): an engineering integration, not a +mathematical acceptance and not an alignment, and it moves no claim, Prop or theorem label. For the final cut the integrator's pre-merge hosted +runs (event pull_request) ran on PR #439's head at merge, `de732f1e8622ad92d80126e11df8ace85075f0ed` (the integration candidate: a merge of the then-current +Math- main into the PR branch), actual tested merge `8fe0759edb8d93b9cfc840ebbafb5ea8cb6b7ca4`: the proof run 38205232428 (attempt 1; receipt `kernel-checked`, +75 theorems over 74 Props, `leanchecker` PASS), the statement run 38205232441 (PR head `de732f1e`, actual tested merge `8fe0759e…`; receipt +`specified`, 150 registered declarations) and the required-aggregate run 38205232621 (PR head `de732f1e`, actual tested merge `8fe0759e…`). The tested merge's tree +`d323c3d63c3afd9981f679c6fb1c873f09772523` equals the landing tree of `4afcca6a` (integrator review 5486666735 and release comment +6118068559 on Math- PR #439). The landing push run 38205855996 (event push: its checked commit is the pushed merge `4afcca6a` +itself, with no PR head and no synthetic merge) ran only `downstream-replay`, `formal / formal-evidence` and `math-downstream-gates`; it did not +run the Lean statement or proof packets and is not a receipt for them. + +**Later landings (2026-10-12 and 2026-10-13).** Round 6 of the proof packet, Math- PR #441 (branch `claude/lean-statement-proofs-round6-20261012`, based on Math- main `a0323b94ae54a78f3d2878dc9c358dc40cdfe1dc`, the merge of #440, not stacked on a PR), landed by `aef861eb4eba87be910e300c5d39da60ddf7cefc` at 2026-10-12T18:41:41Z (GitHub `merged_at`), its head at merge the integrator's pure current-main carry `f42491e1ac057d708d0632c636ca8cc81705f335` of the reviewed receipt-binding head `4a3fbadf`; the carry's pre-merge runs (event pull_request) are the proof run 38291534116, the statement run 38291534102 and the required-aggregate run 38291534324, all on PR head `f42491e1`, actual tested merge `fc139a565e34037f6c348844686a46f8008e7fe0` (whose tree `141dc082db9beba4680be08e687cb5bf972f7b8b` is the carry's and the landing tree); the landing push run 38292645778 (event push: its checked commit is the pushed merge `aef861eb` itself) ran only `downstream-replay`, `formal / formal-evidence` and `math-downstream-gates`. The statement register's round 7 landed on 2026-10-13: Math- PR #445 (branch `claude/lean-statements-frontier-20261013`, documents only: the Frontier section) by `6b5b9a5d7cd1c7f89c2dc5139277c36c8ebe2aaa` at 2026-10-13T05:15:38Z (head `0c506fea`; pre-merge runs 38347541337, 38347541202 and 38347541846 on PR head `0c506fea`, actual tested merge `640093a349a3eb9c66d4abac1a47eb9601062cb6` with base `8acc4856…`, same tree as the head; landing push run 38350487388, checked commit the pushed `6b5b9a5d` itself), and Math- PR #447 (branch `claude/lean-statements-round7-side24b-20261013`, the successor interface `PeriodicCoefficientInterface2` with `CoefficientEnclosure2` and `ReferenceComparison2`) by `7f5f1c82478dd8b983759143922224b634a27679` at 2026-10-13T05:27:53Z (its head at merge the integrator's carry `f6ba2e6ab398b2c4081d0de2a551caea2e6d46ba` of the reviewed head `06f03d06`, both with tree `d2f5bd70…`; pre-merge runs 38350897827, 38350897766 and 38350898066 on PR head `f6ba2e6a`, actual tested merge `ce3b69d322466e36936d5c64988dd387266c0536` with base `6b5b9a5d…`, same tree as the head; landing push run 38351512610, checked commit the pushed `7f5f1c82` itself), the final cut, whose `REGISTER.json` (blob `2eed9bf7`, 626,270 bytes, sha256 `64674ac463c624d1258c5b7e6766bf0482e14b4a1ad241480f0b0c4de306eaf4`) is the register this document renders. Each of these merges was made by an OpenAI/Codex engineering integrator under the same project account (organizational-independence credit 0): an engineering integration, not a mathematical acceptance and not an alignment, and it moves no claim, Prop or theorem label; the push runs ran no Lean packet and are not receipts for them. The 28 P15 targets of main PR #358 (3.1) are still not on main. + +## 4. The statement register + +`specifications/lean_statements_20261010/REGISTER.json` (Math-) lists every registered mathematical +claim of the programme with: the byte-pinned Layer 0 source (repository, commit, path, bytes, +SHA-256), the transcribed LANDING_CLAIMS disposition where one exists (never re-derived), the Lean +statement(s) that specify it, their formal-progress label, what is not established, and the next +step toward a proof. The rendered table: + +Column key. **Claim**: the register `claim_id`. **Layer 0 source**: `commit:path` of the byte-pinned source under `sources/` in the packet (SHA-256 and byte count are in `REGISTER.json` `sources[]`), followed by the heading the row anchors to; *not pinned* means the row has no pinned bytes in this packet and therefore no Lean statement. **Transcribed disposition**: verbatim from `LANDING_CLAIMS.json`, `—` where the source carries none; it is never re-derived. **Lean statement(s)**: `Module.Declaration` in namespace `UniversalLaw.Spec` of the packet, all at `specified`; `main:` prefixes a theorem of the `main` core-Lean package `formal/` listed beneath the claim with its own `proved` manifest label (an arithmetic skeleton, never the claim); `proof:` prefixes a theorem of the Math- proof packet `specifications/lean_statement_proofs_20261011` (Math- PRs #422, #423, #434, #439 and #441, landed on Math- main, cuts `4afcca6a` and `aef861eb`) whose type is exactly one of the registered Props of the row, label `proved` (52 kernel-checked by the hosted run 38121713840: PR head `910809d6`, actual tested merge `5b198699…` with base `b2d70d77…`, same tree as the head; run 38116277597, PR head `00d2ac6e`, actual tested merge `c4c66bb8…`, receipted the first 38; the 8 theorems of `P15Interpolation` (PR #423) by run 38149888699, PR head `0dcb0016`, actual tested merge `4363b692…` with base `79731b96…`, then the head of #422; all 60 corroborated on PR #423 head `12e072d6` by run 38150363063, actual tested merge `86a6e8c8…`; the 13 theorems of the round-4 modules `Side24Analysis`, `Side24Interfaces`, `RNCluster` (branch `claude/lean-statement-proofs-round4-20261011`, PR #434), added after head `12e072d6`, by run 38180705952, PR head `48bfcbae`, actual tested merge `9833d6d9…` with base `12e072d6…`, then the head of #423, which receipts all 73 theorems of that head; the 2 theorems of the round-5 modules `Side24Covariance`, `Side24ConeMoment` (branch `claude/lean-statement-proofs-round5-20261012`, PR #439), added after head `be014794`, by run 38195810463, PR head `c6ce0256`, actual tested merge `1320c5b2…` with base `be014794…`, then the head of #434, which receipts all 75 theorems of that head; the 3 theorems of the round-6 module `Side24Images` (branch `claude/lean-statement-proofs-round6-20261012`, PR #441), added after head `c6ce0256`, by run 38277458954, PR head `9e305ea5`, actual tested merge `1376175c…` with base `a0323b94…`, Math- main at the merge of #440, which receipts all 78 theorems of that head); a proof-packet theorem is evidence about its Prop for the formal objects, never about the claim. Two register fields of row `cert:math-full_price-full_price.py` are transcribed as the register has them although they predate round 3: its `not_established` calls `RhoStarEnclosure` specified only and its `next_step` (shown abridged) names proving it, while `P15Interpolation.rhoStarEnclosure` has been a theorem of exactly that Prop since round 3, kernel-checked by run 38149888699 (PR head `0dcb0016`, actual tested merge `4363b692…`); repairing those fields is a Math- register change, not made here, and it would move no label. **Formal progress**: the claim-level label; no claim is `proved` or `kernel-checked`. **Not established** and **Next step** are abridged here to their first sentence; the full fields in `REGISTER.json` and the packet's `SCOPE.md` are the authoritative text and are longer, not shorter, in what they exclude. Alignment of every statement with its anchor is `PENDING_INDEPENDENT_REVIEW`. + +#### 4.1 Landing claims (10: 8 `specified`, 2 `none`) — disposition transcribed verbatim from `claims/LANDING_CLAIMS.json` + +| Claim | Layer 0 source (commit:path) | Transcribed disposition | Lean statement(s) (module.declaration) | Formal progress | Not established | Next step | +|---|---|---|---|---|---|---| +| `side24-coefficient` | `760340e9:coefficients/side24_v1/PROOF.md` — Theorem | `REVIEWED_SCOPED` | 31 packet statements + 27 main theorems (`proved`) + 22 proof-packet theorems (`proved`): `Side24.ThetaSummable`, `Side24.IsUnitTuple`, `Side24.DerivativePairingBound`, … (+74 more) …, proof:`Side24Images.imageBound` (proved), proof:`Side24Images.entrywiseCovarianceBound` (proved), proof:`Side24Images.covarianceOrdering` (proved) | `specified` | Nothing here encloses the coefficient. | Math- Mathlib lane: CoefficientEnclosure, ReferenceComparison remain the targets of this row (the parametrised predicates IsUnitTuple, NegDefCone are vocabulary, not targets); every proof-packet … | +| `lifetime-remainder` | `760340e9:frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md` — Theorem R | `REVIEWED_SCOPED` | `Lifetime.RemainderBoundedR1`, `Lifetime.IsUnrestrictedPair`, `Lifetime.IsUnrestrictedLeadingCoefficient`, `Lifetime.IsLifetimeDensityVersion` | `specified` | RemainderBoundedR1 states the shape of (R1) for versions of the densities under the interface structures; the result is not proved. | State (R19) (cumulative form) as a further Prop; transcribe the parent interfaces consumed (section 8 comparison, section 9 as replaced by v1.1, section 10, (14.1), (15.2)) as explicit hypotheses … | +| `rn-count-interface` | `760340e9:frontiers/three_fronts_20260924/RN_COUNT_INTERFACE.md` — Theorem N | `HOLD_WITH_DOMAIN` | 5 packet statements + 5 proof-packet theorems (`proved`): `RN.HolderCountBoundN1`, `RN.HolderConsequenceN2`, `RN.ConditionalMeanIdentityN3`, … (+4 more) …, proof:`RNProbability.holderConsequenceN2` (proved), proof:`RNProbability.uniformCounterexampleN4` (proved), proof:`RNProbability.exponentialTailLayerCakeN5` (proved) | `none` | 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 … | State (N7) as an implication with the Kac-Rice numerator as an interface field (the integral of (N6) as a given quantity) and Z_r >= z_* r^2 as a hypothesis; then the claim would be `specified`. The … | +| `rn-fixed-remote-window` | `760340e9:frontiers/remote_window_20260924/PROOF.md` — Theorem A | `HOLD_WITH_DOMAIN` | `RN.PinnedLawInterface`, `RN.IsCriticalPoint`, `RN.HessianHasInertia`, `RN.FixedRemoteMeanMeasureA2`, `RN.FixedRemoteCountBoundA3` | `specified` | FixedRemoteMeanMeasureA2 and FixedRemoteCountBoundA3 state the shapes of displays (2) and (3) for any object satisfying PinnedLawInterface (the regression law Q_r, the weight W_r, the normalizer and the contact kernel Lambda_j … | State Section 6 ((15)-(16), separated m-tuples) as Props; record an inhabitant construction of PinnedLawInterface as a proof-lane target (Dirac mass at one admissible smooth path); independent … | +| `rn-fixed-annulus-window` | `760340e9:frontiers/rn_thin_tube_20260925/FIXED_ANNULUS_CANDIDATE.md` — Candidate theorem | `REVIEWED_SCOPED` | `RN.FixedAnnulusWindowCandidateA2` | `specified` | FixedAnnulusWindowCandidateA2 states the shape of (A2) (d = 2, fixed L, fixed scaled annulus, compact positive gaps, between-pin height window) over PinnedLawInterface; the result is not proved. | Pin TWO_SCALE_ADDENDUM.md and state (S3)-(S5) and (S20)-(S21); independent reviewer: alignment of FixedAnnulusWindowCandidateA2 with (A2), checking that the height window is strict and the constants … | +| `p15-realized-covers` | `760340e9:frontiers/three_fronts_20260924/P15_REALIZED_COVERS.md` — Theorem P | `HOLD_WITH_DOMAIN` | 27 packet statements + 12 main theorems (`proved`) + 20 proof-packet theorems (`proved`): `P15.RealizedData`, `P15.IsRealizedFamily`, `P15.IsGood`, … (+53 more) …, proof:`P15Covers.paletteNumberAttained` (proved), proof:`P15Covers.benchmark816UnionBound` (proved), proof:`P15Budget.coverCostHazardBound` (proved) | `specified` | Props of this row with a theorem of exactly their type in the proof packet specifications/lean_statement_proofs_20261011: PaletteNumberAttained, MinimalForbiddenCharacterisation, LocalRestriction, LocalDecomposability … | Proof lane: every theorem-shaped Prop of this row has a theorem (the parametrised predicates IsRealizedFamily, IsGood, IsKDecomposable, IsGeneratorCover, IsPaletteFeasible, IsMinimalForbidden … | +| `p15-price-boundary` | `760340e9:frontiers/three_fronts_20260924/P15_PRICE_BOUNDARY.md` — Counterexample | `EXACT_COUNTEREXAMPLE` | 3 packet statements + 6 main theorems (`proved`) + 3 proof-packet theorems (`proved`): `P15.TwoCoordGeneratorPrices`, `P15.DemandOneRefutation`, `P15.LogOnePlusBelowIdentity`, … (+6 more) …, proof:`P15Elementary.twoCoordGeneratorPrices` (proved), proof:`P15Elementary.logOnePlusBelowIdentity` (proved), proof:`P15Elementary.demandOneRefutation` (proved) | `specified` | 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)). | The hosted lean-specification-proofs.yml run 38116277597/tested-merge-c4c66bb8… (PR head 00d2ac6e, base b2d70d77…) produced the first receipt (`kernel-checked` appears only there); later commits need … | +| `p15-price-budget-restricted` | `760340e9:frontiers/price_budget_20260924/PROOF.md` — Theorem T1 | `HOLD_WITH_DOMAIN` | 8 packet statements + 3 main theorems (`proved`) + 8 proof-packet theorems (`proved`): `P15.LogRatioBound`, `P15.RatioExponentBound`, `P15.RestrictedLocalBudget`, … (+13 more) …, proof:`P15Budget.rhoTestSufficient` (proved), proof:`P15Budget.restrictedTransformedPriceBudget` (proved), proof:`P15Budget.benchmark816TransformedRange` (proved) | `specified` | 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 … | Math- Mathlib lane: every theorem-shaped Prop of this row has a theorem; every theorem of this row has a hosted receipt (run 38121713840/tested-merge-5b198699… (PR head 910809d6, base b2d70d77…)). | +| `p15-full-price` | `760340e9:frontiers/full_price_20260924/PROOF.md` — Theorem F | `REVIEWED_SCOPED` | 20 packet statements + 7 main theorems (`proved`) + 19 proof-packet theorems (`proved`): `P15.FullTransformedPriceBudget`, `P15.RhoStarEnclosure`, `P15.RhoStarBelowSixSevenths`, … (+40 more) …, proof:`P15Interpolation.fullGroundBudgetIff` (proved), proof:`P15Interpolation.localPriceBoundFull` (proved), proof:`P15Interpolation.fullTransformedPriceBudget` (proved) | `specified` | 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. | 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 … | +| `downstream-hard-gate` | `6c020d6a:frontiers/downstream_gate_20260925/GRAPH.json` — DOWNSTREAM-HARD-GATE-20260925-v1 (GRAPH.json; the README statement_path … | `ENGINEERING_HOLD` | — | `none` | An engineering control, not a mathematical claim: there is no theorem to state in Lean and none is stated. | 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. | + +#### 4.2 Downstream graph nodes (33: 18 `specified`, 15 `none`) — every `math.*` node of `frontiers/downstream_gate_20260925/GRAPH.json`; classifications are source identity + +| Claim | Layer 0 source (commit:path) | Transcribed disposition | Lean statement(s) (module.declaration) | Formal progress | Not established | Next step | +|---|---|---|---|---|---|---| +| `math.uniform-matrix-cap-lifetime` | `c3916425:imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` — Theorem A (uniform selection candidate); Theorem B (compact-mark … | — | 32 packet statements: `Field.IsLPeriodic`, `Field.IsSmooth`, `Field.GaussianFieldInterface`, … (+26 more) …, `Lifetime.ParentCompactWindowDensityB`, `Lifetime.IsUnrestrictedLeadingCoefficient`, `Lifetime.ParentUnrestrictedLeadingDensityC` | `specified` | ParentUniformSelectionA, ParentCompactWindowDensityB and ParentUnrestrictedLeadingDensityC state the shapes of (1.1), (1.2), (1.3) for every object satisfying the interfaces; nothing is proved. | 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 … | +| `math.d1-component.congruence-erratum` | `6c020d6a:frontiers/downstream_gate_20260925/GRAPH.json` — nodes.math.d1-component.congruence-erratum | — | — | `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. | 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). | +| `math.d1-component.section9-replacement-v1_1` | `6c020d6a:frontiers/downstream_gate_20260925/GRAPH.json` — nodes.math.d1-component.section9-replacement-v1_1 | — | — | `none` | No Lean statement: the repair's bytes are not pinned and no Prop states the weighted pair Kac-Rice identity (9.1) or its monotone-class extension to bounded Borel marks. | Pin REPAIR.md (blob fe9b9ce4, 9062 B); state (9.1)-(9.4) as Props over MeasureTheory.Measure on the pair domain with the Armentano-Azais-Leon identity as an interface hypothesis. | +| `math.d1-component.marked-cylinder-cap` | `c3916425:imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md` — Deterministic theorem | — | — | `none` | No Prop of this package states the deterministic cap theorem (unique transverse ridge, closed cap through S separating M from every older point, elder death partner of M is S under conditions (1)). | Register the CapFirstExit declarations here with their ALIGNMENT.md anchors against the pinned CAP bytes (statements of kind theorem, label proved, kernel_evidence cap-first-exit-lean.yml), or state … | +| `math.d1-component.reconciliation-record` | `6c020d6a:frontiers/downstream_gate_20260925/GRAPH.json` — nodes.math.d1-component.reconciliation-record | — | — | `none` | A review/reading-rule record, not a mathematical statement: nothing to state in Lean beyond what its components say. | Add the embedding radius as an explicit hypothesis to ParentUniformSelectionA / PairLawInterface once the reading rule is pinned; no proof target. | +| `math.lifetime-remainder` | `760340e9:frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md` — Theorem R | — | `Lifetime.RemainderBoundedR1` | `specified` | See row lifetime-remainder: (R1) is stated, not proved; the imports of parent interfaces D1-A-E are not transcribed; Theorem A's cubic bound (1.1) is not consumed by R and is not a hypothesis here. | As for row lifetime-remainder. | +| `math.side24-coefficient` | `760340e9:coefficients/side24_v1/PROOF.md` — Theorem | — | `Side24.PeriodicCoefficientInterface`, `Side24.CoefficientEnclosure`, `Side24.ReferenceComparison` | `specified` | See row side24-coefficient: the enclosure is stated for any object satisfying PeriodicCoefficientInterface and is not proved; the "evaluates_eq_15_2" edge to the parent is represented only by the interface field that takes (15.2) … | As for row side24-coefficient. | +| `math.rn-count-interface` | `760340e9:frontiers/three_fronts_20260924/RN_COUNT_INTERFACE.md` — Theorem N | — | 5 packet statements + 5 proof-packet theorems (`proved`): `RN.HolderCountBoundN1`, `RN.HolderConsequenceN2`, `RN.ConditionalMeanIdentityN3`, … (+4 more) …, proof:`RNProbability.holderConsequenceN2` (proved), proof:`RNProbability.uniformCounterexampleN4` (proved), proof:`RNProbability.exponentialTailLayerCakeN5` (proved) | `none` | 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/tested-merge-c4c66bb8… (PR head 00d2ac6e, base b2d70d77…)) … | As for row rn-count-interface. | +| `math.rn-fixed-remote-window` | `760340e9:frontiers/remote_window_20260924/PROOF.md` — Theorem A | — | `RN.PinnedLawInterface`, `RN.FixedRemoteMeanMeasureA2`, `RN.FixedRemoteCountBoundA3` | `specified` | See row rn-fixed-remote-window: displays (2)-(3) stated over PinnedLawInterface, not proved; Section 6 not stated; no inhabitant of the interface. | As for row rn-fixed-remote-window. | +| `math.rn-region.fixed-remote` | `6c020d6a:frontiers/downstream_gate_20260925/GRAPH.json` — nodes.math.rn-region.fixed-remote | — | `RN.FixedRemoteMeanMeasureA2`, `RN.FixedRemoteCountBoundA3` | `specified` | The region's mathematical content is the fixed-remote Theorem A at exactly this scope, stated by A2/A3 and not proved. | As for row rn-fixed-remote-window; nothing region-specific to add. | +| `math.rn-region.mesoscopic-scaled-annulus` | `6c020d6a:reviews/d5_reconciliation_20260929/RECONCILIATION.md` — section 2 table, row D5-d (C2) | — | `RN.D5dSummedPinNeighbourhoodC2`, `RN.AnnulusBridgeAllHeight2` | `specified` | D5dSummedPinNeighbourhoodC2 states the summed pin-neighbourhood bound (all heights, scaled ball of radius R minus the pins) and AnnulusBridgeAllHeight2 the all-height fixed-annulus bridge; neither is proved, and the "covers the … | Independent reviewer: alignment of D5dSummedPinNeighbourhoodC2 with row D5-d; proof lane: none yet (the composition D5-a + D5-c at eta = 1/4 is a proof, not a statement). | +| `math.rn-region.pin-collision` | `6c020d6a:reviews/d5_reconciliation_20260929/RECONCILIATION.md` — section 2 table, rows D5-a (P2), D5-b (microdisk), D5-d (C2) | — | `RN.D5aPuncturedPinDisks`, `RN.D5bMicrodisk`, `RN.D5dSummedPinNeighbourhoodC2` | `specified` | The three row shapes are stated for any object satisfying PinnedLawInterface and are not proved; the P2 source (PUNCTURED_PIN_PROOF.md) is not pinned here, so the Props are anchored to the reconciliation's transcription of the … | Pin PUNCTURED_PIN_PROOF.md and COLLAR_PROOF.md (reviews/d5_local_collar_20260928) and re-anchor D5a/D5b/D5c to their own displays; independent reviewer: alignment of the three Props with rows D5-a … | +| `math.rn-region.intermediate-r-to-rho` | `6c020d6a:reviews/d5_reconciliation_20260929/RECONCILIATION.md` — section 2 table, row D5-e (I3/I4) | — | `RN.D5eIntermediateShellsI3I4` | `specified` | 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. | 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-mesoscopic-reduction` | `6c020d6a:frontiers/downstream_gate_20260925/GRAPH.json` — nodes.math.rn-mesoscopic-reduction | — | — | `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. | 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` | `760340e9:frontiers/full_price_20260924/PROOF.md` — Theorem F | — | 3 packet statements + 7 main theorems (`proved`) + 3 proof-packet theorems (`proved`): `P15.FullTransformedPriceBudget`, `P15.RhoStarEnclosure`, `P15.SharpnessOfRhoStar`, … (+7 more) …, proof:`P15Elementary.sharpnessOfRhoStar` (proved), proof:`P15Interpolation.rhoStarEnclosure` (proved), proof:`P15Interpolation.fullTransformedPriceBudget` (proved) | `specified` | See row p15-full-price. | As for row p15-full-price. | +| `math.p15-price-boundary` | `760340e9:frontiers/three_fronts_20260924/P15_PRICE_BOUNDARY.md` — Counterexample | — | 2 packet statements + 6 main theorems (`proved`) + 2 proof-packet theorems (`proved`): `P15.TwoCoordGeneratorPrices`, `P15.DemandOneRefutation`, main:`P15.smallest_member_block_size` (proved), … (+4 more) …, main:`P15.minimum_generator_price_exceeds_third` (proved), proof:`P15Elementary.twoCoordGeneratorPrices` (proved), proof:`P15Elementary.demandOneRefutation` (proved) | `specified` | 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 … | As for row p15-price-boundary. | +| `math.rn-selector-region-crosswalk` | `6c020d6a:frontiers/downstream_gate_20260925/GRAPH.json` — nodes.math.rn-selector-region-crosswalk | — | — | `none` | An engineering inventory, not a mathematical claim; nothing to state in Lean and nothing stated. | No Lean target. | +| `math.rn-fixed-annulus-window` | `760340e9:frontiers/rn_thin_tube_20260925/FIXED_ANNULUS_CANDIDATE.md` — Candidate theorem | — | `RN.FixedAnnulusWindowCandidateA2` | `specified` | 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. | As for row rn-fixed-annulus-window. | +| `math.rn-region.fixed-annulus-window` | `6c020d6a:frontiers/downstream_gate_20260925/GRAPH.json` — nodes.math.rn-region.fixed-annulus-window | — | `RN.FixedAnnulusWindowCandidateA2` | `specified` | The region's content is (A2) at its exact scope, stated and not proved; the coverage classification is graph bookkeeping, not a Lean statement; the superseded high-jet route (regional.fixed-annulus.high-jet-route … | As for row rn-fixed-annulus-window. | +| `math.d5-pin-neighborhood-first-moment` | `6c020d6a:reviews/d5_reconciliation_20260929/RECONCILIATION.md` — section 2 table D5-a to D5-f | — | `RN.D5aPuncturedPinDisks`, `RN.D5bMicrodisk`, `RN.D5cCollarC1`, `RN.D5dSummedPinNeighbourhoodC2`, `RN.D5eIntermediateShellsI3I4`, `RN.D5fGlobalWindowFirstMomentI5` | `specified` | The six row shapes are stated for any object satisfying PinnedLawInterface (sample space Omega, gated pin regime 0 < r < L) and are not proved. | Pin the three component proofs and re-anchor; independent reviewer: alignment of the six Props with the section 2 table (all-height versus window I_r per row, exclusion of M and S). | +| `math.d5-component.punctured-pin-proof` | `6c020d6a:reviews/d5_reconciliation_20260929/RECONCILIATION.md` — section 2 table, rows D5-a (P2) and D5-b (microdisk) | — | `RN.D5aPuncturedPinDisks`, `RN.D5bMicrodisk` | `specified` | The Props state rows D5-a and D5-b as the reconciliation transcribes P2, not P2 from its own bytes (not pinned); the slices P4, P9, P17, P20 and the continuum argument reviewed are not stated; nothing is proved. | Pin PUNCTURED_PIN_PROOF.md (SHA-256 f972e50b… (GRAPH.json fingerprint)) and anchor D5a/D5b to its own displays. | +| `math.d5-component.punctured-pin-review-111` | `6c020d6a:frontiers/downstream_gate_20260925/GRAPH.json` — nodes.math.d5-component.punctured-pin-review-111 | — | — | `none` | A review record (or its checker) is not a mathematical statement; nothing to state in Lean and nothing stated. | No Lean target. The proof it reviews is specified under its proof-component row. | +| `math.d5-component.punctured-pin-continuum-review` | `6c020d6a:frontiers/downstream_gate_20260925/GRAPH.json` — nodes.math.d5-component.punctured-pin-continuum-review | — | — | `none` | A review record (or its checker) is not a mathematical statement; nothing to state in Lean and nothing stated. | No Lean target. The proof it reviews is specified under its proof-component row. | +| `math.d5-component.punctured-pin-continuum-check` | `6c020d6a:frontiers/downstream_gate_20260925/GRAPH.json` — nodes.math.d5-component.punctured-pin-continuum-check | — | — | `none` | A review record (or its checker) is not a mathematical statement; nothing to state in Lean and nothing stated. | No Lean target. The proof it reviews is specified under its proof-component row. | +| `math.d5-component.collar-review` | `6c020d6a:frontiers/downstream_gate_20260925/GRAPH.json` — nodes.math.d5-component.collar-review | — | — | `none` | A review record (or its checker) is not a mathematical statement; nothing to state in Lean and nothing stated. | No Lean target. The proof it reviews is specified under its proof-component row. | +| `math.d5-component.annulus-review` | `6c020d6a:frontiers/downstream_gate_20260925/GRAPH.json` — nodes.math.d5-component.annulus-review | — | — | `none` | A review record (or its checker) is not a mathematical statement; nothing to state in Lean and nothing stated. | No Lean target. The proof it reviews is specified under its proof-component row. | +| `math.d5-component.i5-review-xai` | `6c020d6a:frontiers/downstream_gate_20260925/GRAPH.json` — nodes.math.d5-component.i5-review-xai | — | — | `none` | A review record (or its checker) is not a mathematical statement; nothing to state in Lean and nothing stated. | No Lean target. The proof it reviews is specified under its proof-component row. | +| `math.d5-component.i5-review-claude` | `6c020d6a:frontiers/downstream_gate_20260925/GRAPH.json` — nodes.math.d5-component.i5-review-claude | — | — | `none` | A review record (or its checker) is not a mathematical statement; nothing to state in Lean and nothing stated. | No Lean target. The proof it reviews is specified under its proof-component row. | +| `math.d5-component.offpin-second-moment-review` | `6c020d6a:frontiers/downstream_gate_20260925/GRAPH.json` — nodes.math.d5-component.offpin-second-moment-review | — | — | `none` | A review record (or its checker) is not a mathematical statement; nothing to state in Lean and nothing stated. | No Lean target. The proof it reviews is specified under its proof-component row. | +| `math.d5-component.collar-proof` | `6c020d6a:reviews/d5_reconciliation_20260929/RECONCILIATION.md` — section 2 table, row D5-c (C1) | — | `RN.D5cCollarC1` | `specified` | D5cCollarC1 states row D5-c as the reconciliation transcribes C1, not C1 from its own bytes (not pinned); the normalizer (P14) it imports and the corollary C2 are not stated separately; nothing is proved. | Pin COLLAR_PROOF.md (SHA-256 794babe0… (GRAPH.json fingerprint)) and anchor D5cCollarC1 to display (C1). | +| `math.d5-component.annulus-proof` | `760340e9:frontiers/rn_annulus_bridge_20260925/PROOF.md` — Candidate theorem | — | `RN.AnnulusBridgeAllHeight2` | `specified` | AnnulusBridgeAllHeight2 states display (2) (d = 2, fixed L, compact birth, k_- > 0, 1 < A < B, all heights) over PinnedLawInterface; not proved. | State the R1-R7 interfaces as Props; independent reviewer: alignment of AnnulusBridgeAllHeight2 with display (2), checking "all heights" and the uniformity over E and j. | +| `math.d5-component.intermediate-window-proof` | `6c020d6a:reviews/d5_reconciliation_20260929/RECONCILIATION.md` — section 2 table, rows D5-e (I3/I4) and D5-f (I5) | — | `RN.D5eIntermediateShellsI3I4`, `RN.D5fGlobalWindowFirstMomentI5` | `specified` | The Props state rows D5-e and D5-f as the reconciliation transcribes I3/I4/I5, not from the proof's own bytes (not pinned); the tiling N1 of the Claude review and the planar F+ lower bound source are not stated; nothing is proved. | Pin intermediate_window_20260928/PROOF.md (SHA-256 b3eb9456… (GRAPH.json fingerprint)) and anchor the shell displays there. | +| `math.d5-component.remote-window-proof` | `760340e9:frontiers/remote_window_20260924/PROOF.md` — Theorem A | — | `RN.FixedRemoteMeanMeasureA2`, `RN.FixedRemoteCountBoundA3` | `specified` | See rows rn-fixed-remote-window and math.rn-fixed-remote-window; the D5 consumption at rho = s_0 is a proof step, not stated. | As for row rn-fixed-remote-window. | + +#### 4.3 Open obligations (2: 1 `specified`, 1 `none`) — stated as targets where a Prop exists; nothing asserts they hold + +| Claim | Layer 0 source (commit:path) | Transcribed disposition | Lean statement(s) (module.declaration) | Formal progress | Not established | Next step | +|---|---|---|---|---|---|---| +| `math.rn-region.witness-collision` | `6c020d6a:reviews/d5_reconciliation_20260929/RECONCILIATION.md` — section 5 (open obligation: torus-wide second factorial moment with … | — | `RN.WitnessCollisionNearPinPairsTarget`, `RN.RemoteCollisionSecondFactorialD` | `specified` | 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. | 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. | +| `hist.D0-RN-UNIF-historical-predicates` | `6c020d6a:frontiers/downstream_gate_20260925/GRAPH.json` — nodes.hist.* (ENV-RESCOV, ALLCELL-FDZ-Q4, LOGQ-TAIL, SYM-Fw-jet, … | — | — | `none` | No Lean statement: the historical numerical RN all-cell / 24-jet certification predicates have no in-tree source text to anchor (their carriers are ABSENT by fingerprint) and no Prop states any of them. | None for Lean until a source text exists; recovery of the absent carriers is a custody question (reviews/d0_custody_audit_20260926), not a formalization one. | + +#### 4.4 PROOF_INDEX results (95: 6 `specified`, 89 `none`) — reviewed scoped results and the packets PROOF_INDEX lists by id only + +82 of these rows are packets that PROOF_INDEX lists by id only: their bytes are not pinned in this packet, their statement is recorded as *not extracted*, and no verdict is implied by the row's existence. They are kept as rows rather than omitted so that the register's inventory is two-way complete against PROOF_INDEX. + +| Claim | Layer 0 source (commit:path) | Transcribed disposition | Lean statement(s) (module.declaration) | Formal progress | Not established | Next step | +|---|---|---|---|---|---|---| +| `D1-THM-A` | `c3916425:imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` — Theorem A (uniform selection candidate) | — | `Lifetime.PairLawInterface`, `Lifetime.ParentUniformSelectionA` | `specified` | ParentUniformSelectionA states the shape of (1.1): existential r_* > 0, C < infinity outside the universal quantifiers over 0 < r <= r_*, b in [bLo,bHi], k in [kLo,kHi] and all frames, for the interface field p of … | Independent reviewer: alignment of ParentUniformSelectionA with (1.1) under the honesty checklist; formal lane: none until the regression law is constructed. | +| `D1-THM-B` | `c3916425:imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` — Theorem B (compact-mark density candidate) | — | `Lifetime.IsWindowPair`, `Lifetime.IsWindowElderPair`, `Lifetime.IsLifetimeDensityVersion`, `Lifetime.ParentCompactWindowDensityB` | `specified` | ParentCompactWindowDensityB states the shape of (1.2) (asymptotics of versions of nu_cand and nu_eld, c_{B,K} > 0, the O(ell^(2/3)) difference) for compact B, K of positive length; not proved. | State (11.3) as a Prop over an explicit Gaussian conditional law; independent reviewer: alignment of ParentCompactWindowDensityB with (1.2), including the positive-length requirement. | +| `D1-THM-C` | `c3916425:imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` — Theorem C (unrestricted finite-lifetime leading density candidate) | — | `Lifetime.IsUnrestrictedPair`, `Lifetime.IsUnrestrictedLeadingCoefficient`, `Lifetime.ParentUnrestrictedLeadingDensityC` | `specified` | ParentUnrestrictedLeadingDensityC states the shape of (1.3) (leading term only) with the coefficient as an abstract positive constant c in IsUnrestrictedLeadingCoefficient; not proved. | State (15.2) and (14.1) as Props; independent reviewer: alignment of ParentUnrestrictedLeadingDensityC with (1.3), in particular the exclusion of the essential global-maximum class. | +| `OA-ELDER-LOWER-DENSITY-GAP-20260928-v1` | `6c020d6a:frontiers/window_multiplicity_laws_20260928/ELDER_LOWER_AND_DENSITY_GAP.md` — Theorem E1 (direct lower bound) | — | `Lifetime.PlanarElderLowerE2`, `Lifetime.PlanarTwoSidedRateE4`, `Lifetime.PlanarDensityGapE11` | `specified` | PlanarElderLowerE2 states (E2) for d = 2 over PairLawInterface; PlanarTwoSidedRateE4 states (E4) CONDITIONALLY on the parent (1.1) as the source's Corollary E2 does; PlanarDensityGapE11 states (E11) under the same (1.1) … | Independent reviewer: record whether (E11)'s lower half should be stated without the (1.1) hypothesis (a narrower-scope verdict is the reviewer's to write); transcribe the review verdict once pinned. | +| `two-scale-s6-s21` | not pinned — TWO_SCALE_ADDENDUM.md "Candidate conclusions" (S3)-(S5), (S20)-(S21) … | — | — | `none` | No Lean statement: the addendum is not pinned here and none of (S3)-(S5), (S20)-(S21) is stated; it enters the register only as the named support of FixedAnnulusWindowCandidateA2. Does not establish uniform O(r^3) on a fixed … | Pin TWO_SCALE_ADDENDUM.md (blob 89cae3a9, 15902 B) and state (S3)-(S5) over PinnedLawInterface with the Stecconi weighted Kac-Rice input as an interface field. | +| `axial-density` | not pinned — Candidate theorem (1): p_{grad f(X) under Q_r}(0) <= C r^(-5) exp(-c … | — | — | `none` | No Lean statement: not pinned, not stated. | Pin axial_density_20260925/PROOF.md (blob a72418d7) and state (1) as a density bound over PinnedLawInterface with the conditional gradient density as an interface field. | +| `fixed-transverse-chart` | not pinned — Candidate theorem: E_(Qr^W) N_j(rE) <= C k r^3 area(E) on the chart \|v\| … | — | — | `none` | No Lean statement: not pinned, not stated. | Pin TRANSVERSE_BOUND_CANDIDATE.md (blob 024d9277) and state the chart bound as a Prop parallel to FixedAnnulusWindowCandidateA2 with the extra \|v\| >= eta restriction. | +| `CL-D5-DIMENSION-LIFT-20260929-v1` | `6c020d6a:frontiers/d5_dimension_lift_20260929/PROOF.md` — Theorem P_d (all-height punctured pin ball); Theorem C_d (compact … | — | `RN.DimensionLiftPuncturedPinBallP`, `RN.DimensionLiftCompactCollarC`, `RN.DimensionLiftIntermediateShellsI`, `RN.DimensionLiftGlobalWindowG` | `specified` | The four theorem shapes (1.2), (1.3), (1.5)-(1.6), (1.7) are stated over PinnedLawInterface for fixed d >= 2 and not proved. | Read reviews/d5_dimension_lift_erratum_20261005 and amend the four Props if the displays changed; state Corollaries F_d and M_d; independent reviewer: alignment of the four Props with (1.2)-(1.7). | +| `OA-C6-FOURIER-20260929-v1` | `6c020d6a:frontiers/c6_fourier_cutoff_20260929/PROOF.md` — Theorem F (count cap, no G_d input); Theorem W (window consequence); … | — | `RN.FourierCutoffPlanarSecondFactorialF4` | `none` | No Prop states Theorem F (the cap functional Psi_F and its stretched-exponential tail (F1)-(F2)), Theorem W in general d and p (F3), or Proposition B; only the planar consequence (F4) is stated, GIVEN the hypothesis G_2 (E N <= C … | State (F1)-(F2) with Psi_F as an interface field (a measurable functional dominating the total critical count) and (F3) for general d, p; then the claim would be `specified`. Round-4 triage … | +| `CL-C6-PALM-20260929-v1` | `6c020d6a:frontiers/c6_palm_route_20260929/PROOF.md` — Theorem Q (factorial moments, every fixed dimension); Corollary Theta; … | — | `RN.PalmRouteFactorialMomentsQ`, `RN.PalmRouteSecondFactorialTheta` | `specified` | PalmRouteFactorialMomentsQ states (1.1) (with r_* allowed to depend on q) and PalmRouteSecondFactorialTheta states (1.2) over PinnedLawInterface; not proved. | State Corollary P; independent reviewer: alignment of the two Props with (1.1)-(1.2), including whether r_* may depend on q. | +| `OA-C6-RARE-CLUSTER-20260929-v1` | `6c020d6a:frontiers/c6_rare_cluster_laws_20260929/PROOF.md` — Theorem O | — | `RN.RareClusterPoissonObstructionO`, proof:`RNCluster.rareClusterPoissonObstructionO` (proved) | `none` | Only Theorem O (3.1) is stated, for a family of laws with hypotheses (pmf, summable mean, H1, H2) on 0 < r <= r0; Theorems C (compound Poisson (4.1)), S (6.1), the replica limit (7.1), display (5.2) and the addendum (A1)-(A2) are … | State Theorems C and S and (7.1) over pmfs on N (Mathlib PMF or explicit functions N -> R); the theorem of this row (RNCluster.rareClusterPoissonObstructionO, added after PR head 12e072d6) has a … | +| `CL-D5-REMOTE-COLLISION-20260928-v1` | `6c020d6a:frontiers/remote_collision_20260928/PROOF.md` — 1. Results (Theorems C-F, Corollary D) | — | `RN.RemoteCollisionSecondFactorialD` | `none` | Only Corollary D (second factorial moment <= C r^5 \|E\| in the fixed remote region) is stated; Theorem C (ordered near-pair count), Corollaries E and F (event asymptotics, torus-wide lower bound) are not, so the packet is not … | State Theorem C and Corollaries E, F; independent (non-Anthropic) reviewer for both the source and the Props. | +| `cumulative-transfer-correction` | `6c020d6a:reviews/collision_mechanism_20260925/CUMULATIVE_TRANSFER_CORRECTION.md` — Corrected cumulative theorem | — | — | `none` | No Prop states the corrected cumulative theorem (sigma-finite (Z, lambda), alpha > -1, m > 0, ratio hypothesis h/(kappa r^m) -> 1, limit N(ell)/ell^beta -> (1/(alpha+1)) int B0 kappa^(-beta)), although its bytes are pinned. | State the corrected theorem as a def : Prop over MeasureTheory.Measure Z (an abstract measure-space statement with no Gaussian input; a natural Mathlib-lane proof target afterwards). | +| `CL-SIDE24-PFV-20260929-v1` | not pinned — frontiers/side24_periodization_20260929 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/side24_periodization_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `OA-SIDE24-REMAINDER-20260929-v1` | not pinned — coefficients/side24_remainder_20260929 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:coefficients/side24_remainder_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `CL-SIDE24-PERIODIZATION-REMAINDER-20260929-v1` | not pinned — frontiers/side24_periodization_remainder_20260929 (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/side24_periodization_remainder_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `OA-CONTACT-ANGULAR-TAIL-20260925-v1` | not pinned — reviews/contact_angular_tail_20260925 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:reviews/contact_angular_tail_20260925 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `OA-PIN-MICRO-COV-20260926-v1` | not pinned — reviews/pin_micro_covariance_20260926 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:reviews/pin_micro_covariance_20260926 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `OA-D5-MICRODISK-20260926-v1` | not pinned — reviews/d5_microdisk_20260926 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:reviews/d5_microdisk_20260926 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `D5-PIN-MICRODISK-20260927-v1` | not pinned — reviews/d5_pin_microdisk_20260927 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:reviews/d5_pin_microdisk_20260927 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `OA-BF-SIX-PIN-HESSIAN-20260926-v1` | not pinned — certificates/bf_six_pin_hessian_20260926 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:certificates/bf_six_pin_hessian_20260926 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `OA-CONTACT-KERNEL-SUBSTITUTE-20260926-v1` | not pinned — reviews/contact_kernel_substitute_20260926 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:reviews/contact_kernel_substitute_20260926 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `OA-D5-SHORT-EDGE-20260928-v1` | not pinned — reviews/d5_short_edge_20260928 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:reviews/d5_short_edge_20260928 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `CL-D5-PIN-DISK-20260928-v1` | not pinned — reviews/d5_pin_disk_all_directions_20260928 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:reviews/d5_pin_disk_all_directions_20260928 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `OA-D5-REMOTE-SINGLETON-LAW-20260928-v1` | not pinned — frontiers/remote_singleton_law_20260928 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/remote_singleton_law_20260928 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `OA-REMOTE-HEIGHT-DECOUPLING-20260928-v1` | not pinned — frontiers/remote_height_decoupling_20260928 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/remote_height_decoupling_20260928 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `OA-WINDOW-MULTIPLICITY-LOCAL` | not pinned — frontiers/window_multiplicity_laws_20260928 (C2) (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/window_multiplicity_laws_20260928 (C2) at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `OA-WINDOW-MULTIPLICITY-REMOTE` | not pinned — frontiers/window_multiplicity_laws_20260928 (C3) (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/window_multiplicity_laws_20260928 (C3) at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `OA-WINDOW-MULTIPLICITY-DISTANCE` | not pinned — frontiers/window_multiplicity_laws_20260928 (C4) (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/window_multiplicity_laws_20260928 (C4) at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `OA-WINDOW-MULTIPLICITY-HEIGHT` | not pinned — frontiers/window_multiplicity_laws_20260928 (C5) (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/window_multiplicity_laws_20260928 (C5) at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `OA-REMOTE-INVERSE-SEPARATION-20260928-v1` | not pinned — frontiers/remote_inverse_separation_20260928 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/remote_inverse_separation_20260928 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `OA-ELDER-DIMENSION-LIFT-20260928-v1` | not pinned — frontiers/elder_dimension_lift_20260928 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/elder_dimension_lift_20260928 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `CL-ELDER-LOWER-ALL-D-20260929-v1.1` | not pinned — frontiers/elder_lower_all_d_20260929 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/elder_lower_all_d_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `CL-C6-FACTORIAL-20260929-v1` | not pinned — frontiers/c6_factorial_moment_20260929 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/c6_factorial_moment_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `CL-C6-SHARPENED-20260929-v1` | not pinned — frontiers/c6_sharpened_20260929 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/c6_sharpened_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `OA-C6-COUNT-CAP-BOUNDARY-20260929-v1` | not pinned — frontiers/c6_count_cap_boundary_20260929 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/c6_count_cap_boundary_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `OA-LOCAL-CLUSTER-TIGHTNESS-20260929-v1` | not pinned — frontiers/local_cluster_tightness_20260929 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/local_cluster_tightness_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `OA-REMOTE-MIXED-INVERSE-20260929-v1` | not pinned — frontiers/remote_mixed_inverse_20260929 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/remote_mixed_inverse_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `CL-D1-UNRESTRICTED-DIFFERENCE-20260929-v3` | not pinned — frontiers/unrestricted_selection_difference_20260929 (bytes not pinned … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/unrestricted_selection_difference_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop … | +| `CL-C7-TOTAL-BOUNDED-20260929-v1.2` | not pinned — frontiers/c7_total_bounded_20260929 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/c7_total_bounded_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `OA-C7-ZERO-GAP-LIMIT-20260929-v1` | not pinned — frontiers/c7_zero_gap_limit_20260929 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/c7_zero_gap_limit_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `OA-SARD-ROBUST-CHARTS-20260929-v1` | not pinned — frontiers/sard_g_robust_charts_20260929 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/sard_g_robust_charts_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `OA-SARD-A2-FIXED-FRAME-20260929-v2` | not pinned — frontiers/sard_g_a2_parameter_20260929/v2/A2_FIXED_FRAME.md (bytes not … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/sard_g_a2_parameter_20260929/v2/A2_FIXED_FRAME.md at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def … | +| `packet:sard_g_a2_regularity_20260929` | not pinned — frontiers/sard_g_a2_regularity_20260929 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/sard_g_a2_regularity_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:sard_g_pinned_transfer_20260929` | not pinned — frontiers/sard_g_pinned_transfer_20260929 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/sard_g_pinned_transfer_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `OA-P15-BIPARTITE-OVERLAP-20260928-v1` | not pinned — frontiers/p15_bipartite_overlap_20260928 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/p15_bipartite_overlap_20260928 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `OA-P15-TAIL-LOAD-20260928-v1` | not pinned — frontiers/p15_tail_load_20260928 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/p15_tail_load_20260928 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:planar_cubic_cluster_20260929` | not pinned — frontiers/planar_cubic_cluster_20260929 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/planar_cubic_cluster_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:c6_marked_fourier_20260929` | not pinned — frontiers/c6_marked_fourier_20260929 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/c6_marked_fourier_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:c6_cluster_law_20260929` | not pinned — frontiers/c6_cluster_law_20260929 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/c6_cluster_law_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:cluster_exponential_weight_20260930` | not pinned — frontiers/cluster_exponential_weight_20260930 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/cluster_exponential_weight_20260930 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:spectral_cluster_closure_20260929` | not pinned — frontiers/spectral_cluster_closure_20260929 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/spectral_cluster_closure_20260929 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:lifetime_moment_boundary_20260930` | not pinned — frontiers/lifetime_moment_boundary_20260930 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/lifetime_moment_boundary_20260930 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:radial_rate_20260930` | not pinned — frontiers/radial_rate_20260930 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/radial_rate_20260930 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:extreme_cluster_sampling_20260930` | not pinned — frontiers/extreme_cluster_sampling_20260930 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/extreme_cluster_sampling_20260930 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:fixed_r_inverse_lifetime_20260930` | not pinned — frontiers/fixed_r_inverse_lifetime_20260930 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/fixed_r_inverse_lifetime_20260930 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:local_elder_geometry_20260930` | not pinned — frontiers/local_elder_geometry_20260930 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/local_elder_geometry_20260930 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:concave_fibre_elder_20260930` | not pinned — frontiers/concave_fibre_elder_20260930 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/concave_fibre_elder_20260930 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:elder_partner_extremes_20260930` | not pinned — frontiers/elder_partner_extremes_20260930 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/elder_partner_extremes_20260930 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:remainder_vanishing_20260930` | not pinned — frontiers/remainder_vanishing_20260930 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/remainder_vanishing_20260930 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:elder_selected_extremes_20260930` | not pinned — frontiers/elder_selected_extremes_20260930 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/elder_selected_extremes_20260930 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:remainder_rate_20260930` | not pinned — frontiers/remainder_rate_20260930 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/remainder_rate_20260930 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:far_elder_rate_20260930` | not pinned — frontiers/far_elder_rate_20260930 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/far_elder_rate_20260930 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:short_bar_endpoint_law_20261001` | not pinned — frontiers/short_bar_endpoint_law_20261001 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/short_bar_endpoint_law_20261001 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:c2_finite_jet_transfer_20261001` | not pinned — frontiers/c2_finite_jet_transfer_20261001 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/c2_finite_jet_transfer_20261001 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:cusp_second_order_20261001` | not pinned — frontiers/cusp_second_order_20261001 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/cusp_second_order_20261001 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:candidate_third_order_20261001` | not pinned — frontiers/candidate_third_order_20261001 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/candidate_third_order_20261001 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:elder_third_order_20261001` | not pinned — frontiers/elder_third_order_20261001 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/elder_third_order_20261001 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:third_order_rate_20261001` | not pinned — frontiers/third_order_rate_20261001 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/third_order_rate_20261001 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:elder_cusp_parity_20261002` | not pinned — frontiers/elder_cusp_parity_20261002 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/elder_cusp_parity_20261002 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:separated_fold_multiplicity_20261002` | not pinned — frontiers/separated_fold_multiplicity_20261002 (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/separated_fold_multiplicity_20261002 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:subpin_collision_20261002` | not pinned — frontiers/subpin_collision_20261002 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/subpin_collision_20261002 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:soft_rejected_pairs_20261002` | not pinned — frontiers/soft_rejected_pairs_20261002 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/soft_rejected_pairs_20261002 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:soft_fold_limit_20261002` | not pinned — frontiers/soft_fold_limit_20261002 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/soft_fold_limit_20261002 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:soft_closed_form_20261002` | not pinned — frontiers/soft_closed_form_20261002 (bytes not pinned in this packet; … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/soft_closed_form_20261002 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:cusp_torus_transfer_20261001` | not pinned — frontiers/cusp_torus_transfer_20261001 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/cusp_torus_transfer_20261001 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is warranted. | +| `packet:moving_remote_collision_20261003` | not pinned — frontiers/moving_remote_collision_20261003 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/moving_remote_collision_20261003 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:ordinary_short_bar_occurrence_20261001` | not pinned — frontiers/ordinary_short_bar_occurrence_20261001 (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/ordinary_short_bar_occurrence_20261001 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:replacement_bar_occurrence_20261001` | not pinned — frontiers/replacement_bar_occurrence_20261001 (bytes not pinned in this … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/replacement_bar_occurrence_20261001 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:strict_unique_replacement_coefficient_20261003` | not pinned — frontiers/strict_unique_replacement_coefficient_20261003 (bytes not … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/strict_unique_replacement_coefficient_20261003 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def … | +| `packet:unique_replacement_bar_intensity_20261001` | not pinned — frontiers/unique_replacement_bar_intensity_20261001 (bytes not pinned … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/unique_replacement_bar_intensity_20261001 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:planar_rejected_endpoint_margin_20261003/A4` | not pinned — frontiers/planar_rejected_endpoint_margin_20261003/A4 (bytes not pinned … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/planar_rejected_endpoint_margin_20261003/A4 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop … | +| `packet:planar_soft_layer_chain_20261003/C91` | not pinned — frontiers/planar_soft_layer_chain_20261003/C91 (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/planar_soft_layer_chain_20261003/C91 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:planar_soft_layer_chain_20261003/C92` | not pinned — frontiers/planar_soft_layer_chain_20261003/C92 (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/planar_soft_layer_chain_20261003/C92 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:planar_soft_layer_chain_20261003/C93` | not pinned — frontiers/planar_soft_layer_chain_20261003/C93 (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/planar_soft_layer_chain_20261003/C93 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:planar_soft_layer_chain_20261003/C94` | not pinned — frontiers/planar_soft_layer_chain_20261003/C94 (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/planar_soft_layer_chain_20261003/C94 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:planar_soft_layer_chain_20261003/C95` | not pinned — frontiers/planar_soft_layer_chain_20261003/C95 (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/planar_soft_layer_chain_20261003/C95 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:planar_soft_layer_chain_20261003/C96` | not pinned — frontiers/planar_soft_layer_chain_20261003/C96 (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/planar_soft_layer_chain_20261003/C96 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:planar_soft_layer_chain_20261003/C97` | not pinned — frontiers/planar_soft_layer_chain_20261003/C97 (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/planar_soft_layer_chain_20261003/C97 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:planar_soft_layer_chain_20261003/C98` | not pinned — frontiers/planar_soft_layer_chain_20261003/C98 (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/planar_soft_layer_chain_20261003/C98 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:planar_soft_layer_chain_20261003/C99` | not pinned — frontiers/planar_soft_layer_chain_20261003/C99 (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/planar_soft_layer_chain_20261003/C99 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:planar_soft_layer_chain_20261003/C101` | not pinned — frontiers/planar_soft_layer_chain_20261003/C101 (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/planar_soft_layer_chain_20261003/C101 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:planar_soft_layer_chain_20261003/C102` | not pinned — frontiers/planar_soft_layer_chain_20261003/C102 (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/planar_soft_layer_chain_20261003/C102 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:planar_soft_layer_chain_20261003/C103` | not pinned — frontiers/planar_soft_layer_chain_20261003/C103 (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/planar_soft_layer_chain_20261003/C103 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | +| `packet:planar_soft_layer_chain_20261003/C124` | not pinned — frontiers/planar_soft_layer_chain_20261003/C124 (bytes not pinned in … | — | — | `none` | Statement not extracted in this programme: the packet was inventoried by id only, its bytes are not pinned here and nothing about it is stated in Lean. | Read Math-:frontiers/planar_soft_layer_chain_20261003/C124 at 6c020d6a, pin the bytes under sources/, extract the headline statement and its review disposition, and decide whether a def : Prop is … | + +#### 4.5 Existing Lean packages (7: 7 `none`) — their theorems are not Props stating a research claim of this register + +| Claim | Layer 0 source (commit:path) | Transcribed disposition | Lean statement(s) (module.declaration) | Formal progress | Not established | Next step | +|---|---|---|---|---|---|---| +| `lean:main-formal-UniversalLaw` | `760340e9:coefficients/side24_v1/ENCLOSURE.json` — ENCLOSURE.json (the four Endpoints targets anchor here; the other 55 … | — | main:`Side24.d2_endpoints_adjacent` (proved), main:`Side24.d3_endpoints_adjacent` (proved), main:`Side24.d3_below_d2` (proved), main:`Side24.endpoints_in_unit_tenth` (proved) | `none` | The package states no research claim as a Prop, so the claim-level label is none; its 31 theorems at origin/main f6deeba7 are finite integer/cross-multiplied rational facts proved by decide (label `proved` in the manifest … | PR #358 merge is the operator's decision; until then the 28 P15 targets are on a branch, not on main. | +| `lean:math-formal-ResearchFormalCoreR1` | not pinned | — | — | `none` | The package states no research claim of this register as a Prop and none of its statements can be listed here: its bound sources (P02-LM-008 proof.md.export.txt at 22876eda, MOMENT_TAIL.md, WEIGHT_PERTURBATION.md, the D2 small-L … | Pin the Math- formal sources in a later packet revision and register the 63 targets as `proved` statements with anchors; obtain a fresh alignment record for the 63-target manifest from a lane … | +| `lean:math-companion-d2_moment_bridge_20261006` | not pinned | — | — | `none` | States no research claim of this register; its sources (Math-#302 NOTE.md section 4 / C7, #326, #328, #343 comments) are not pinned here, so no statement can be anchored and listed. | Pin the companion sources and register its theorems as `proved` statements in a later packet revision; a reviewer differing in provider, family and agent for alignment. | +| `lean:math-companion-d2_square_schur_20261006` | not pinned | — | — | `none` | States no research claim of this register; its sources (Math-#302 NOTE.md section 4 / C7, #326, #328, #343 comments) are not pinned here, so no statement can be anchored and listed. | Pin the companion sources and register its theorems as `proved` statements in a later packet revision; a reviewer differing in provider, family and agent for alignment. | +| `lean:math-companion-d2_atom_integral_20261006` | not pinned | — | — | `none` | States no research claim of this register; its sources (Math-#302 NOTE.md section 4 / C7, #326, #328, #343 comments) are not pinned here, so no statement can be anchored and listed. | Pin the companion sources and register its theorems as `proved` statements in a later packet revision; a reviewer differing in provider, family and agent for alignment. | +| `lean:math-frontier-cap_first_exit_lean_20261002` | `c3916425:imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md` — Deterministic theorem (CAP sections 1-5; one of the frontier's two … | — | — | `none` | The frontier states and kernel-checks the topological global step of D1 component III (maximin level, elder merge, elder death level, saddle cut, older peak on compact locally connected spaces, torus transport) and the analytic … | Transcribe ALIGNMENT.md row by row and register the 152 declarations as `proved` statements anchored in the pinned CAP bytes (and a pinned SP review); non-Claude delta review of v1.5-v2.6. | +| `lean:math-w3scratch-side24-proposal` | not pinned | — | — | `none` | No kernel evidence exists for this package in any workflow or committed receipt: builds and axiom reports are author-reported, box-local, in a scratch copy of formal/ with an appended lean_lib, and gate.py --execute was never … | If the proposal is adopted, register it under a lakefile and workflow in Math- first; only then could its statements enter a register with anchors and `proved` labels. | + +#### 4.6 main experiment proofs (12: 12 `none`) — prose proofs on `main`, not in the Math- registers + +| Claim | Layer 0 source (commit:path) | Transcribed disposition | Lean statement(s) (module.declaration) | Formal progress | Not established | Next step | +|---|---|---|---|---|---|---| +| `main:experiments/universality/finite_gaussian_contact` | not pinned — experiments/universality/finite_gaussian_contact/PROOF.md (bytes not … | — | — | `none` | A prose proof on main, indexed only in experiments/universality/README.md (not in PROOF_INDEX, LANDING_CLAIMS or STATUS.md, which are Math- registers); no Lean statement exists and none is stated here; its bytes are not pinned in … | Pin experiments/universality/finite_gaussian_contact/PROOF.md by SHA-256, extract the theorem and its interfaces (the five field-admission interfaces as structure fields), and state it as a def … | +| `main:experiments/universality/finite_candidate_lifetime` | not pinned — experiments/universality/finite_candidate_lifetime/PROOF.md (bytes not … | — | — | `none` | A prose proof on main, indexed only in experiments/universality/README.md (not in PROOF_INDEX, LANDING_CLAIMS or STATUS.md, which are Math- registers); no Lean statement exists and none is stated here; its bytes are not pinned in … | Pin experiments/universality/finite_candidate_lifetime/PROOF.md by SHA-256, extract the theorem and its interfaces (the five field-admission interfaces as structure fields), and state it as a def … | +| `main:experiments/universality/finite_fold_chart` | not pinned — experiments/universality/finite_fold_chart/PROOF.md (bytes not pinned … | — | — | `none` | A prose proof on main, indexed only in experiments/universality/README.md (not in PROOF_INDEX, LANDING_CLAIMS or STATUS.md, which are Math- registers); no Lean statement exists and none is stated here; its bytes are not pinned in … | Pin experiments/universality/finite_fold_chart/PROOF.md by SHA-256, extract the theorem and its interfaces (the five field-admission interfaces as structure fields), and state it as a def : Prop in a … | +| `main:experiments/universality/finite_weighted_fold_window` | not pinned — experiments/universality/finite_weighted_fold_window/PROOF.md (bytes … | — | — | `none` | A prose proof on main, indexed only in experiments/universality/README.md (not in PROOF_INDEX, LANDING_CLAIMS or STATUS.md, which are Math- registers); no Lean statement exists and none is stated here; its bytes are not pinned in … | Pin experiments/universality/finite_weighted_fold_window/PROOF.md by SHA-256, extract the theorem and its interfaces (the five field-admission interfaces as structure fields), and state it as a def … | +| `main:experiments/universality/finite_contact_genericity` | not pinned — experiments/universality/finite_contact_genericity/PROOF.md (bytes not … | — | — | `none` | A prose proof on main, indexed only in experiments/universality/README.md (not in PROOF_INDEX, LANDING_CLAIMS or STATUS.md, which are Math- registers); no Lean statement exists and none is stated here; its bytes are not pinned in … | Pin experiments/universality/finite_contact_genericity/PROOF.md by SHA-256, extract the theorem and its interfaces (the five field-admission interfaces as structure fields), and state it as a def … | +| `main:experiments/universality/finite_elder_transfer` | not pinned — experiments/universality/finite_elder_transfer/PROOF.md (bytes not … | — | — | `none` | A prose proof on main, indexed only in experiments/universality/README.md (not in PROOF_INDEX, LANDING_CLAIMS or STATUS.md, which are Math- registers); no Lean statement exists and none is stated here; its bytes are not pinned in … | Pin experiments/universality/finite_elder_transfer/PROOF.md by SHA-256, extract the theorem and its interfaces (the five field-admission interfaces as structure fields), and state it as a def : Prop … | +| `main:experiments/universality/finite_h0_lifetime` | not pinned — experiments/universality/finite_h0_lifetime/PROOF.md (bytes not pinned … | — | — | `none` | A prose proof on main, indexed only in experiments/universality/README.md (not in PROOF_INDEX, LANDING_CLAIMS or STATUS.md, which are Math- registers); no Lean statement exists and none is stated here; its bytes are not pinned in … | Pin experiments/universality/finite_h0_lifetime/PROOF.md by SHA-256, extract the theorem and its interfaces (the five field-admission interfaces as structure fields), and state it as a def : Prop in … | +| `main:experiments/universality/fold_structural_universality` | not pinned — experiments/universality/fold_structural_universality/PROOF.md (bytes … | — | — | `none` | A prose proof on main, indexed only in experiments/universality/README.md (not in PROOF_INDEX, LANDING_CLAIMS or STATUS.md, which are Math- registers); no Lean statement exists and none is stated here; its bytes are not pinned in … | Pin experiments/universality/fold_structural_universality/PROOF.md by SHA-256, extract the theorem and its interfaces (the five field-admission interfaces as structure fields), and state it as a def … | +| `main:experiments/universality/periodized_gaussian_h0` | not pinned — experiments/universality/periodized_gaussian_h0/PROOF.md (bytes not … | — | — | `none` | A prose proof on main, indexed only in experiments/universality/README.md (not in PROOF_INDEX, LANDING_CLAIMS or STATUS.md, which are Math- registers); no Lean statement exists and none is stated here; its bytes are not pinned in … | Pin experiments/universality/periodized_gaussian_h0/PROOF.md by SHA-256, extract the theorem and its interfaces (the five field-admission interfaces as structure fields), and state it as a def : Prop … | +| `main:experiments/universality/iid_short_bar_process` | not pinned — experiments/universality/iid_short_bar_process/PROOF.md (bytes not … | — | — | `none` | A prose proof on main, indexed only in experiments/universality/README.md (not in PROOF_INDEX, LANDING_CLAIMS or STATUS.md, which are Math- registers); no Lean statement exists and none is stated here; its bytes are not pinned in … | Pin experiments/universality/iid_short_bar_process/PROOF.md by SHA-256, extract the theorem and its interfaces (the five field-admission interfaces as structure fields), and state it as a def : Prop … | +| `main:experiments/periodic_h0/spectral_shrinking_bins` | not pinned — experiments/periodic_h0/spectral_shrinking_bins/PROOF.md (bytes not … | — | — | `none` | A conditional prose theorem under explicit input interfaces (spectral error, spatial interpolation, exceptional expected counts); not pinned here, not stated in Lean, review pending by its own header. | Pin the bytes, extract the conditional theorem with its three input interfaces as structure fields, state as def : Prop; nonauthor review first. | +| `main:unmerged-codex-prs-330-350` | not pinned | — | — | `none` | Nothing on origin/main: these are open pull requests whose PROOF.md, guard and certificate files are not merged, not pinned and not stated; their RESULTS.md scope statuses record lean_kernel NOT_RUN and scientific_promotion … | Revisit after merge: pin, extract, state. The exact Fraction certificates of #343/#349 (which import periodic_h0 sqrt/exp/log bound helpers) would be exact_certificate rows then. | + +#### 4.7 Exact certificates (12: 12 `none`) — L2 exact-arithmetic Python evidence, not Lean + +| Claim | Layer 0 source (commit:path) | Transcribed disposition | Lean statement(s) (module.declaration) | Formal progress | Not established | Next step | +|---|---|---|---|---|---|---| +| `cert:main-periodic_h0-exact_h0_1` | not pinned — experiments/periodic_h0/results/exact_h0_1/CERTIFICATE.json scope field … | — | — | `none` | L2 exact-arithmetic evidence (Python stdlib Fraction / integer) about one finite rounded object: a Python certificate is not a kernel proof and is not Lean. | Restate the finite inequality that the Python certificate checks in exact rational arithmetic (the bounds for the fixed object) as a Lean Prop over ℚ / ℕ and prove it in a proof package (norm_num / … | +| `cert:main-periodic_h0-certificate8` | not pinned — experiments/periodic_h0/results/certificate8/CERTIFICATE.json scope … | — | — | `none` | L2 exact-arithmetic evidence (Python stdlib Fraction / integer) about one finite rounded object: a Python certificate is not a kernel proof and is not Lean. | Restate the finite inequality that the Python certificate checks in exact rational arithmetic (the bounds for the fixed object) as a Lean Prop over ℚ / ℕ and prove it in a proof package (norm_num / … | +| `cert:main-periodic_h0-nodal1` | not pinned — experiments/periodic_h0/results/nodal1/CERTIFICATE.json scope field … | — | — | `none` | L2 exact-arithmetic evidence (Python stdlib Fraction / integer) about one finite rounded object: a Python certificate is not a kernel proof and is not Lean. | Restate the finite inequality that the Python certificate checks in exact rational arithmetic (the bounds for the fixed object) as a Lean Prop over ℚ / ℕ and prove it in a proof package (norm_num / … | +| `cert:main-periodic_h0-hessian1` | not pinned — experiments/periodic_h0/results/hessian1/CERTIFICATE.json scope field … | — | — | `none` | L2 exact-arithmetic evidence (Python stdlib Fraction / integer) about one finite rounded object: a Python certificate is not a kernel proof and is not Lean. | Restate the finite inequality that the Python certificate checks in exact rational arithmetic (the bounds for the fixed object) as a Lean Prop over ℚ / ℕ and prove it in a proof package (norm_num / … | +| `cert:main-periodic_h0-gaussian_tail1` | not pinned — experiments/periodic_h0/results/gaussian_tail1/CERTIFICATE.json scope … | — | — | `none` | L2 exact-arithmetic evidence (Python stdlib Fraction / integer) about one finite rounded object: a Python certificate is not a kernel proof and is not Lean. | Restate the finite inequality that the Python certificate checks in exact rational arithmetic (the bounds for the fixed object) as a Lean Prop over ℚ / ℕ and prove it in a proof package (norm_num / … | +| `cert:main-periodic_h0-gaussian_coupling1` | not pinned — experiments/periodic_h0/results/gaussian_coupling1/CERTIFICATE.json … | — | — | `none` | L2 exact-arithmetic evidence (Python stdlib Fraction / integer) about one finite rounded object: a Python certificate is not a kernel proof and is not Lean. | Restate the finite inequality that the Python certificate checks in exact rational arithmetic (the bounds for the fixed object) as a Lean Prop over ℚ / ℕ and prove it in a proof package (norm_num / … | +| `cert:main-periodic_h0-word_polynomial1` | not pinned — experiments/periodic_h0/results/word_polynomial1/CERTIFICATE.json scope … | — | — | `none` | L2 exact-arithmetic evidence (Python stdlib Fraction / integer) about one finite rounded object: a Python certificate is not a kernel proof and is not Lean. | Restate the finite inequality that the Python certificate checks in exact rational arithmetic (the bounds for the fixed object) as a Lean Prop over ℚ / ℕ and prove it in a proof package (norm_num / … | +| `cert:main-periodic_h0-finite_count_loss1` | not pinned — experiments/periodic_h0/results/finite_count_loss1/CERTIFICATE.json … | — | — | `none` | L2 exact-arithmetic evidence (Python stdlib Fraction / integer) about one finite rounded object: a Python certificate is not a kernel proof and is not Lean. | Restate the finite inequality that the Python certificate checks in exact rational arithmetic (the bounds for the fixed object) as a Lean Prop over ℚ / ℕ and prove it in a proof package (norm_num / … | +| `cert:main-periodic_h0-count_confidence1` | not pinned — experiments/periodic_h0/results/count_confidence1/CERTIFICATE.json … | — | — | `none` | L2 exact-arithmetic evidence (Python stdlib Fraction / integer) about one finite rounded object: a Python certificate is not a kernel proof and is not Lean. | Restate the finite inequality that the Python certificate checks in exact rational arithmetic (the bounds for the fixed object) as a Lean Prop over ℚ / ℕ and prove it in a proof package (norm_num / … | +| `cert:main-universality-fold_controls` | not pinned — experiments/universality/fold_controls.py (bytes not pinned in this … | — | — | `none` | Exact Fraction toy control (L2 evidence), by its own words "no random-field admissibility or Lean claim": not a stationary random-field counterexample, not a formal kernel proof, not stated in Lean. | The exact pushforward exponent identities are elementary and could be stated and proved over ℚ in a proof package; low priority. | +| `cert:math-side24_v1-coefficient.py` | `760340e9:coefficients/side24_v1/ENCLOSURE.json` — ENCLOSURE.json ("2": lower/upper, "3": lower/upper, … | — | — | `none` | L2 exact-arithmetic evidence: a Python outward-rounding procedure is not a kernel proof, and main's 31 Side24 theorems formalize only its integer arithmetic skeleton (not the interval arithmetic, not the Gamma / pi / exp … | A proof-producing enclosure pipeline (the numerical formalizer work offer of main docs/FORMAL_VERIFICATION.md): proof-producing Gamma(7/6), pi, exp and theta-sum enclosures in Mathlib, then … | +| `cert:math-full_price-full_price.py` | `760340e9:frontiers/full_price_20260924/PROOF.md` — 0.84547981724898672067 < rho_star < 0.84547981724898672068 < 6/7. (F3) | — | — | `none` | L2 exact-arithmetic evidence (stdlib Fraction) for finite rational facts; not a kernel proof. | Prove RhoStarEnclosure in the Math- Mathlib lane via proof-producing exp/log enclosures (RhoStarBelowSixSevenths / SixSeventhsCertificate are already proved in … | + +## 5. Coverage summary + +Every number here is computed from `REGISTER.json` by the rendering script and re-asserted on each render; the +labels are the four of the lane and nothing else. A row at `none` says only that no Lean sentence for the claim +exists yet; it is not a verdict on the mathematics, and a row at `specified` is a precise question, not evidence. + +### 5.1 Counts + +| Formal-progress label | Claims (171) | Statement entries (360) | Where the label may appear | +|---|---:|---:|---| +| `none` | 138 | — | claim rows only | +| `specified` | 33 | 200 | claim rows; every statement of the packet | +| `proved` | 0 | 160 | statements of other packages, one entry per claim a theorem is listed beneath, so 160 entries are not 160 distinct theorems: the 59 `main` arithmetic theorems, 72 entries (41 of them for the 28 P15 targets at commit `91cffbb5` of main PR #358, not yet on main), and the 78 proof-packet theorems over 77 Props, 88 entries, every one of the 78 with a hosted receipt; no claim | +| `kernel-checked` | 0 | 0 | run receipts only, never in the register | + +By claim kind: + +| Kind | Rows | `specified` | `none` | +|---|---:|---:|---:| +| `landing_claim` (Landing claims) | 10 | 8 | 2 | +| `graph_node` (Downstream graph nodes) | 33 | 18 | 15 | +| `open_obligation` (Open obligations) | 2 | 1 | 1 | +| `proof_index_result` (PROOF_INDEX results) | 95 | 6 | 89 | +| `existing_lean_package` (Existing Lean packages) | 7 | 0 | 7 | +| `main_experiment_proof` (main experiment proofs) | 12 | 0 | 12 | +| `exact_certificate` (Exact certificates) | 12 | 0 | 12 | +| **all** | **171** | **33** | **138** | + +The 200 `specified` statement entries point at **153 distinct declarations** of the packet (143 `def … : Prop`, +10 interface `structure`s): `Field` 12, `Lifetime` 24, `Side24` 31, `RN` 28, `P15` 58. A declaration is listed +beneath every claim it serves, which is why there are more entries than declarations (`RN.FixedRemoteMeanMeasureA2`, +for instance, sits beneath the landing claim, the graph node, the region and the D5 component that consume Theorem A). +The modules' other 132 declarations are non-Prop definitions (`cRef`, `rhoStar`, `thetaSum`, `coverCost`, …) that the +Props are stated about; they are not register entries. The 160 `proved` entries (entries, not distinct theorems: a theorem is listed beneath every claim it serves, and the 160 entries +are 137 distinct theorems, 59 of `main` and 78 of the proof packet) are theorems of two other packages, each listed beneath a claim and never as the claim. +(a) 72 entries for the 59 theorems of the `main` core-Lean package `formal/`: 31 SIDE24 targets at origin/main +`f6deeba7` (`Ledger` 17, `ConeMoments` 10, `Endpoints` 4), whose kernel evidence is the `formal / formal-evidence` +job of `workspace-landing` run 38068951535 (event push to `main`, 2026-10-10, conclusion success; a push run checks out the pushed commit itself, +here `f6deeba7`, so it has no PR head and no synthetic merge; the reusable +`formal-verification.yml` runs inside that caller, so it does not appear under its own workflow's run list; artifact +`formal-verification-38068951535`; the last stand-alone `formal-verification.yml` run is 36356485214, an event-push run whose checked commit is +the pushed `d0c0512f` itself, 2026-09-27, and the 31 Lean texts are byte-identical between the two commits), and 28 P15 targets at commit +`91cffbb5` of main PR #358, not yet on main (`PriceBoundary` 6, `RealizedCovers` 12, `FullPrice` 10; kernel evidence the +`formal / formal-evidence` job of `workspace-landing` run 38096827443, event pull_request on main PR #358: PR head `91cffbb5`, actual +tested merge `3c02eb7d004c4b7a44f5ce7b04c2c5de94e47c0c` (the synthetic merge of that head into main at `6e11abfb…`, the receipt's `checked_commit`, +as the job's checkout log and receipt record it; its `formal/` subtree is the head's, `9357d392…`, its whole tree is not, main having moved), artifact +`formal-verification-38096827443`; listed on every P15 row whose source they anchor to, hence 41 entries); each of the 59 is a finite integer or +cross-multiplied rational identity (`decide`, one conjunct by core `Nat.pow_pos`), an arithmetic skeleton, so none +states a research claim. (b) 88 entries for the 78 theorems of the Math- proof packet +`specifications/lean_statement_proofs_20261011` (rounds 1-2 in PR #422, receipted at head `79731b96`; round 3 in PR #423, head `12e072d6`; round 4 in +PR #434 on the branch `claude/lean-statement-proofs-round4-20261011`, head `48bfcbae`; round 5 in PR #439 on the branch `claude/lean-statement-proofs-round5-20261012`, heads `c6ce0256` and `32fc9845`; round 6 in PR #441 on the branch `claude/lean-statement-proofs-round6-20261012`, heads `9e305ea5`, `4a3fbadf` and the integrator's carry `f42491e1`; the first five +landed on Math- main on 2026-10-12, cut `4afcca6a`, and #441 later that day, merge `aef861eb`, §3), each typed exactly as one of 77 registered +Props (`TriangleNeedsThree` twice): 52 of them kernel-checked by the hosted `lean-specification-proofs` run 38121713840 on PR +head `910809d6`, actual tested merge `5b198699…` (receipt `kernel-checked`, `leanchecker` PASS, axioms within the three allowed; artifact +`lean-specification-proofs-38121713840-1`; the 38 theorems of head `00d2ac6e` were first receipted by run 38116277597, actual tested merge `c4c66bb8…`, artifact +`lean-specification-proofs-38116277597-1`; run 38122386459 corroborates on head `d9b8dd33`, actual tested merge `866136cc…`, and run 38124262242 on head `79731b96`, actual +tested merge `318ff194…`, theorem_count 52). A pull_request run checks out the synthetic +merge of the PR head into its base, so each receipt's `checked_commit` is that merge commit, not the head. Bound identities: +run 38121713840, PR head `910809d6`, actual tested merge `5b198699308e0585904c21d12bf540cf2475d2f0` with base `b2d70d77876a10c365f5db5d3b6cafcf180af4e2`; run 38116277597, PR head `00d2ac6e`, actual tested merge +`c4c66bb8cb26f0cd9bc03d52bb25f1b3925b272c`, same base; run 38122386459, PR head `d9b8dd33`, actual tested merge `866136cca66b46e6dbd3186b47c9340f7e93b4f6`, same base; run 38124262242, PR head `79731b96`, +actual tested merge `318ff194eecc42c39a6b27c1d7bf03f30d6a34d9`, same base. Because the branch +contains the base, each merge's tree equals its head's tree (verified by comparing the tree hashes of the merge and the head), so the +receipted bytes are the head's bytes. The 8 theorems of the round-3 module `P15Interpolation` (`CoordinatewiseConcavity`, `FullGroundBudgetIff`, `FullGroundPriceBound`, `FullTransformedPriceBudget`, `HazardPhiBound`, `HazardProductBound`, `LocalPriceBoundFull`, `RhoStarEnclosure`) were +added after head `79731b96` in PR #423 and are kernel-checked by the hosted run 38149888699 on that PR (PR head `0dcb0016`, actual tested merge +`4363b6928c62da242952631c6b0357d096c3b252` with base `79731b961fac555f33be3cd90e379b246a5a80e3`, then the head of PR #422, on which #423 was stacked; receipt `kernel-checked`, `leanchecker` PASS, +theorem_count 60, worktree CLEAN, axioms within the three allowed; artifact `lean-specification-proofs-38149888699-1` (PR head `0dcb0016`, actual tested +merge `4363b692…`), sha256 `cdeb5c73aa03124ed0db16fa14d25fb03a8fa842457fce1e0c6565dbc5ee7ca8`); they were first receipted by run 38149524759 +on PR head `88c21058`, actual tested merge `3306233bbdeadb15d9b4b07b94cc52a80ed8caeb`, same base (same Lean bytes; artifact `lean-specification-proofs-38149524759-1`, sha256 `ddefbdcc63223d05fd8ed34addbeebc199e271525d87dead01109cddc529e836`); +both merges have the tree of their head (the base is an ancestor of the head). All 60 theorems of PR #423 head `12e072d6` are corroborated by run 38150363063 +(actual tested merge `86a6e8c876f7904cadda2d006a56f8792dc5c1af` with base `79731b961fac555f33be3cd90e379b246a5a80e3`; receipt theorem_count 60; artifact `lean-specification-proofs-38150363063-1`, sha256 `bf0e0515e2035103b07d894e2a73eeb5b542885f6da16b98c228877a5e0c1690`). +The 13 theorems of the round-4 modules `Side24Analysis` (9: `ThetaSummable`, `DerivativePairingBound`, `DerivativeBoundAtLeastOne`, `DerivativeBoundAtZero`, `ReferenceOddAndPinBlocks`, `ReferencePinDensityProduct`, `IntegrandRatioBounds`, `LatticeImageSumBound`, `DensityComparison`); `Side24Interfaces` (3: `ConeMomentD1Identity`, `TraceMoments`, `RayleighSquareLaw`); `RNCluster` (1: `RareClusterPoissonObstructionO`) were added after head `12e072d6` on the branch `claude/lean-statement-proofs-round4-20261011` +(commit `80e80243`, then stacked on #423; PR #434) and are kernel-checked by the hosted `lean-specification-proofs.yml` run 38180705952 on that PR +(PR head `48bfcbae7834c2d6f4d3123d85c69d0c5afedfa6`, actual tested merge `9833d6d9f9facc335e1a56e243c3144adefe6225` with base `12e072d614dbe6e91b66d22a2ab55cf87860d693`, then the head of PR #423, on which #434 +was stacked; event pull_request; job proof-evidence, success; receipt `kernel-checked`, `leanchecker` PASS, theorem_count 73, covered_props 72, every control +classified as intended (negative controls refused, positive controls accepted), worktree CLEAN, axioms within the three allowed; artifact +`lean-specification-proofs-38180705952-1` (PR head `48bfcbae`, actual tested merge `9833d6d9…`), 29 files, 43937 bytes, sha256 `87309efad9b804c53c543b60fdb466de1f797971417363cc2e8fa1e10eac26bd` as GitHub reports it, +the artifact bytes not having been downloaded here); the merge has the tree of its head (`1956e629…`), so the receipted bytes are the head's. That run is their first receipt and receipts all 73 theorems of that head; +the round-4 commit's local `lake build` and `#print axioms` on a worktree remain evidence about no commit. +The 2 theorems of the round-5 modules `Side24Covariance` (1: `ReferenceCovarianceLowerBound`) and `Side24ConeMoment` (1: `ConeMomentD2Identity`) were added after head `be014794` of PR #434 (its receipt-binding +commit, the base of the first-receipt and corroboration runs bound next) on the branch `claude/lean-statement-proofs-round5-20261012` (PR #439, then stacked on #434) and are +kernel-checked by the hosted `lean-specification-proofs.yml` run 38195810463 on that PR (PR head `c6ce025652f76be6e580fa24947380253450cd3b`, actual tested merge +`1320c5b217e491d301ea140e5cc25b07ff5a21b7` with base `be01479435f98f34b802258ee9ec3c3578f37169`, then the head of PR #434, on which #439 was stacked; attempt 1; event +pull_request; job proof-evidence 114638065311, success; receipt `kernel-checked`, `leanchecker` PASS, theorem_count 75, covered_props 74, every control +classified as intended (negative controls refused, positive controls accepted), worktree CLEAN, axioms within the three allowed; artifact +`lean-specification-proofs-38195810463-1` (PR head `c6ce0256`, actual tested merge `1320c5b2…`), sha256 `d8abd42be0facd4248647c3c7eb67a264bd19b9b47c6128733b5b5fc93b0a6ff` as GitHub reports it); the merge has the tree of its head. That run is their first receipt and receipts all 75 theorems +of that head. All 75 theorems of the receipt-binding successor head `32fc98455128c9903741aece5f79744ffe928d31` are corroborated by run 38198716748 (actual +tested merge `37e0f1d86ed2295e8ec0bbe72b716d934e07079c` with base `be01479435f98f34b802258ee9ec3c3578f37169`; receipt theorem_count 75). Two bounded nonauthor +reviews on PR #439, both by OpenAI/Codex agents under the same project account (organizational-independence credit 0 each), are technical records +only: review 5486104267, a source/type comparison of the two declarations with their registered Props at head `c6ce0256` (PASS; no local Lean run), and +review 5486293837, a readback of the receipt-binding delta `c6ce0256..32fc9845` (PASS); neither is an alignment review, an approval or an acceptance, and the +alignment gate stays open (`PENDING_INDEPENDENT_REVIEW`). The 3 theorems of the round-6 module `Side24Images` (3: `ImageBound`, `EntrywiseCovarianceBound`, `CovarianceOrdering`) were added after head `c6ce0256` on the branch `claude/lean-statement-proofs-round6-20261012` (PR #441, based on Math- main `a0323b94ae54a78f3d2878dc9c358dc40cdfe1dc`, +the merge of #440; not stacked on a PR) and are kernel-checked by the hosted `lean-specification-proofs.yml` run 38277458954 on that PR (PR head `9e305ea5141a1d1503560efd0e3deaf25441749e`, actual tested merge +`1376175ce5536a6ac74cb03706d18e65fdb695fa` with base `a0323b94ae54a78f3d2878dc9c358dc40cdfe1dc`; attempt 1; event pull_request; job proof-evidence 114906310832, success; receipt `kernel-checked`, `leanchecker` PASS, theorem_count 78, worktree CLEAN, +axioms within the three allowed; artifact `lean-specification-proofs-38277458954-1` (PR head `9e305ea5`, actual tested merge `1376175c…`), 47041 bytes, sha256 `1f32d60e08b0ff11b634c0413291686982f0b02e6809b9e96af2848350cbbf79` as GitHub reports it, the artifact bytes not having been +downloaded here). Unlike rounds 1-5, that tested merge does not have the head's tree: it differs from the head only outside both packets (13 files under `companions/torus_filtration_20261011/` and +`.github/workflows/torus-filtration.yml`, main's changes from PRs #428 and #440), so the receipted packet bytes are the head's while the whole tree is not. That run is their first receipt and receipts all 78 +theorems of that head. The receipt-binding successor head `4a3fbadf56c807f7f538fb42ab304ab789d77878` (register and documents only, every Lean byte unchanged) is corroborated by run 38285814238 (PR head `4a3fbadf`, actual tested merge +`0017d0ceeabed4dddcca69a9fb44c3f29a59280c`, same base; job proof-evidence 114933796783, success), and the integrator's pure current-main carry `f42491e1ac057d708d0632c636ca8cc81705f335` by run 38291534116 (PR head `f42491e1`, actual tested merge `fc139a565e34037f6c348844686a46f8008e7fe0`, same base, whose tree +`141dc082db9beba4680be08e687cb5bf972f7b8b` is the carry's and the landing tree of `aef861eb`; job proof-evidence 114952544961, success; the integrator's pre-merge readback 6130405801 reports `kernel-checked`, `leanchecker` PASS, 78 theorems over 77 Props; +artifact `lean-specification-proofs-38291534116-1` (PR head `f42491e1`, actual tested merge `fc139a56…`), sha256 `a64064499aae2aa4cf18571c82e1da9a4f2fe0872253b840c21923081a77ba99` as GitHub reports it). Three bounded nonauthor records on PR #441, all by OpenAI/Codex agents under the same project account +(organizational-independence credit 0 each), are technical records only: review 5493661142, a source/type comparison of the three declarations with their registered Props at head `9e305ea5` (PASS; no local Lean run), review 5494599128, +a readback of the receipt-binding delta `9e305ea5..4a3fbadf` (PASS), and the hosted-original byte audit 6128623199 of the run's artifacts (PASS); the readiness-triggered automatic review was NOT_RUN (usage limit, 6130327350) +and counts as nothing. None is an alignment review, an approval or an acceptance, and the alignment gate stays open (`PENDING_INDEPENDENT_REVIEW`). The packet's `check.py` in source mode +inventories the 78 theorems over 77 distinct registered Props and labels them +`proved`, the label of a committed proof package; `kernel-checked` is written by no local run. A proof-packet theorem is evidence about its Prop for the formal objects (the `RealizedData` record, the formal +downset, `coverCost` as an `sInf`, `mu`): Proposition P1, both halves of Theorem P2 ((P7) and (P8)) for prices +`c_v ≤ p_v`, the restricted budget (T1) with (T4)-(T5), the six-block union bound (P11) and transformed range, (F9), +(F13), the sharpness clause of `ρ*`, `ρ* < 6/7` with its certificate, the (N1)-(N5) parts of Theorem N and five +elementary SIDE24 identities, and, in the round-3 module `P15Interpolation` (PR #423; run 38149888699: PR head `0dcb0016`, actual tested merge `4363b692…`), the hazard interpolation chain `CoordinatewiseConcavity`, `HazardProductBound`, `HazardPhiBound`, `FullGroundPriceBound`, `FullGroundBudgetIff`, `LocalPriceBoundFull`, `FullTransformedPriceBudget` ((F6)-(F8), (F12) and Theorem F (F2) itself, through the coordinatewise concavity in place of the undisplayed (F4)-(F5)) and the 20-digit enclosure (F3) `RhoStarEnclosure` (a rational certificate with explicit series remainders, not the source's Fraction procedure), and, in the round-4 modules `Side24Analysis`, `Side24Interfaces` and `RNCluster` (branch `claude/lean-statement-proofs-round4-20261011`, PR #434; run 38180705952: PR head `48bfcbae`, actual tested merge `9833d6d9…`), +summability of the formal theta family `n ↦ exp(-‖z + 24n‖²/2)` over `Fin d → ℤ` for every `d` (`ThetaSummable`), the Section 2 derivative +bounds for `q ≤ 6` (`DerivativePairingBound`, `DerivativeBoundAtLeastOne`, `DerivativeBoundAtZero`), the lattice image sum with its bound +`1458 e^{-288}` (`LatticeImageSumBound`), the five reference block identities and the pin density product for the formal matrices +(`ReferenceOddAndPinBlocks`, `ReferencePinDensityProduct`), the integrand-ratio arithmetic for `d = 2, 3` (`IntegrandRatioBounds`), Loewner +determinant and inverse monotonicity for positive-definite real matrices (`DensityComparison`), over `ConeMomentInterface` the `m = 1` cone +moment `4/3`, the trace moments `5/3`, `25/3`, `√(3/8)` and the distribution function `P(R² ≤ a) = ∫₀^a e^{-z/2}/2 dz` (`ConeMomentD1Identity`, +`TraceMoments`, `RayleighSquareLaw`: for every inhabitant, from the law fields alone, constructing none), and Theorem O's inequality for every +family of pmfs satisfying the Prop's own antecedents (H1), (H2) (`RareClusterPoissonObstructionO`), and, in the round-5 modules `Side24Covariance` and `Side24ConeMoment` (branch `claude/lean-statement-proofs-round5-20261012`, PR #439; run 38195810463: PR head `c6ce0256`, +actual tested merge `1320c5b2…`), `C_ref ≥ I/3` in the positive-semidefinite order for the formal matrix `Cref` in every orthonormal frame, `d = 2, 3` +(`ReferenceCovarianceLowerBound`), and over `ConeMomentInterface` the `m = 2` cone moment `(1/2)[25/3 - 20/3 + 8 - 8√(3/8)]` +(`ConeMomentD2Identity`: for every inhabitant, from the law field `sxy_law` alone, constructing none), and, in the round-6 module `Side24Images` (branch `claude/lean-statement-proofs-round6-20261012`, PR #441; run 38277458954: PR head `9e305ea5`, +actual tested merge `1376175c…`), display (2)'s bound on `|D^q K_24(0) - D^q K_∞(0)|` for `q ≤ 6`, through a local, open-set version of `iteratedFDeriv_tsum` proved inside the packet from Mathlib's +first-order `hasFDerivAt_tsum_of_isPreconnected` (`ImageBound`), the Section 3 entrywise covariance bound `2E` (`EntrywiseCovarianceBound`) and display (3), the two-sided positive-semidefinite comparison of `C_24` +with `C_ref` within `ε` in every orthonormal frame, from the symmetry of `C_24` (even kernel, block-swap invariance of the analytic contractions) and Cauchy-Schwarz over at most 13 coordinates +(`CovarianceOrdering`) are proved *as the Props state them*. Every claim they sit under stays `specified` or +`none`: the register admits only those two labels at claim level, alignment of each Prop with its source paragraph +is `PENDING_INDEPENDENT_REVIEW`, and the one Prop with a theorem that the register names as stating its claim itself (`DemandOneRefutation`, row +`p15-price-boundary`; whether it says what the source paragraph says is the independent reviewer's alignment question) is recorded for the operator +and not relabelled. What has no theorem (66 of the 143 registered Props), and why, is tabulated +Prop by Prop in the statement packet's Frontier section (its README and SCOPE at `7f5f1c82`, from PR #445 with the two round-7 rows of #447; a single author's classification, moving no label): 36 vocabulary +predicates (not targets), 24 interface-blocked Props (19 `RN`, 3 `Lifetime` and the SIDE24 Props `CoefficientEnclosure`, `ReferenceComparison`; for each, a single reader's non-kernel judgement names an inhabitant of its interface that violates the conclusion, which refutes only the unrestricted universal closure for the given outer objects: for the SIDE24 Props, universal validity would force the interface empty, without an inhabitant being constructed; the `Lifetime` refutations hold for given admissible `G`, `I` and do not construct those; the `RN` refutations are read under the stated path-space, counted-set, region and window hypotheses, and the preserved RN probe supplies conditional Dirac, count and null-set reductions, not a formal countermodel receipt), 4 Mathlib-blocked +Lifetime Props and the 2 open targets `CoefficientEnclosure2`, `ReferenceComparison2` over the round-7 successor interface `PeriodicCoefficientInterface2` (36 + 24 + 4 + 2 = 66). + +**Round-4 triage** (workflow `wf_a3531fd8-891`, 2026-10-11; same account, organizational-independence credit 0; it moves no label, and its +probes are scratch files, not receipts and not in any packet). Of the 82 registered Props without a theorem after round 3, the 8 P15 +parametrised predicates were already classified by the proof packet's README and the other 74 were classified one by one: +10 PROVABLE_NOW and 5 PROVABLE_WITH_WORK, of which the 10 and 3 of the 5 (`LatticeImageSumBound`, `DensityComparison`, `RayleighSquareLaw`) are the 13 round-4 theorems above and the other 2 +(`ReferenceCovarianceLowerBound`, `ConeMomentD2Identity`; weeks), still open after round 4, are the 2 round-5 theorems above; 7 BLOCKED_MISSING_MATHLIB (`CovarianceOrdering`, `EntrywiseCovarianceBound`, `ImageBound`: no local, open-set `iteratedFDeriv_tsum` at Mathlib `d13f23b7`, since proved in round 6 by building that local version inside the proof packet, `Side24Images`, run 38277458954: PR head `9e305ea5`, actual tested merge `1376175c…` with base `a0323b94…`; +`ParentCompactWindowDensityB`, `ParentUnrestrictedLeadingDensityC`, `PlanarDensityGapE11`, `RemainderBoundedR1`: weeks); 24 BLOCKED_INTERFACE (19 `RN`, 3 `Lifetime`, 2 `Side24`), interface under-determination rather than statement +defects: each Prop is refuted at a concrete inhabitant of its interface (a Dirac law with prescribed extra critical points in 17 cases, the free +kernel field `Λ := 0`, a two-point law with a rare large cluster, the constant `p ≡ 0` or `p ≡ 1`; for `CoefficientEnclosure` and `ReferenceComparison` +the universal closure would make `PeriodicCoefficientInterface` empty, a probe-level elaboration), so no theorem of its type can exist until the +interface carries more fields; 28 PREDICATE_VOCABULARY (14 `Lifetime`, 10 `Field`, 2 `Side24`, 2 `RN`: parametrised predicates, the vocabulary of the other Props, not targets). +The proof packet README's informal reasons for its groups 'Side24 derivative bounds', 'Side24 lattice sums', 'Side24 covariance and density' and +'Side24 interface statements' were found not load-bearing and are superseded by the theorems; the per-Prop verdicts, efforts and Mathlib references +are recorded in the register's `next_step` fields (30 rows). Nothing here is a review: every verdict is author-side. + +The **33 `specified` claims** are: + +- `landing_claim` (8): `side24-coefficient`, `lifetime-remainder`, `rn-fixed-remote-window`, `rn-fixed-annulus-window`, `p15-realized-covers`, `p15-price-boundary`, `p15-price-budget-restricted`, `p15-full-price` +- `graph_node` (18): `math.uniform-matrix-cap-lifetime`, `math.lifetime-remainder`, `math.side24-coefficient`, `math.rn-fixed-remote-window`, `math.rn-region.fixed-remote`, `math.rn-region.mesoscopic-scaled-annulus`, `math.rn-region.pin-collision`, `math.rn-region.intermediate-r-to-rho`, `math.p15-full-price`, `math.p15-price-boundary`, `math.rn-fixed-annulus-window`, `math.rn-region.fixed-annulus-window`, `math.d5-pin-neighborhood-first-moment`, `math.d5-component.punctured-pin-proof`, `math.d5-component.collar-proof`, `math.d5-component.annulus-proof`, `math.d5-component.intermediate-window-proof`, `math.d5-component.remote-window-proof` +- `open_obligation` (1): `math.rn-region.witness-collision` +- `proof_index_result` (6): `D1-THM-A`, `D1-THM-B`, `D1-THM-C`, `OA-ELDER-LOWER-DENSITY-GAP-20260928-v1`, `CL-D5-DIMENSION-LIFT-20260929-v1`, `CL-C6-PALM-20260929-v1` + +Existing Lean coverage outside the packet is inventoried as seven `existing_lean_package` rows, all `none` at +claim level: `main formal/` (59 theorems, all listed as above), Math- `formal/ResearchFormalCoreR1` (63 theorems; four statement-alignment records exist for earlier +heads of that package and all are stale for the current 63-target manifest `40cb6ffc…`: main +`reviews/lean_probability_alignment_20261005` (xAI/Grok reviewer, 20 targets of Math- #272 at `27016790`, ACCEPTED), +Math- `reviews/lean_probability_alignment_20261005/alignment.json` (xAI/Grok, 29 targets, manifest `d843ba7b…`, +ACCEPTED), Math- `reviews/moment_tail_alignment_20261005/alignment.json` (xAI/Grok, 36 targets, manifest +`ddaa3707…`, ACCEPTED) and Math- `reviews/moment_generality_alignment_claude_20261005/alignment.candidate.json` +(Anthropic/Claude, 40 targets, `WITHHELD_PROPOSER_LINEAGE_UNKNOWN`); every reviewer posted under the same GitHub +account, so each record carries zero organizational-independence credit whatever the validator's provider/family/agent +check says), the three D2 companions (16 + 4 + 6 theorems), `CapFirstExit` +(152 declarations, kernel evidence via `cap-first-exit-lean.yml`, `alignment_review: NOT_CLAIMED`) and `W3Scratch` +(about 101 declarations, unregistered, built by no workflow, no kernel evidence). Their theorems are not Props stating +a claim of this register, and where their sources are not among the 23 pinned here no statement can be listed with +a verbatim anchor; the register's next step for each is to pin those sources and list the theorems as `proved` +statements in a later packet revision. + +### 5.2 What stays at `none`, and why + +Two different reasons put a row at `none`. The *mathematical* reason: the claim's principal display cannot be stated +without an object the sources leave informal, and the packet's rule is to make such objects fields of an interface +`structure`, never axioms; where even that would leave the claim itself unstated, no Prop was written. The +*inventory* reason: the bytes are not pinned in the packet (the 82 id-only PROOF_INDEX packets, the 12 `main` +experiment proofs, the 12 exact certificates, the 7 Lean packages, the graph's reading-rule and review nodes), or +there is no theorem to state (`hist.D0-RN-UNIF-historical-predicates`, whose carriers are absent by fingerprint; +`downstream-hard-gate`, an engineering control). Mapped onto the missing interfaces of +[docs/agents/LEAN_AUDIT_OWNER.md](agents/LEAN_AUDIT_OWNER.md) (paths below are relative to +`.lake/packages/mathlib/Mathlib/` in the pinned tree at `d13f23b7`, confirmed by `grep`): + +| Interface | Claim families kept at `none`, or `specified` only over an interface | What the sources leave informal | Pinned Mathlib: has / lacks | +|---|---|---|---| +| **I1 source objects** | the four D1 reading-rule component nodes (`congruence-erratum`, `section9-replacement-v1_1`, `reconciliation-record`, `marked-cylinder-cap`: the last has pinned bytes but no Prop, and `CapFirstExit`'s 152 declarations are not registered); the D5 component rows, anchored to the reconciliation's transcription because `PUNCTURED_PIN_PROOF.md`, `COLLAR_PROOF.md` and `intermediate_window/PROOF.md` are not pinned; the eight D5 review-record nodes (reviews, not theorems) | identification of SP's frame, periodic lift, cap and frontier with the interface objects; the reading rule itself (E1, Section 9 v1.1, W1, `r < L/(4√2)`) is not transcribed into any hypothesis | has: `EuclideanSpace` (Analysis/InnerProductSpace/PiL2.lean:114), `ContDiff` (Analysis/Calculus/ContDiff/Defs.lean:1068), `Matrix.PosSemidef` (LinearAlgebra/Matrix/PosDef.lean:60); lacks: nothing structural, the gap is pinning and transcription | +| **I2 persistence pairing** | `SuperlevelBarInterface` (`Field`, `Lifetime`) takes the bar and the elder pairing as fields; `IsLifetimeDensityVersion` is characterised only by an integral identity; `RemainderBoundedR1`, `PlanarElderLowerE2`/`E4`/`E11` and the three parent Props are stated over it; the `main` experiment proofs (finite H0 lifetime, elder transfer, iid short-bar process, …) and the nine `periodic_h0` certificates are `none` | the H0 superlevel persistence module, born class, elder convention, tie rules; `elder_death_level_peak` in `CapFirstExit` is component-level only | lacks: persistent homology, barcodes, any elder rule (`grep -ri persisten\|barcode` finds only metaprogramming); has: `MeasureTheory.Measure.hausdorffMeasure` (MeasureTheory/Measure/Hausdorff.lean:535) | +| **I3 source data** | `PinnedLawInterface` (`RN`) imports the pin regime `0 < r < L`, `Z_r > 0`, the weight `W_r`, the contact kernel `Λ_j`; every D5/C6/RN row (`D5a`–`D5f`, dimension lift `P`/`C`/`I`/`G`, Palm `Q`/`Θ`, Fourier `F4`, remote collision `D`, annulus bridge, fixed annulus `A2`) is `specified` only over it; no inhabitant is constructed | the regression law `Q_r`, the typed weight, the normalizer floor `Z_r ≥ z_* r²` (5.5) — stated nowhere, the boundary of the "Probability formalizer" work offer | has: `MeasureTheory.Measure.withDensity`, `IsProbabilityMeasure`; lacks: nothing structural; an inhabitant (the Dirac-mass remark in the `PinnedLawInterface` docstring) is a proof-lane target | +| **I4 probability** | `GaussianFieldInterface` (`Field`) takes Gaussianity of finite linear combinations as a field (`ProbabilityTheory.gaussianReal`, Probability/Distributions/Gaussian/Real.lean:222, with `covQuadForm`); `rn-count-interface` stays `none` because (N6)–(N7), the Gaussian numerator interface, are not stated; `two-scale-s6-s21`, `axial-density`, `fixed-transverse-chart` are `none` (not pinned) | the field's construction; the Kac–Rice representations (parent Sections 9–10, contact kernel (13), the Stecconi weighted Kac–Rice input, the Palm route's marked Kac–Rice with Hölder insertion); `Q^W(G_r^c) ≤ C r³` | has: `gaussianReal`, `multivariateGaussian` (Gaussian/Multivariate.lean:166), `IsGaussian` (Gaussian/Basic.lean:45), `IsGaussianProcess` (Gaussian/IsGaussianProcess/Def.lean:30), `IsProjectiveMeasureFamily` / `IsProjectiveLimit` (MeasureTheory/Constructions/Projective.lean:45/115), `IsKolmogorovProcess` (Probability/Process/Kolmogorov.lean); lacks: the Kolmogorov extension theorem ("not in Mathlib yet", header of Probability/BrownianMotion/GaussianProjectiveFamily.lean), a continuous- or smooth-modification theorem (no grep match), Kac–Rice, area and coarea formulas (`grep -rn 'Kac\|coarea\|area formula'` finds only Kac–Moody algebras and Rice's theorem in computability), Palm measures, point processes; change of variables exists only for injective maps (`integral_image_eq_integral_abs_det_fderiv_smul`, MeasureTheory/Function/Jacobian.lean:1213, hypothesis `InjOn f s`) | +| **Analytic coefficient** | `side24-coefficient` is `specified` only over `PeriodicCoefficientInterface` (the cone moment `D_u` is a given field; the cone-moment theorems `ConeMomentD1Identity` (round 4) and `ConeMomentD2Identity` (round 5) are about the separate `ConeMomentInterface`, hold for every inhabitant of it, construct none and do not identify its `D_1`, `D_2` with `D_u`; since round 7, Math- #447 merged `7f5f1c82`, the numbered successor interface `PeriodicCoefficientInterface2` pins the cone moment to the Gaussian cone expectation under the conditional covariance of `K_24` given the pin `V_u = H_f u = 0`, and the successor Props `CoefficientEnclosure2`, `ReferenceComparison2` restate the headline displays over it, all `specified`, no inhabitant constructed); the enclosure, the Section 5 Stirling / `Gamma(7/6)` remainder, the theta sums and `coefficient.py`'s interval arithmetic are not stated; the three SIDE24 follow-up packets (`CL-SIDE24-PFV`, `OA-SIDE24-REMAINDER`, `CL-SIDE24-PERIODIZATION-REMAINDER`) are `none` (not pinned); `cert:math-side24_v1-coefficient.py` is L2 evidence | the integration of the coefficient and a proof-producing enclosure | has: `Real.Gamma` (Analysis/SpecialFunctions/Gamma/Basic.lean:402), `Gamma_add_one` :410, `Gamma_one` :416, `Gamma_nat_eq_factorial` :422, `Gamma_pos_of_pos` :443, `Real.Gamma_one_half_eq` (Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean:307), `convexOn_log_Gamma` (Gamma/BohrMollerup.lean:111), `Gamma_strictMonoOn_Ici` :353, `Gamma_mul_Gamma_one_sub` (Gamma/Beta.lean:491); lacks: any numerical bound on `Gamma (7/6)`, interval arithmetic over ℝ (Tactic/NormNum has extensions for `Nat.log`, `Nat.sqrt`, `Real.sqrt`, none for `Real.exp`, `Real.log` or `Gamma`) | +| **Other source claims** | the 82 PROOF_INDEX packets listed by id only (statement *not extracted*; in the audit owner's words NOT ASSESSED, never inferred covered); `cumulative-transfer-correction` (pinned, no Prop); `math.rn-mesoscopic-reduction` and `math.rn-selector-region-crosswalk` (inventory nodes); `main:unmerged-codex-prs-330-350` (not on origin/main); the two P15 prize-reconnaissance packets (HOLD, listed by id only) | — | — | + +Of the 15 graph nodes at `none`, four are D1 reading-rule components, eight are D5 review records (reviews, not +theorems), two have no Prop for a different reason each (`math.rn-mesoscopic-reduction`, whose source is not pinned, +and `math.rn-selector-region-crosswalk`, an inventory node) and one is `math.rn-count-interface` (its five abstract +Props exist, the Gaussian interface does not). Of the 89 PROOF_INDEX rows at `none`, 82 are id-only packets and +seven are inventoried with their statements but without a Prop for the headline: three whose bytes are not pinned +(`two-scale-s6-s21`, `axial-density`, `fixed-transverse-chart`) and four that are pinned (`OA-C6-FOURIER-20260929-v1`, +only (F4) stated and under the hypothesis `G_2`; `OA-C6-RARE-CLUSTER-20260929-v1`, only Theorem O stated (and, in round 4, proved as the Prop states it and kernel-checked by run 38180705952: PR head `48bfcbae`, actual tested merge `9833d6d9…` with base `12e072d6…`; the row stays `none` because Theorems C, S and (7.1) are not stated); +`CL-D5-REMOTE-COLLISION-20260928-v1`, only Corollary D stated; `cumulative-transfer-correction`, no Prop). + +## 6. Roadmap from `specified` to `proved` + +Ordered by how much of each proof already exists in the pinned Mathlib tree (`d13f23b7`; every identifier below +was found by `grep` in `.lake/packages/mathlib/Mathlib/`, paths relative to that directory). The procedural frame +is the same for every step: the proof is written in a Math- Mathlib proof package (the sibling proof packet +`specifications/lean_statement_proofs_20261011`, on Math- main since 2026-10-12, whose gate requires each theorem's type to be exactly a +registered Prop applied to its own binders; the statement packet's checker refuses `theorem`); the register then lists the theorem beneath its claim with the label `proved`; +the claim's own label stays `specified` or `none`, the only claim-level labels the register admits, even where the theorem's type is +the Prop the register names as stating the claim itself (`DemandOneRefutation` for `p15-price-boundary`, the one such row; whether it +says what the source paragraph says is the independent reviewer's alignment question, `PENDING_INDEPENDENT_REVIEW`), and any +claim-level label beyond none/specified is a register-schema decision for the operator after that review, which no receipt produces; +`kernel-checked` is written only by a trusted run receipt; and an independent alignment review is a separate +dimension that none of this produces. No step below changes a Layer 0 status. + +**Step 1 — `ρ* < 6/7`, then the 20-digit enclosure of `ρ*`** (`P15.RhoStarBelowSixSevenths`, +`P15.SixSeventhsCertificate`, `P15.RhoStarEnclosure`; the next full-theorem target named in +[docs/RESEARCH_INDEX.md](RESEARCH_INDEX.md)). `rhoStar = 1 / (3 - Real.log (3 * Real.exp 1 - 2))` +(`Specifications/P15.lean:806`), so `ρ* < 6/7 ⇔ h* > 7/6 ⇔ log(3e − 2) < 11/6 ⇔ 3e − 2 < exp(11/6)`: one `Real.log` +and two `Real.exp` values. *Mathlib has*: `Real.exp_one_lt_d9` (Analysis/Complex/ExponentialBounds.lean:38), which +already gives `e < 31967/11760`; `Real.sum_le_exp_of_nonneg` (Analysis/Complex/Exponential.lean:248) for +`197/32 < Σ_{j<6} (11/6)^j/j! ≤ exp(11/6)` (the rational identity `Σ − 197/32 = 26081/933120` is a `decide` +theorem on `main`, `exp_eleven_sixths_taylor_certificate`); `Real.log_lt_log` (Analysis/SpecialFunctions/Log/Basic.lean:155), +`Real.log_exp` :75, `Real.exp_lt_exp` (Exponential.lean:312); `norm_num` for the rationals. *Mathlib lacks*: an +evaluator for `Real.exp` or `Real.log`, so the 20-digit display (F3) must be assembled by hand from the Taylor bounds +`Real.abs_log_sub_add_sum_range_le` (Log/Deriv.lean:217, `|Σ_{i 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. diff --git a/formal/ALIGNMENT.md b/formal/ALIGNMENT.md index d1c3de1b4..c68a91406 100644 --- a/formal/ALIGNMENT.md +++ b/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/327/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 | diff --git a/formal/README.md b/formal/README.md index f4dfa173f..c45460453 100644 --- a/formal/README.md +++ b/formal/README.md @@ -1,4 +1,4 @@ -# Formal package: SIDE24 arithmetic skeleton (Lean 4, core only) +# Formal package: SIDE24 and P15 arithmetic skeletons (Lean 4, core only) Scientific effect: **NONE**. This directory is the second package in the repository's formal-verification lane. The lane's contract is the @@ -22,17 +22,38 @@ guide's work-offer table this is the **first step only** of the "Numerical formalizer" offer; the exact coefficient definition and the proof-producing enclosure pipeline are not supplied. +Since 2026-10-10 the package also holds 28 targets in namespace +`UniversalLaw.P15` (three modules under `UniversalLaw/P15/`) restating the exact +finite arithmetic displayed in, or immediately implied by, four P15 price/cover notes pinned at +`Math-@760340e9…` (`frontiers/three_fronts_20260924/P15_PRICE_BOUNDARY.md`, +`…/P15_REALIZED_COVERS.md`, `frontiers/full_price_20260924/PROOF.md`, +`frontiers/price_budget_20260924/PROOF.md`, byte copies under +`sources/p15_v1/`): the demand-one counterexample's four-subset enumeration +(`mu_p(D) = 3/4`, prices `1, 2/3, 2/3, 4/9`, `4/9 > 1/3`), the 816-label +benchmark counts (`6·C(409,2) = 500616`, `15·409⁴ = 419743994415`, `815·3 < 2448`, +`2454/3 = 818`, the (P9) and (P11) evaluations), and the `rho_star` endpoint and +rational-certificate arithmetic (`…67 / …68` adjacent, `…68·7 < 6·10²⁰`, +`16/27 < 6/7`, the (T3) instance `16/27`). It does **not** cover the logarithm +inequalities those notes prove, the `rho_star` enclosure itself, `p_star`, the +probability semantics of `mu_p`, Theorems F, T1 or P2, Proposition P1, or any +prize status; [SCOPE.md](SCOPE.md#p15-exact-arithmetic-added-2026-10-10) lists +the boundary target by target. + ## Layout | Path | Role | |---|---| | `lean-toolchain`, `lakefile.toml`, `lake-manifest.json` | Pinned toolchain `leanprover/lean4:v4.34.1`; Lake package `UniversalLaw` with **no** dependencies (`dependency_revisions` is empty and the gate checks the lock agrees) | -| `UniversalLaw.lean` | Root module; imports exactly the three registered modules | +| `UniversalLaw.lean` | Root module; imports exactly the six registered modules | | `UniversalLaw/Side24/Ledger.lean` | 17 targets: pairing count, image constant, `60E < 10^-108`, Taylor partial sum of `exp(288/125)`, odd-block minors, section-4 exponent bounds, density-comparison order of magnitude | | `UniversalLaw/Side24/ConeMoments.lean` | 10 targets: conditional variances, transverse covariance thirds, `D_1 = 4/3`, `D_2 = 29/6 − √6` algebra, cube-root simplification, Hessian block eigenvalues | | `UniversalLaw/Side24/Endpoints.lean` | 4 targets: the published 20-digit endpoints as integers — adjacency, ordering, magnitude. **Not an enclosure of the coefficient.** | +| `UniversalLaw/P15/PriceBoundary.lean` | 6 targets: the demand-one counterexample on `{x,y}` enumerated as Boolean pairs — good sets, obstruction `{X}`, `mu_p(D) = 3/4` in quarters, prices `9, 6, 6, 4` in ninths, minimum `4/9 > 1/3`. **Not the log inequalities or the counterexample's conclusion.** | +| `UniversalLaw/P15/RealizedCovers.lean` | 12 targets: 816-label benchmark sizes and counts (P10), palette counts `816`, `815·3 < 2448`, `818`, the (P9) right-hand side at the displayed inputs, `⌈(ad+1)/a⌉ = d+1` instances, the (P11) rational cross-multiplied, `6/40900⁴⁰⁹ > 0` as positivity of numerator and power (core `Nat.pow_pos`). **Not Proposition P1, Theorem P2 or the union bound.** | +| `UniversalLaw/P15/FullPrice.lean` | 10 targets: the published `rho_star` endpoints as integers in `10⁻²⁰` units (adjacent, upper `< 6/7`), `16/27 < 6/7`, `n ≥ 2a+1` instances, the section-6 rational certificates (`31967/11760 < 87/32`, the degree-5 Taylor numerator of `exp(11/6)`, `197`, `7/6`), the (T3) instance `16/27` and finite instances, the explicit price `81801/3345620000 > 1/40900`. **Not an enclosure of `rho_star`, not Theorem F or T1.** | | `sources/side24_v1/` | Byte copies of the two pinned Layer 0 sources (`PROOF.md`, `ENCLOSURE.json`) | -| `manifest.json` | Evidence sidecar: package identity, toolchain, allowed axioms, SHA-256 of every bound file, pinned sources, 31 targets with verbatim informal anchors and `does_not_claim`, executable negative controls | +| `sources/p15_v1/` | Byte copies of the four pinned P15 notes at `Math-@760340e9…` | +| `manifest.json` | Evidence sidecar: package identity, toolchain, allowed axioms, SHA-256 of every bound file, pinned sources, 59 targets with verbatim informal anchors and `does_not_claim`, executable negative controls | | `SCOPE.md` | Exact coverage and "not established" per target; the review contract | | `ALIGNMENT.md` | Generated from the manifest (`--write-alignment`); never hand-edited | | `GLOSSARY.md` | Descriptive mapping of project terms to standard objects and Lean availability | @@ -50,9 +71,11 @@ enclosure pipeline are not supplied. A receipt supplied by a caller is untrusted until matched to the actual workflow run and commit. - `alignment_status` is **`PENDING_INDEPENDENT_REVIEW`**. The author is - Anthropic / Claude via a Cursor cloud agent (2026-09-27); an alignment record - from the same provider, family or agent is refused by the validator. The - manifest cannot say `ACCEPTED`. + Anthropic / Claude — via a Cursor cloud agent (2026-09-27) for the Side24 + modules and via Claude Code session `session_01Cz7WZybv8znP64SpPj6sWY` + (2026-10-10) for the P15 modules, both at zero organizational-independence + credit; an alignment record from the same provider, family or agent is refused + by the validator. The manifest cannot say `ACCEPTED`. - In the ladder of [#95](https://github.com/d6g8k5htny-coder/main/issues/95) (L0 prose … L5 proof-assistant-checked, `verification_level` separate from scientific status) a target with a trusted `kernel-checked` receipt is L5 @@ -80,7 +103,7 @@ The source-only gate prints `SOURCE_IDENTITY_PASS (not a Lean build or scientific acceptance): `. `--run-lean` removes `.lake/build`, runs `lake build`, `leanchecker` on every module, a transitive `#print axioms` audit restricted to `propext` / `Classical.choice` / `Quot.sound`, an -elaborated-type capture, and the executable negative controls: seven +elaborated-type capture, and the executable negative controls: fifteen tightened-or-wrong statements written into a scratch copy of the Lean text (each must be rejected by Lean), plus `sorry`, an indirectly imported custom axiom, and `native_decide` (each must be rejected by the axiom gate). It then @@ -103,8 +126,9 @@ keys. ## Why core Lean and not Mathlib here -Everything the arithmetic skeleton needs is `Nat`/`Int` and `decide`, which the -kernel evaluates with GMP-backed literals in well under a second. That keeps +Everything the arithmetic skeleton needs is `Nat`/`Int` and `decide` (plus core +`Nat.pow_pos` for one positivity conjunct), which the kernel evaluates with +GMP-backed literals in well under a second. That keeps this package's CI cost at seconds with no multi-gigabyte cache. The Math- pilot already carries the Mathlib dependency (revision `d13f23b723b8a846827a245b89c10fc7d3f11612`, same Lean `v4.34.1`); any statement diff --git a/formal/REVIEW_LANE.md b/formal/REVIEW_LANE.md index 16eeb6d91..9ebe65bd2 100644 --- a/formal/REVIEW_LANE.md +++ b/formal/REVIEW_LANE.md @@ -11,19 +11,27 @@ boundary") and is restated for this package in ## Who may review Anyone whose provider, family **and** agent all differ from the author's -(`Anthropic` / `Claude` / Cursor cloud agent, 2026-09-27). The validator refuses -a record where any of the three coincides, case-insensitively. Same-provider +(`Anthropic` / `Claude` / the `author.agent` string of `manifest.json`: a +Cursor cloud agent on 2026-09-27 for the Side24 modules and Claude Code session +`session_01Cz7WZybv8znP64SpPj6sWY` on 2026-10-10 for the P15 modules). The validator refuses +a record where any of the three coincides, case-insensitively. The `agent` check +is an exact (trimmed, case-folded) string comparison against the single +`author.agent` string, which names both agents; a reviewer's `agent` must be +neither of the two agents named in it, not merely different from the combined +string, and the validator cannot see that distinction on its own — the +integrator checks it by hand and should re-check it when main #315 lands. +Same-provider reviewers earn zero organizational-independence credit whatever they write; this is the repository's existing rule and it applies to Lean text as to prose. ## What the reviewer does Read the exact current head first; a changed source, scope, toolchain or -manifest stales any earlier record. Then, for each of the 31 targets in +manifest stales any earlier record. Then, for each of the 59 targets in `manifest.json`: 1. Locate the `informal_anchor` in the pinned local source copy under - `sources/side24_v1/` and read its context. + `sources/side24_v1/` or `sources/p15_v1/` and read its context. 2. Read the Lean **statement** (not the proof) and its docstring. Decide whether it is the informal statement at the scope stated in `SCOPE.md`: same constants, same quantifiers, same direction of inequality, same @@ -56,7 +64,7 @@ Two files under `reviews/`, named `_.md` and `.json`: the intended outcome. `manifest_sha256` is the SHA-256 of `formal/manifest.json` at the reviewed commit; `scope_sha256` is the hash of `formal/SCOPE.md` recorded in the manifest's `files`. `targets` is exactly - the 31 manifest target names. `evidence` points to the committed Markdown + the 59 manifest target names. `evidence` points to the committed Markdown record by repository, 40-character commit, path and SHA-256. Validate: `python3 tools/formal_gate_check.py --alignment formal/reviews/.json`. @@ -81,8 +89,10 @@ hash, new `--run-lean` receipt) or fix the anchor, then re-review. ## Current state -All 31 targets: authored by Anthropic / Claude via a Cursor cloud agent on -2026-09-27; `proved` at source; `kernel-checked` only in the receipt of a +All 59 targets: authored by Anthropic / Claude (31 Side24 targets via a Cursor +cloud agent on 2026-09-27; 28 P15 targets via Claude Code session +`session_01Cz7WZybv8znP64SpPj6sWY` on 2026-10-10, organizational-independence +credit 0); `proved` at source; `kernel-checked` only in the receipt of a trusted run; alignment `PENDING_INDEPENDENT_REVIEW`. No record other than the template exists. Record actual pickup in [work item #95](https://github.com/d6g8k5htny-coder/main/issues/95) so two diff --git a/formal/SCOPE.md b/formal/SCOPE.md index dea7de288..81d768cd2 100644 --- a/formal/SCOPE.md +++ b/formal/SCOPE.md @@ -1,15 +1,20 @@ -# Exact formal scope and alignment review — SIDE24 arithmetic skeleton +# Exact formal scope and alignment review — SIDE24 and P15 arithmetic skeletons -Scientific effect: NONE. This package offers 31 exact integer statements that are -the arithmetic skeleton of the SIDE24 coefficient note, `Math-` commit +Scientific effect: NONE. This package offers 59 exact integer statements. Thirty-one +(namespace `UniversalLaw.Side24`) are the arithmetic skeleton of the SIDE24 +coefficient note; twenty-eight (namespace `UniversalLaw.P15`, added 2026-10-10) +are the exact finite arithmetic displayed in four P15 price/cover notes and are +scoped in the section [P15 exact arithmetic](#p15-exact-arithmetic-added-2026-10-10) +below. The SIDE24 note is `Math-` commit `9d7b6802424fb4715b31999066aafca8ee2f3cca`, `coefficients/side24_v1/PROOF.md` (10,272 bytes, SHA-256 `c06daccc4ba4b9168522b9888b76a7d599934fc3b91bd753ee5d492262917769`), and of its published `ENCLOSURE.json` (1,090 bytes, SHA-256 `72b6cd92d31394cdaf5da8919a5d548e902228af1f095cc184158a71d8287811`). Both sources -are preserved byte-identically under `sources/side24_v1/`. Core Lean has no -rational type, so each rational identity is stated as the equivalent -cross-multiplied integer identity; the docstring gives the rational form and the -independent alignment review must check that the two agree. +are preserved byte-identically under `sources/side24_v1/`. Core Lean's `Rat` is +not kernel-decidable by `decide` (its `DecidableEq` instance does not reduce), so +each rational identity is stated as the equivalent cross-multiplied identity over +`Nat`; the docstring gives the rational form and the independent alignment +review must check that the two agree. This package addresses the **first step only** of the "Numerical formalizer" work offer in [docs/FORMAL_VERIFICATION.md](../docs/FORMAL_VERIFICATION.md). It does @@ -43,22 +48,85 @@ or `log` bounds, the Stirling remainder, Gaussian conditioning, the cone integrals, the parent lifetime theorem, elder selection or Kac–Rice. The Layer 0 status of D3 in [STATUS.md](../STATUS.md) is unchanged by anything here. +## P15 exact arithmetic (added 2026-10-10) + +Scientific effect: NONE. Twenty-eight targets in namespace `UniversalLaw.P15` +(modules `UniversalLaw/P15/PriceBoundary.lean`, `RealizedCovers.lean`, +`FullPrice.lean`) restate, as cross-multiplied integer facts proved by `decide` +(one positivity conjunct by core `Nat.pow_pos`), the exact finite arithmetic that +four P15 notes display or immediately imply. Four conjuncts — `1·1 + 1 = 2`, +`3 + 1 = 4`, `16·10²⁰ < 27·(lower endpoint)`, `3·6 − 11 = 7` — are not displayed +in the registered source and are marked as such in their rows and docstrings. +All four notes are pinned at +`Math-` commit `760340e921ac4ceda296b8118da936f1133e956e` and preserved +byte-identically under `sources/p15_v1/`: + +| Source id | Original path | Bytes | SHA-256 | +|---|---|---|---| +| `p15-price-boundary` | `frontiers/three_fronts_20260924/P15_PRICE_BOUNDARY.md` | 2,266 | `498af650ef7139c39d2630561dbfd0822c495ce6308a6cac8b767aefe0c2a40b` | +| `p15-realized-covers` | `frontiers/three_fronts_20260924/P15_REALIZED_COVERS.md` | 11,467 | `c0dbb821fb57b685a20cc321e4074456f39a9697f3104afd1f728e4732179bb9` | +| `p15-full-price` | `frontiers/full_price_20260924/PROOF.md` | 11,352 | `87521901ca8e5405b4d1e47f1deb1cd0326affbd6f5967b53c4178590da993f9` | +| `p15-price-budget` | `frontiers/price_budget_20260924/PROOF.md` | 7,935 | `3b79d2de60d77df9dd0d81cea60935d3dbceeb26fcf2d38d62667a425180a535` | + +The notes' author is OpenAI / ChatGPT; each carries its own disposition +("author-side mathematical derivation", nonauthor review open), which is +transcribed here and not re-derived. The Lean text was written by Anthropic / +Claude (Claude Code session `session_01Cz7WZybv8znP64SpPj6sWY`, 2026-10-10) at +zero organizational-independence credit. Core Lean's `Rat` is not +kernel-decidable by `decide` (its `DecidableEq` instance does not reduce), so each +rational identity is the equivalent cross-multiplied identity over `Nat`, with +the rational form in the docstring, and the independent alignment review must +check that the two agree. Binomial coefficients use the exact multiplicative recursion +`C(n,k+1) = C(n,k)(n−k)/(k+1)`, ceilings use `(a+b−1)/b`, and the two-coordinate +ground set of the counterexample is enumerated as the four Boolean pairs. + +| Targets | Exact coverage | Not established | +|---|---|---| +| `smallest_member_block_size` | `1·1 + 1 = 2`: block size of the demand-one member `a_1 = d_1 = 1`, `X = {x,y}` (the formula `n_i = a_i d_i + 1` is display (P1) of `p15-realized-covers`, not of this note) | The realized-cover family or theorem | +| `demand_one_good_sets`, `demand_one_obstruction` | Of the four subsets of `{x,y}`, the capacity-one filter keeps exactly `∅, {x}, {y}`; its complement is exactly `{X}` | The downset `D` beyond this enumeration; `I_1(D) = D` in general; cover semantics | +| `good_measure_three_quarters` | At `p_x = p_y = 1/2` the four quarter-weights total `4 = 2²` and the good sets total `3`, i.e. `mu_p(D) = 3/4` cross-multiplied | The product-measure semantics of `mu_p`; `min(1, −log mu_p(D)) = log(4/3)`; `log(4/3) < 1/3` | +| `generator_prices_ninths`, `minimum_generator_price_exceeds_third` | At `c_x = c_y = 2/3` the generator prices over `9` are `9, 6, 6, 4` (`1, 2/3, 2/3, 4/9`); their minimum is `4`; `4/9 > 1/3` as `1·9 < 4·3` | That `phi(1/2) = log 2 > 2/3` (admissibility of `c`); that the minimum over subsets of `X` is the exact optimal cover price (the set-theoretic steps); `1/3 > log(4/3)`; **the source's conclusion that the same-palette extension to `c ≤ phi(p)` is false in general** | +| `benchmark_block_and_ground_sizes`, `four_block_supports_fifteen` | `1·408 + 1 = 409`, `6·409 = 2454`, `C(6,4) = 15` | The construction (P1)–(P2), Proposition P1 | +| `minimal_forbidder_counts` | (P10) `6·C(409,2) = 500616`, `15·409⁴ = 419743994415` | That these count the minimal forbidders (Proposition P1) | +| `palette_816_from_two_label_classes`, `palette_815_fails_by_counting`, `whole_ground_chromatic_818` | `408 + 408 = 816`; `2454 − 6 = 2448`, `815·3 < 2448`, `6·408 = 2448`; `2454/3 = 818` exactly | Theorem P2 (cover iff `K ≥ K_H(d)`); that the palette satisfies (P6) and no smaller one does; that a colour class holds at most three vertices; the chromatic number of the ground set | +| `elementary_palette_formula_instances`, `macro_triangle_three_colors`, `ceil_block_over_capacity_instances` | The right-hand side of (P9) evaluated at `(b,s,d_i) = (6,3,408)`, `(6,3,409)`, `(3,1,1)`; `3 + 1 = 4` (not displayed: `s + 1 = 4` with `s = 3`); `⌈(ad+1)/a⌉ = d+1` at five `(a,d)` instances | The formula (P9) itself; that the benchmark's `K_H` is given by (P9); the general ceiling identity; the triangle's chromatic claim | +| `block_occupancy_one_percent`, `low_failure_union_bound_arithmetic`, `cover_price_numerator_and_denominator_positive` | `409·100 = 40900`; (P11) `500616/40900² + 15/100⁴ = 2449227/8180000000 < 3/10000` cross-multiplied; `10000 − 3 = 9997`; `6/40900⁴⁰⁹ > 0` as `0 < 6` and `0 < 40900⁴⁰⁹` (core `Nat.pow_pos`; the power is not evaluated) | The union bound and the independence of block occupancies; that `Q = 1 − mu_p(D)`; the price identity `6/40900⁴⁰⁹` for the six-generator cover; (P4)–(P5), (P8) | +| `rho_star_endpoints_adjacent`, `rho_star_upper_endpoint_below_six_sevenths` | The published 20-digit endpoints of (F3), as integers in `10⁻²⁰` units, are adjacent; `…68·7 < 6·10²⁰` (upper endpoint `< 6/7`) | **That `rho_star = 1/(3 − log(3e − 2))` lies between the endpoints**; `rho_star < 6/7` as a real-number statement; Theorem F (F2); the constant's optimality | +| `sixteen_twentysevenths_below_six_sevenths` | `16·7 < 6·27`; `16·10²⁰ < 27·(lower endpoint)` (not displayed; implied by the displayed numbers) | Theorem (T1) or its domain `p_v ≤ 1/4`; that `16/27 < rho_star` as a real-number statement | +| `minimal_block_size_instances` | `1·2 + 1 = 3`; `2a + 1 ≤ ad + 1` at five `(a,d)` with `d ≥ 2` | The implication for all `a ≥ 1, d ≥ 2`; the binomial tail comparison (F9)–(F11); the sharpness argument | +| `e_rational_bounds_ordering`, `exp_eleven_sixths_taylor_certificate`, `h_star_rational_certificate_constants` | `31967·32 < 87·11760`; `87/32 − 31967/11760 = 11/23520` cross-multiplied; degree-5 Taylor numerator of `exp(11/6)` equals `197·29160 + 26081` over `933120 = 6⁵·5! = 32·29160`; `3·87 − 2·32 = 197`; `3·6 − 11 = 7` (not displayed; the arithmetic behind `h_star > 7/6`) | `e < 31967/11760`, `e < 87/32`, that the partial sum is below `exp(11/6)`, `197/32 < exp(11/6)`, monotonicity of `log`, `h_star > 7/6`, `rho_star < 6/7` as real-number statements | +| `t3_ratio_at_minimal_block`, `t3_bound_finite_instances` | (T3) at `a = 1, n = 3`: `4³ = 4¹·4²`, `4² = 16`, `3³ = 27`, `(4/3)(4/9)¹ = 16/27`; `4^(a+1)·27 ≤ 16·3ⁿ` at seven `(a,n)` with `n ≥ 2a+1`; `4·4ᵃ·27 ≤ 16·3·9ᵃ` for `a = 1..6` | The ratio chain (T3) in general (it uses (T2), `p_v ≤ 1/4` and independence); (T2); Theorem (T1) | +| `explicit_rational_price_above_p` | `2·40900 + 1 = 81801`, `2·40900² = 3345620000`, `3345620000 < 81801·40900` (i.e. `c = p + p²/2 = 81801/3345620000 > p` at `p = 1/40900`) | Admissibility `c ≤ phi(p)`; the price bound (T7); validity of the 816-label cover at these prices | + +None of these targets is Theorem F (F2), Theorem (T1), Theorem P2, Proposition +P1, the enclosure (F3) of `rho_star`, any inequality involving `log`, `exp` or +`e`, the probability semantics of `mu_p`, the union bound (P11), `p_star`, the +P15-B amalgamation, or any prize status; every prize claim in this repository +carries `original_prize_closed: false` and nothing here touches it. No Lean +`Prop` stating any of those research claims exists in this package, so their +formal-progress label stays `none`; the targets above are arithmetic +sub-identities whose own label is `proved` at source and `kernel-checked` only +in a trusted receipt. The Layer 0 dispositions of the four notes are unchanged. + ## Review contract Identical to the Math- lane contract. The manifest is an evidence sidecar, not a scientific register. A trusted successful `--run-lean` execution establishes -kernel evidence only for these 31 target declarations and their displayed +kernel evidence only for these 59 target declarations and their displayed hypotheses, relative to Lean's kernel, standard foundations and the pinned toolchain. Independent review must compare each Lean statement (and each cross-multiplication) to this scope note and the informal anchor in `manifest.json`. Review author, provider, family and agent must be explicit and -differ from the author's (`Anthropic` / `Claude` / Cursor cloud agent). Validate +differ from the author's (`Anthropic` / `Claude` / the `author.agent` string of +`manifest.json`, which names the Cursor cloud agent of 2026-09-27 for the Side24 +modules and Claude Code session `session_01Cz7WZybv8znP64SpPj6sWY` of 2026-10-10 +for the P15 modules). Validate a record with `python3 tools/formal_gate_check.py --alignment review.json`; the validator checks structure, digests, coverage and lineage, and does not authenticate that a review happened. The record contains disposition `ACCEPTED`, `manifest_sha256`, `scope_sha256` -(the hash of this file as bound in the manifest), exactly the 31 targets, +(the hash of this file as bound in the manifest), exactly the 59 targets, author/reviewer objects with provider/family/agent, and evidence repository/path/40-character commit/sha256. At publication no independent alignment review is claimed. A fresh source, scope, toolchain or manifest digest diff --git a/formal/UniversalLaw.lean b/formal/UniversalLaw.lean index ff12fa0eb..4d24df02e 100644 --- a/formal/UniversalLaw.lean +++ b/formal/UniversalLaw.lean @@ -1,9 +1,12 @@ import UniversalLaw.Side24.Ledger import UniversalLaw.Side24.ConeMoments import UniversalLaw.Side24.Endpoints +import UniversalLaw.P15.PriceBoundary +import UniversalLaw.P15.RealizedCovers +import UniversalLaw.P15.FullPrice /-! -# Universal Law — main-side formal package (SIDE24 arithmetic skeleton) +# Universal Law — main-side formal package (SIDE24 and P15 arithmetic skeletons) Root module. `tools/formal_gate_check.py` requires this file to import exactly the modules registered in `formal/manifest.json`, derives the target inventory diff --git a/formal/UniversalLaw/P15/FullPrice.lean b/formal/UniversalLaw/P15/FullPrice.lean new file mode 100644 index 000000000..0cdea915d --- /dev/null +++ b/formal/UniversalLaw/P15/FullPrice.lean @@ -0,0 +1,125 @@ +/-! +# P15 full transformed-price budget — endpoint and certificate arithmetic + +Informal sources (Layer 0, byte-pinned), both at `Math-` commit +`760340e921ac4ceda296b8118da936f1133e956e`: + +* `frontiers/full_price_20260924/PROOF.md`, 11352 bytes, SHA-256 + `87521901ca8e5405b4d1e47f1deb1cd0326affbd6f5967b53c4178590da993f9` + (object P15-FULL-TRANSFORMED-PRICE-20260924-v1, author OpenAI / ChatGPT): + the published 20-digit endpoints of `rho_star` in display (F3), the comparison + with `6/7` and `16/27`, the block-size inequality `n ≥ 2a + 1`, and the short + rational certificates of section 6. +* `frontiers/price_budget_20260924/PROOF.md`, 7935 bytes, SHA-256 + `3b79d2de60d77df9dd0d81cea60935d3dbceeb26fcf2d38d62667a425180a535` + (object P15-TRANSFORMED-PRICE-BUDGET-20260924-v1, author OpenAI / ChatGPT): + the ratio chain (T3) at its equality instance `a = 1, n = 3` and at finitely + many further instances, and the explicit rational price of section 4. + +The endpoints are transcribed as natural numbers in units of `10^-20`. Core +Lean's `Rat` is not kernel-decidable by `decide` (its `DecidableEq` instance does +not reduce), so every rational statement is the equivalent cross-multiplied +statement over `Nat` with the rational form in the docstring. + +What this module does **not** establish: that `rho_star = 1/(3 − log(3e − 2))` +lies between the published endpoints (that needs `Real.exp`, `Real.log` and an +enclosure, which belong to the Mathlib lane), `e < 87/32`, `197/32 < exp(11/6)`, +`h_star > 7/6`, `rho_star < 6/7` as a statement about the real number, the +hazard interpolation lemma (F4)–(F8), the binomial tail comparison (F9)–(F11), +Theorem F (F2), Theorem (T1), the inequalities (T2) and (T3) in general, the +admissibility `c <= phi(p)` of the explicit price, `p_star = 1 − exp(−1)`, or any +prize status. Nothing here changes any Layer 0 status. +-/ + +namespace UniversalLaw.P15 + +/-- `0.84547981724898672067` and `0.84547981724898672068` in units of `10^-20`: +the published lower and upper endpoints of display (F3). -/ +def rhoLower : Nat := 84547981724898672067 +def rhoUpper : Nat := 84547981724898672068 + +/-- Factorial on `Nat`; kept local so that the library has no dependencies. -/ +def fact : Nat → Nat + | 0 => 1 + | n + 1 => (n + 1) * fact n + +/-- Numerator of the degree-5 Taylor partial sum of `exp(11/6)` after clearing +the denominator `6^5 · 5! = 933120`: `∑_{j=0}^{5} 11^j · 6^(5-j) · 5!/j!`. -/ +def expElevenSixthsNumerator : Nat := + (List.range 6).foldl (fun acc j => acc + 11 ^ j * 6 ^ (5 - j) * (fact 5 / fact j)) 0 + +/-- Source (F3): "0.84547981724898672067 < rho_star < 0.84547981724898672068 < 6/7". +The published endpoints are distinct and adjacent on the 20-digit grid. -/ +theorem rho_star_endpoints_adjacent : rhoLower < rhoUpper ∧ rhoUpper = rhoLower + 1 := by decide + +/-- Source (F3): "< 0.84547981724898672068 < 6/7". The upper endpoint is below +`6/7`: `rhoUpper / 10^20 < 6/7 ⇔ rhoUpper · 7 < 6 · 10^20`. -/ +theorem rho_star_upper_endpoint_below_six_sevenths : rhoUpper * 7 < 6 * 10 ^ 20 := by decide + +/-- Source: "The prior probability<=1/4 theorem ... gives the stronger factor +16/27 on its smaller domain" (source: "factor16/27"). Stronger means smaller: +`16/27 < 6/7 ⇔ 16 · 7 < 6 · 27`, and `16/27` is also below the published lower +endpoint: `16/27 < rhoLower / 10^20 ⇔ 16 · 10^20 < 27 · rhoLower`. The second +comparison is not displayed in the source; it is implied by the displayed numbers. -/ +theorem sixteen_twentysevenths_below_six_sevenths : + 16 * 7 < 6 * 27 ∧ 16 * 10 ^ 20 < 27 * rhoLower := by decide + +/-- Source: "Our n=ad+1 and d>=2 imply n>=2a+1." and (section 5) "Take one block, +a=1,d=2,n=3". Checked: `1 · 2 + 1 = 3` and `2a + 1 ≤ ad + 1` at five `(a, d)` +instances with `d ≥ 2`. The general implication is not checked. -/ +theorem minimal_block_size_instances : + 1 * 2 + 1 = 3 ∧ + ∀ p, p ∈ [(1, 2), (1, 3), (2, 2), (3, 5), (4, 2)] → 2 * p.1 + 1 ≤ p.1 * p.2 + 1 := by + decide + +/-- Source (section 6): "e < 31967/11760 < 87/32, 87/32-31967/11760=11/23520." +Checked: `31967/11760 < 87/32 ⇔ 31967 · 32 < 87 · 11760`, and the difference +`87/32 − 31967/11760 = 11/23520 ⇔ (87·11760 − 31967·32) · 23520 = 11 · (32·11760)`. +The bound `e < 31967/11760` (series plus geometric tail) is not checked. -/ +theorem e_rational_bounds_ordering : + 31967 * 32 < 87 * 11760 ∧ (87 * 11760 - 31967 * 32) * 23520 = 11 * (32 * 11760) := by + decide + +/-- Source (section 6): "sum_(j=0)^5 (11/6)^j/j! -197/32=26081/933120>0". +Over the common denominator `933120 = 6^5 · 5! = 32 · 29160`: +the partial sum numerator equals `197 · 29160 + 26081`, i.e. the difference is +`26081/933120 > 0`. That the partial sum is below `exp(11/6)` is analysis. -/ +theorem exp_eleven_sixths_taylor_certificate : + 6 ^ 5 * fact 5 = 933120 ∧ 32 * 29160 = 933120 ∧ + expElevenSixthsNumerator = 197 * 29160 + 26081 ∧ 0 < 26081 := by decide + +/-- Source (section 6): "Therefore 3e-2<197/327/6 and +rho_star<6/7." The two rational constants: `3 · (87/32) − 2 = 197/32 ⇔ +3 · 87 − 2 · 32 = 197`, and `3 − 11/6 = 7/6 ⇔ 3 · 6 − 11 = 7`. The second identity +is not displayed in the source; it is the arithmetic behind `h_star > 7/6` once +`log(3e − 2) < 11/6`. The inequalities involving `e`, `exp`, `log`, `h_star` and +`rho_star` are not checked. -/ +theorem h_star_rational_certificate_constants : 3 * 87 - 2 * 32 = 197 ∧ 3 * 6 - 11 = 7 := by + decide + +/-- Source (T3, price_budget): "= (4^(a+1))/(3^n) <= (4/3)*(4/9)^a <=16/27" at the +equality instance `a = 1`, `n = 3`: `(1/4)^(n−a−1)/(3/4)^n = 4^(a+1)/3^n` needs +`4^n = 4^(n−a−1) · 4^(a+1)`, i.e. `4^3 = 4^1 · 4^2`; then `4^2 = 16`, `3^3 = 27`, +and `(4/3)(4/9)^1 = 16/27` is `4 · 4^1 = 16`, `3 · 9^1 = 27`. -/ +theorem t3_ratio_at_minimal_block : + 4 ^ 3 = 4 ^ (3 - 1 - 1) * 4 ^ (1 + 1) ∧ 4 ^ (1 + 1) = 16 ∧ 3 ^ 3 = 27 ∧ + 4 * 4 ^ 1 = 16 ∧ 3 * 9 ^ 1 = 27 := by decide + +/-- Source (T3, price_budget): "<= (4/3)*(4/9)^a <=16/27". Finite instances: +`4^(a+1)/3^n ≤ 16/27 ⇔ 4^(a+1) · 27 ≤ 16 · 3^n` at seven `(a, n)` pairs with +`n ≥ 2a + 1`, and `(4/3)(4/9)^a ≤ 16/27 ⇔ 4 · 4^a · 27 ≤ 16 · (3 · 9^a)` for +`a = 1, …, 6`. The inequalities for all `a ≥ 1`, `n ≥ 2a + 1` are not checked. -/ +theorem t3_bound_finite_instances : + (∀ p, p ∈ [(1, 3), (1, 4), (2, 5), (2, 6), (3, 7), (3, 10), (4, 9)] → + 4 ^ (p.1 + 1) * 27 ≤ 16 * 3 ^ p.2) ∧ + (∀ a, a ∈ [1, 2, 3, 4, 5, 6] → 4 * 4 ^ a * 27 ≤ 16 * (3 * 9 ^ a)) := by decide + +/-- Source (section 4, price_budget): "An explicit rational price strictly larger +than p is c=p+p^2/2=81801/3345620000." At `p = 1/40900`: +`p + p^2/2 = (2·40900 + 1)/(2·40900^2) = 81801/3345620000`, and `c > p ⇔ +81801 · 40900 > 3345620000`. Admissibility `c ≤ phi(p)` is not checked. -/ +theorem explicit_rational_price_above_p : + 2 * 40900 + 1 = 81801 ∧ 2 * 40900 ^ 2 = 3345620000 ∧ 3345620000 < 81801 * 40900 := by + decide + +end UniversalLaw.P15 diff --git a/formal/UniversalLaw/P15/PriceBoundary.lean b/formal/UniversalLaw/P15/PriceBoundary.lean new file mode 100644 index 000000000..f33f5ecb5 --- /dev/null +++ b/formal/UniversalLaw/P15/PriceBoundary.lean @@ -0,0 +1,94 @@ +/-! +# P15 demand-one price boundary — exact finite arithmetic of the counterexample + +Informal source (Layer 0, byte-pinned): `Math-` commit +`760340e921ac4ceda296b8118da936f1133e956e`, +`frontiers/three_fronts_20260924/P15_PRICE_BOUNDARY.md`, 2266 bytes, SHA-256 +`498af650ef7139c39d2630561dbfd0822c495ce6308a6cac8b767aefe0c2a40b` +(object P15-PRICE-BOUNDARY-20260924-v1, author OpenAI / ChatGPT). + +The source exhibits the smallest one-block member of the realized-cover family +(`a_1 = d_1 = 1`, `X = {x, y}`, no macro edges) with `p_x = p_y = 1/2` and +transformed prices `c_x = c_y = 2/3`, and computes `mu_p(D) = 3/4`, the four +generator costs `1, 2/3, 2/3, 4/9` and the comparison `4/9 > 1/3`. This module +restates exactly that finite arithmetic: subsets of the two-coordinate ground set +are Boolean pairs, the product measure at `p = 1/2` is carried as integer +numerators over the denominator `4`, and prices at `c = 2/3` as integer +numerators over the denominator `9`. Core Lean's `Rat` is not kernel-decidable +by `decide` (its `DecidableEq` instance does not reduce), so each rational +statement is the equivalent cross-multiplied statement over `Nat` with the +rational form in the docstring. The kernel checks the integers; the alignment +review checks that each integer statement is the stated rational one. + +What this module does **not** establish: the two logarithm inequalities the +source proves (`phi(1/2) = log 2 > 2/3` and `log(4/3) < 1/3`), the identity +`min(1, -log mu_p(D)) = log(4/3)`, the probability semantics of `mu_p` beyond +the displayed finite sum, that every cover of the obstruction `{X}` must contain +a generator inside `X`, that additional nonnegative-price generators cannot lower +the minimum, and therefore the source's conclusion that the same-palette +extension to `c <= phi(p)` is false in general. Nothing here bears on P15-B, on +Theorem F, on any prize, or on any Layer 0 status. +-/ + +namespace UniversalLaw.P15 + +/-- The ground set `X = {x, y}` of the smallest one-block member: a subset of `X` +is a pair of Booleans (`x ∈ U`, `y ∈ U`). These are its four subsets, in the +order `∅, {x}, {y}, X`. -/ +def subsets2 : List (Bool × Bool) := [(false, false), (true, false), (false, true), (true, true)] + +/-- Membership in the demand-one downset `D` on one block of capacity `a_1 = 1` +with no macro edges: at most one coordinate is present. -/ +def good (U : Bool × Bool) : Bool := !(U.1 && U.2) + +/-- Numerator of the product-measure weight of `U` at `p_x = p_y = 1/2`, over the +common denominator `2 · 2 = 4`: a present coordinate contributes the numerator of +`p = 1/2`, an absent one the numerator of `1 - p = (2 - 1)/2`; both are `1`. -/ +def weightNum (U : Bool × Bool) : Nat := (if U.1 then 1 else 2 - 1) * (if U.2 then 1 else 2 - 1) + +/-- Numerator of the generator price `∏_{v ∈ U} c_v` at `c_x = c_y = 2/3`, over +the common denominator `3 · 3 = 9`: a present coordinate contributes `2` (the +numerator of `2/3`), an absent one `3` (the empty factor `1 = 3/3`). -/ +def priceNum (U : Bool × Bool) : Nat := (if U.1 then 2 else 3) * (if U.2 then 2 else 3) + +/-- Total product-measure mass of all four subsets, in units of `1/4`. -/ +def totalMassNum : Nat := subsets2.foldl (fun acc U => acc + weightNum U) 0 + +/-- Product-measure mass of the good sets, in units of `1/4`. -/ +def goodMassNum : Nat := (subsets2.filter good).foldl (fun acc U => acc + weightNum U) 0 + +/-- Source: "Consider its smallest one-block member: a_1=d_1=1, X={x,y}, no macro +edges." The block-size formula `n_i = |X_i| = a_i d_i + 1` is not displayed in this +note; it is display (P1) of the realized-cover note (`p15-realized-covers`, +`P15_REALIZED_COVERS.md`: "n_i=|X_i|=a_i d_i+1."). Checked: at `a_1 = d_1 = 1` it +gives `2 = |{x, y}|`. -/ +theorem smallest_member_block_size : 1 * 1 + 1 = 2 := by decide + +/-- Source: "Its good sets are the empty set and singletons". Filtering the four +subsets by the capacity-one condition leaves exactly `∅`, `{x}`, `{y}`. -/ +theorem demand_one_good_sets : + subsets2.filter good = [(false, false), (true, false), (false, true)] := by decide + +/-- Source: "its one-piece obstruction is exactly {X}". The only subset outside +`D` is `X = {x, y}` itself; with `I_1(D) = D` this is `O_1(D) = {X}`. -/ +theorem demand_one_obstruction : subsets2.filter (fun U => !good U) = [(true, true)] := by decide + +/-- Source: "Nevertheless mu_p(D)=3/4". At `p_x = p_y = 1/2` every subset has +weight `1/4`; the four weights sum to `1` (`4/4`) and the three good sets to +`3/4`. Cross-multiplied: `goodMassNum / 2^2 = 3/4 ⇔ goodMassNum · 4 = 3 · 2^2`. -/ +theorem good_measure_three_quarters : totalMassNum = 2 ^ 2 ∧ goodMassNum * 4 = 3 * 2 ^ 2 := by + decide + +/-- Source: "The possible generator costs are 1, 2/3, 2/3, 4/9 for the empty set, +the two singletons, and X respectively" (the source runs "are1,2/3,2/3,4/9" +together). Over the denominator `9`: `9/9, 6/9, 6/9, 4/9`. -/ +theorem generator_prices_ninths : 3 * 3 = 9 ∧ subsets2.map priceNum = [9, 6, 6, 4] := by decide + +/-- Source: "covercost_c(O_1(D))=4/9 > 1/3 > log(4/3)". Checked here: the minimum +of the four displayed generator costs is `4/9` (numerator `4` over `9`), and +`4/9 > 1/3 ⇔ 1 · 9 < 4 · 3`. The identification of that minimum with the exact +optimal cover price, and the final comparison with `log(4/3)`, are not checked. -/ +theorem minimum_generator_price_exceeds_third : + (subsets2.map priceNum).foldl min 9 = 4 ∧ 1 * 9 < 4 * 3 := by decide + +end UniversalLaw.P15 diff --git a/formal/UniversalLaw/P15/RealizedCovers.lean b/formal/UniversalLaw/P15/RealizedCovers.lean new file mode 100644 index 000000000..9fa4614b6 --- /dev/null +++ b/formal/UniversalLaw/P15/RealizedCovers.lean @@ -0,0 +1,127 @@ +/-! +# P15 realized covers — exact counts of the 816-label benchmark + +Informal source (Layer 0, byte-pinned): `Math-` commit +`760340e921ac4ceda296b8118da936f1133e956e`, +`frontiers/three_fronts_20260924/P15_REALIZED_COVERS.md`, 11467 bytes, SHA-256 +`c0dbb821fb57b685a20cc321e4074456f39a9697f3104afd1f728e4732179bb9` +(object P15-REALIZED-COVERS-20260924-v1, author OpenAI / ChatGPT), sections 4–6. + +What this module establishes: the exact integer and rational arithmetic that the +source displays for the six-block benchmark (`a_i = 1`, `d_i = 408`, `H` = all +four-block subsets of six indices) — block and ground-set sizes, the two +minimal-forbidder counts of display (P10), the palette counts `816`, `815·3 < 2448` +and `818`, the elementary palette formula (P9) evaluated at the displayed inputs, +the ceiling identity `⌈n_i/a_i⌉ = d_i + 1` at finitely many instances, and the +union-bound rational of display (P11), and the positivity of the displayed cover +price `6/(40900^409)` as positivity of its numerator and of the power. Binomial +coefficients are computed by the exact multiplicative recursion and ceilings by +`(a + b − 1) / b`; both are defined locally so that the library has no +dependencies. Core Lean's `Rat` is not kernel-decidable by `decide` (its +`DecidableEq` instance does not reduce), so (P11) is stated cross-multiplied over +`Nat` with the rational form in the docstring. Every proof is `decide` except the +positivity of `40900 ^ 409`, which is core `Nat.pow_pos` applied to `0 < 40900`. + +What this module does **not** establish: Proposition P1 (completeness of the +minimal forbidders), display (P2), Theorem P2 (that the full-block family covers +`O_K(D)` iff `K >= K_H(d)`), the palette formula (P9) itself, the probability +semantics of `mu_p`, the union bound and independence step behind (P11), the +hazard comparison (P4)–(P5), display (P8), or anything about the unrestricted +P15 prize, which the source itself leaves open. Nothing here changes any Layer 0 +status. +-/ + +namespace UniversalLaw.P15 + +/-- Binomial coefficient by the exact multiplicative recursion +`C(n, k+1) = C(n, k) · (n − k) / (k + 1)` (each product is divisible by `k + 1`, +and `n − k` truncates to `0` once `k ≥ n`). Kept local: no dependencies. -/ +def choose (n : Nat) : Nat → Nat + | 0 => 1 + | k + 1 => choose n k * (n - k) / (k + 1) + +/-- Ceiling of `a / b` for `b > 0`: `⌈a/b⌉ = (a + b − 1) / b`. -/ +def ceilDiv (a b : Nat) : Nat := (a + b - 1) / b + +/-- Source: "Take six blocks, a_i=1 and d_i=408. Thus EACH original block has 409 +vertices and the original ground set has 2454 vertices" (the source runs +"has409" and "has2454" together). `n_i = a_i d_i + 1 = 409`, `6 · 409 = 2454`. -/ +theorem benchmark_block_and_ground_sizes : 1 * 408 + 1 = 409 ∧ 6 * 409 = 2454 := by decide + +/-- Source: "H consists of all 15 four-block subsets" (source: "all15"): +`C(6, 4) = 15`. -/ +theorem four_block_supports_fifteen : choose 6 4 = 15 := by decide + +/-- Source (P10): "6*binom(409,2)=500616 internal pairs, 15*409^4=419743994415 +crossing transversal quadruples." Only the two integer values are checked; that +these count the minimal forbidders is Proposition P1. -/ +theorem minimal_forbidder_counts : + 6 * choose 409 2 = 500616 ∧ 15 * 409 ^ 4 = 419743994415 := by decide + +/-- Source: "Use 408 labels on macro-indices {0,2,4} and 408 different labels on +{1,3,5}, giving K_H(408,...,408)=816." Checked: `408 + 408 = 816`. That this +palette satisfies (P6), and that no smaller one does, is not checked. -/ +theorem palette_816_from_two_label_classes : 408 + 408 = 816 := by decide + +/-- Source: "at 815 it does not, because omitting one vertex from each block +leaves 2448 vertices, each color holds at most 3, and 815*3<2448. +Pairwise-disjoint local palettes would have used 2448 labels." Checked: +`2454 − 6 = 2448`, `815 · 3 < 2448`, `6 · 408 = 2448`. That each colour class +holds at most three vertices is the combinatorial step, not checked. -/ +theorem palette_815_fails_by_counting : 2454 - 6 = 2448 ∧ 815 * 3 < 2448 ∧ 6 * 408 = 2448 := by + decide + +/-- Source: "The whole ground set, unlike the cover-avoiding sets, needs 818 +colors, since 2454/3=818." Checked: the exact quotient `2454 / 3 = 818` with +`818 · 3 = 2454`. The chromatic claim itself is not checked. -/ +theorem whole_ground_chromatic_818 : 2454 / 3 = 818 ∧ 818 * 3 = 2454 := by decide + +/-- Source (P9): "K_H(d)=max(max_i d_i, ceil(sum_i d_i/s))" for `H` = all +`(s+1)`-subsets of `b` indices. The section-6 benchmark is the case `b = 6`, +`s + 1 = 4`, `d_i = 408`: `max(408, ⌈6·408/3⌉) = 816`; with `d_i + 1 = 409` for +the whole ground set: `max(409, ⌈6·409/3⌉) = 818`. The conjunct `3 + 1 = 4` is +not displayed: it reads the four-block supports as `s + 1 = 4` with `s = 3`. Only +the right-hand side of (P9) is evaluated; the formula is not proved. -/ +theorem elementary_palette_formula_instances : + 3 + 1 = 4 ∧ max 408 (ceilDiv (6 * 408) 3) = 816 ∧ max 409 (ceilDiv (6 * 409) 3) = 818 := by + decide + +/-- Source: "The macro triangle at unit demands needs 3 colors" (source: +"needs3"). The right-hand side of (P9) at `b = 3`, `s = 1`, `d_i = 1`: +`max(1, ⌈3/1⌉) = 3`. The chromatic claim is not checked. -/ +theorem macro_triangle_three_colors : max 1 (ceilDiv (1 + 1 + 1) 1) = 3 := by decide + +/-- Source: "the chromatic number of the ENTIRE ground set X is K_H(d+1), because +ceil(n_i/a_i)=d_i+1." With `n_i = a_i d_i + 1`, checked at five `(a_i, d_i)` +instances including the benchmark `(1, 408)`. The general identity for all +`a_i ≥ 1` is not checked. -/ +theorem ceil_block_over_capacity_instances : + ∀ p, p ∈ [(1, 1), (1, 408), (2, 3), (3, 5), (5, 2)] → + ceilDiv (p.1 * p.2 + 1) p.1 = p.2 + 1 := by decide + +/-- Source: "each block's occupancy probability is at most 409p=1/100" (source: +"at most409p") at `p = 1/40900`: `409 · (1/40900) = 1/100 ⇔ 409 · 100 = 40900`. +That the occupancy probability is at most `409p` (a union bound) is not checked. -/ +theorem block_occupancy_one_percent : 409 * 100 = 40900 := by decide + +/-- Source (P11): "Q=1-mu_p(D) <=500616/(40900^2)+15/(100^4) =2449227/8180000000 +< 3/10000" and "the actual-good probability exceeds 0.9997". Cross-multiplied: +`500616/40900^2 + 15/100^4 = 2449227/8180000000` is +`(500616·100^4 + 15·40900^2)·8180000000 = 2449227·(40900^2·100^4)`; +`2449227/8180000000 < 3/10000` is `2449227·10000 < 3·8180000000`; and +`1 − 3/10000 = 9997/10000`. The union bound, the independence of block +occupancies and the probability semantics are not checked. -/ +theorem low_failure_union_bound_arithmetic : + (500616 * 100 ^ 4 + 15 * 40900 ^ 2) * 8180000000 = 2449227 * (40900 ^ 2 * 100 ^ 4) ∧ + 2449227 * 10000 < 3 * 8180000000 ∧ 10000 - 3 = 9997 := by decide + +/-- Source: "The cover price is exactly 6/(40900^409)>0" at `p_v = c_v = 1/40900`. +Checked: `6/(40900^409) > 0` as positivity of the numerator `6` (six full-block +generators) and of the denominator `40900^409`; the latter is core `Nat.pow_pos` +applied to `0 < 40900` (the kernel does not evaluate the power). The price +identity itself — that the six-generator cover costs exactly `6/(40900^409)` — +is not checked. -/ +theorem cover_price_numerator_and_denominator_positive : 0 < 6 ∧ 0 < 40900 ^ 409 := + ⟨by decide, Nat.pow_pos (a := 40900) (n := 409) (by decide)⟩ + +end UniversalLaw.P15 diff --git a/formal/manifest.json b/formal/manifest.json index 8d4318869..4de5d9ec2 100644 --- a/formal/manifest.json +++ b/formal/manifest.json @@ -13,12 +13,12 @@ "work_item": "https://github.com/d6g8k5htny-coder/main/issues/95", "math_pilot": "https://github.com/d6g8k5htny-coder/Math-/tree/cc2989c1280f4f227d0c6aa30c8841d6ba01e46e/formal", "rollout_record": "docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md", - "work_offer_addressed": "Numerical formalizer, first step only: the exact arithmetic skeleton of the SIDE24 note. The coefficient definition and the proof-producing enclosure pipeline are NOT supplied." + "work_offer_addressed": "Numerical formalizer, first step only: the exact arithmetic skeleton of the SIDE24 note (31 targets, 2026-09-27) and of the four P15 price/cover notes (28 targets, 2026-10-10). The coefficient definition, the proof-producing enclosure pipeline, the rho_star enclosure, the log inequalities and Theorems F / T1 / P2 are NOT supplied." }, "author": { "provider": "Anthropic", "family": "Claude", - "agent": "Cursor cloud agent, 2026-09-27" + "agent": "Cursor cloud agent, 2026-09-27 (Side24 modules); Claude Code session_01Cz7WZybv8znP64SpPj6sWY, 2026-10-10 (P15 modules)" }, "lean_toolchain": "leanprover/lean4:v4.34.1", "dependency_revisions": {}, @@ -31,20 +31,27 @@ "formal/lean-toolchain": "d5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b", "formal/lakefile.toml": "58f0fa6864cc03e9bcbef2d8c0404e9f3385a30a6124000454319367906cbe4a", "formal/lake-manifest.json": "562d38ad95598486b2b592e6d072d5d3212735bfeb1cb6d8eb8ec04492522ba2", - "formal/UniversalLaw.lean": "cb94ad3490a00bc35b420a53a42ff65b6fc66a46b8a26ef1b87035d7bb15587e", + "formal/UniversalLaw.lean": "503f8ce5e3123f820e378a68961bca04c16e427dba2d48d8afdc372559f9fb32", "formal/UniversalLaw/Side24/Ledger.lean": "ae4a14f3db8cf26668e55e2d2f80e0dcecb0703826b40396d91fb6e0d266d3f7", "formal/UniversalLaw/Side24/ConeMoments.lean": "2bcd4a83683188856bce010c3dcdec6904e45a6d73b50b9f3891e632ff58985c", "formal/UniversalLaw/Side24/Endpoints.lean": "095102245297707316cfd7e244d5509f9b102fe5aa638b7acdbbcf9d3c9d52bd", + "formal/UniversalLaw/P15/PriceBoundary.lean": "d11f32fbbf6ffe726dff0ac889bfaf04d61c9f5818d3c447abf7132fbe96bd6e", + "formal/UniversalLaw/P15/RealizedCovers.lean": "1b60dd00925789ae86f081463fd97117561223568532b5f5a886fdc8247051b3", + "formal/UniversalLaw/P15/FullPrice.lean": "9fb2aad19ac132f52c6e6b89c1040890922e1f905e88fac29992b62cbc890569", "formal/sources/side24_v1/PROOF.md": "c06daccc4ba4b9168522b9888b76a7d599934fc3b91bd753ee5d492262917769", "formal/sources/side24_v1/ENCLOSURE.json": "72b6cd92d31394cdaf5da8919a5d548e902228af1f095cc184158a71d8287811", - "formal/SCOPE.md": "fd06700628b1fbc81c5cfe3786aaa455032375bcb879914f068a66b726802a17", + "formal/sources/p15_v1/three_fronts_20260924_P15_PRICE_BOUNDARY.md": "498af650ef7139c39d2630561dbfd0822c495ce6308a6cac8b767aefe0c2a40b", + "formal/sources/p15_v1/three_fronts_20260924_P15_REALIZED_COVERS.md": "c0dbb821fb57b685a20cc321e4074456f39a9697f3104afd1f728e4732179bb9", + "formal/sources/p15_v1/full_price_20260924_PROOF.md": "87521901ca8e5405b4d1e47f1deb1cd0326affbd6f5967b53c4178590da993f9", + "formal/sources/p15_v1/price_budget_20260924_PROOF.md": "3b79d2de60d77df9dd0d81cea60935d3dbceeb26fcf2d38d62667a425180a535", + "formal/SCOPE.md": "1793f0a86f3f5d5678373b73b766a24d2492b0feec21e46c507e92715afdd8d4", "formal/GLOSSARY.md": "342d4efb374fea31c39e51f8f6bcdbc50d7fb5fea1fd393eda21afff92c62fb8", - "formal/README.md": "1398c3c6d15476afe9d4ef01fc98fb199976907123b438ae1743f4e87e31e007", - "formal/REVIEW_LANE.md": "6a0dcdd93f1aec16ede829820b913116a5c60c2bbbd78630690599dbc5d8be41", - "formal/reviews/TEMPLATE_alignment_review.json": "e722e928ca43c16981e063d8eb1c91e9bf8c683241d9dcf156400a419e72feb3", + "formal/README.md": "1011d50bbeeb3f71e08e4bf6236c9a1ebda8edfa76beadfa3d1727b35da9e49b", + "formal/REVIEW_LANE.md": "651fb4e18b2691f215b52e8fcdc875d85a6c92b495dbff5532b863ecfaf13960", + "formal/reviews/TEMPLATE_alignment_review.json": "2f1302611aa84652490bd89f04d2bba833e95d762c06b1230ae832086ccdeef5", "formal/reviews/README.md": "333ca71e7c676cee89e5d01cd61999c21bb0584e41d6bdacb18afa410109f95d", "tools/formal_gate_check.py": "21c355e02ac6e01337d10465a3105b34b93f832586ee60aa2430f662a90cd8b7", - "tests/test_formal_gate.py": "4286136d8b24eca9b26d1e7b12933bed5b0961809b362a60c3af7bf46e6ed4b6" + "tests/test_formal_gate.py": "1a9e32ad54378874eb007db8d94ce45b340fc4ba16c48a680cc7c506c8bbd805" }, "unbound_files": [ "formal/manifest.json", @@ -68,12 +75,51 @@ "bytes": 1090, "sha256": "72b6cd92d31394cdaf5da8919a5d548e902228af1f095cc184158a71d8287811", "local_copy": "formal/sources/side24_v1/ENCLOSURE.json" + }, + { + "id": "p15-price-boundary", + "repository": "d6g8k5htny-coder/Math-", + "commit": "760340e921ac4ceda296b8118da936f1133e956e", + "path": "frontiers/three_fronts_20260924/P15_PRICE_BOUNDARY.md", + "bytes": 2266, + "sha256": "498af650ef7139c39d2630561dbfd0822c495ce6308a6cac8b767aefe0c2a40b", + "local_copy": "formal/sources/p15_v1/three_fronts_20260924_P15_PRICE_BOUNDARY.md" + }, + { + "id": "p15-realized-covers", + "repository": "d6g8k5htny-coder/Math-", + "commit": "760340e921ac4ceda296b8118da936f1133e956e", + "path": "frontiers/three_fronts_20260924/P15_REALIZED_COVERS.md", + "bytes": 11467, + "sha256": "c0dbb821fb57b685a20cc321e4074456f39a9697f3104afd1f728e4732179bb9", + "local_copy": "formal/sources/p15_v1/three_fronts_20260924_P15_REALIZED_COVERS.md" + }, + { + "id": "p15-full-price", + "repository": "d6g8k5htny-coder/Math-", + "commit": "760340e921ac4ceda296b8118da936f1133e956e", + "path": "frontiers/full_price_20260924/PROOF.md", + "bytes": 11352, + "sha256": "87521901ca8e5405b4d1e47f1deb1cd0326affbd6f5967b53c4178590da993f9", + "local_copy": "formal/sources/p15_v1/full_price_20260924_PROOF.md" + }, + { + "id": "p15-price-budget", + "repository": "d6g8k5htny-coder/Math-", + "commit": "760340e921ac4ceda296b8118da936f1133e956e", + "path": "frontiers/price_budget_20260924/PROOF.md", + "bytes": 7935, + "sha256": "3b79d2de60d77df9dd0d81cea60935d3dbceeb26fcf2d38d62667a425180a535", + "local_copy": "formal/sources/p15_v1/price_budget_20260924_PROOF.md" } ], "source_modules": [ "UniversalLaw/Side24/Ledger.lean", "UniversalLaw/Side24/ConeMoments.lean", - "UniversalLaw/Side24/Endpoints.lean" + "UniversalLaw/Side24/Endpoints.lean", + "UniversalLaw/P15/PriceBoundary.lean", + "UniversalLaw/P15/RealizedCovers.lean", + "UniversalLaw/P15/FullPrice.lean" ], "targets": [ { @@ -323,6 +369,230 @@ "source": "side24-enclosure", "informal_anchor": "\"relative_periodization_bound\": \"1e-106\"", "does_not_claim": "anything about the true coefficients" + }, + { + "name": "UniversalLaw.P15.smallest_member_block_size", + "module": "UniversalLaw/P15/PriceBoundary.lean", + "title": "Smallest one-block member has block size 1·1+1 = 2", + "source": "p15-price-boundary", + "informal_anchor": "one-block member: a_1=d_1=1, X={x,y}", + "does_not_claim": "the realized-cover theorem or its family; the probability or price semantics; the two log inequalities; Theorem F; prize status" + }, + { + "name": "UniversalLaw.P15.demand_one_good_sets", + "module": "UniversalLaw/P15/PriceBoundary.lean", + "title": "Good sets of the demand-one block are ∅, {x}, {y} (finite enumeration)", + "source": "p15-price-boundary", + "informal_anchor": "Its good sets are the empty\nset and singletons", + "does_not_claim": "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" + }, + { + "name": "UniversalLaw.P15.demand_one_obstruction", + "module": "UniversalLaw/P15/PriceBoundary.lean", + "title": "One-piece obstruction O_1(D) is exactly {X} (finite enumeration)", + "source": "p15-price-boundary", + "informal_anchor": "its one-piece obstruction\nis exactly {X}", + "does_not_claim": "the identity I_1(D)=D in general; cover semantics; the log inequalities; Theorem F; prize status" + }, + { + "name": "UniversalLaw.P15.good_measure_three_quarters", + "module": "UniversalLaw/P15/PriceBoundary.lean", + "title": "mu_p(D) = 3/4 at p = 1/2 as 3 of 4 quarter-weights (total 4 = 2^2)", + "source": "p15-price-boundary", + "informal_anchor": "Nevertheless mu_p(D)=3/4", + "does_not_claim": "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" + }, + { + "name": "UniversalLaw.P15.generator_prices_ninths", + "module": "UniversalLaw/P15/PriceBoundary.lean", + "title": "Generator costs 1, 2/3, 2/3, 4/9 over denominator 9: 9, 6, 6, 4", + "source": "p15-price-boundary", + "informal_anchor": "The possible generator costs are1,2/3,2/3,4/9", + "does_not_claim": "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" + }, + { + "name": "UniversalLaw.P15.minimum_generator_price_exceeds_third", + "module": "UniversalLaw/P15/PriceBoundary.lean", + "title": "Minimum displayed generator cost 4/9, and 4/9 > 1/3 (1·9 < 4·3)", + "source": "p15-price-boundary", + "informal_anchor": "covercost_c(O_1(D))=4/9 > 1/3 > log(4/3)", + "does_not_claim": "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" + }, + { + "name": "UniversalLaw.P15.benchmark_block_and_ground_sizes", + "module": "UniversalLaw/P15/RealizedCovers.lean", + "title": "Benchmark sizes: 1·408+1 = 409 per block, 6·409 = 2454 vertices", + "source": "p15-realized-covers", + "informal_anchor": "EACH original block has409 vertices and the original ground set has2454 vertices", + "does_not_claim": "the construction (P1)–(P2), Proposition P1, probability semantics; Theorem P2; prize status" + }, + { + "name": "UniversalLaw.P15.four_block_supports_fifteen", + "module": "UniversalLaw/P15/RealizedCovers.lean", + "title": "C(6,4) = 15 four-block supports", + "source": "p15-realized-covers", + "informal_anchor": "H consists of all15 four-block subsets", + "does_not_claim": "the clutter structure of H or Proposition P1; Theorem P2; prize status" + }, + { + "name": "UniversalLaw.P15.minimal_forbidder_counts", + "module": "UniversalLaw/P15/RealizedCovers.lean", + "title": "(P10) 6·C(409,2) = 500616 and 15·409^4 = 419743994415", + "source": "p15-realized-covers", + "informal_anchor": "6*binom(409,2)=500616 internal pairs,\n 15*409^4=419743994415 crossing transversal quadruples.", + "does_not_claim": "that these numbers count the minimal forbidders (Proposition P1); Theorem P2; prize status" + }, + { + "name": "UniversalLaw.P15.palette_816_from_two_label_classes", + "module": "UniversalLaw/P15/RealizedCovers.lean", + "title": "K_H(408,…,408) = 816 as 408 + 408", + "source": "p15-realized-covers", + "informal_anchor": "K_H(408,...,408)=816", + "does_not_claim": "that the two label classes satisfy (P6) or that no smaller palette does (the palette optimum); Theorem P2; prize status" + }, + { + "name": "UniversalLaw.P15.palette_815_fails_by_counting", + "module": "UniversalLaw/P15/RealizedCovers.lean", + "title": "2454−6 = 2448, 815·3 < 2448, 6·408 = 2448", + "source": "p15-realized-covers", + "informal_anchor": "omitting one vertex from each block leaves2448 vertices, each color holds at most3, and815*3<2448", + "does_not_claim": "that each colour class holds at most three vertices (the combinatorial step); Theorem P2; prize status" + }, + { + "name": "UniversalLaw.P15.whole_ground_chromatic_818", + "module": "UniversalLaw/P15/RealizedCovers.lean", + "title": "2454/3 = 818 exactly (818·3 = 2454)", + "source": "p15-realized-covers", + "informal_anchor": "needs818 colors, since2454/3=818", + "does_not_claim": "the chromatic number of the ground set (K_H(d+1)) or the palette argument; Theorem P2; prize status" + }, + { + "name": "UniversalLaw.P15.elementary_palette_formula_instances", + "module": "UniversalLaw/P15/RealizedCovers.lean", + "title": "(P9) right-hand side at the benchmark: max(408,⌈2448/3⌉) = 816, max(409,⌈2454/3⌉) = 818; 3+1 = 4", + "source": "p15-realized-covers", + "informal_anchor": "K_H(d)=max(max_i d_i, ceil(sum_i d_i/s))", + "does_not_claim": "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" + }, + { + "name": "UniversalLaw.P15.macro_triangle_three_colors", + "module": "UniversalLaw/P15/RealizedCovers.lean", + "title": "(P9) right-hand side for the macro triangle at unit demands: max(1,⌈3/1⌉) = 3", + "source": "p15-realized-covers", + "informal_anchor": "The macro triangle at unit demands needs3 colors", + "does_not_claim": "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" + }, + { + "name": "UniversalLaw.P15.ceil_block_over_capacity_instances", + "module": "UniversalLaw/P15/RealizedCovers.lean", + "title": "⌈(a·d+1)/a⌉ = d+1 at five (a,d) instances including (1,408)", + "source": "p15-realized-covers", + "informal_anchor": "ceil(n_i/a_i)=d_i+1", + "does_not_claim": "the identity for all a_i >= 1; that the whole-ground chromatic number is K_H(d+1); Theorem P2; prize status" + }, + { + "name": "UniversalLaw.P15.block_occupancy_one_percent", + "module": "UniversalLaw/P15/RealizedCovers.lean", + "title": "409·100 = 40900 behind 409p = 1/100 at p = 1/40900", + "source": "p15-realized-covers", + "informal_anchor": "each block's occupancy probability is at most409p=1/100", + "does_not_claim": "the union bound giving occupancy probability at most 409p; probability semantics; Theorem P2; prize status" + }, + { + "name": "UniversalLaw.P15.low_failure_union_bound_arithmetic", + "module": "UniversalLaw/P15/RealizedCovers.lean", + "title": "(P11) 500616/40900^2 + 15/100^4 = 2449227/8180000000 < 3/10000, cross-multiplied; 10000−3 = 9997", + "source": "p15-realized-covers", + "informal_anchor": "=2449227/8180000000 < 3/10000", + "does_not_claim": "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" + }, + { + "name": "UniversalLaw.P15.cover_price_numerator_and_denominator_positive", + "module": "UniversalLaw/P15/RealizedCovers.lean", + "title": "6/(40900^409) > 0 as 0 < 6 and 0 < 40900^409 (core Nat.pow_pos)", + "source": "p15-realized-covers", + "informal_anchor": "6/(40900^409)>0", + "does_not_claim": "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" + }, + { + "name": "UniversalLaw.P15.rho_star_endpoints_adjacent", + "module": "UniversalLaw/P15/FullPrice.lean", + "title": "Published rho_star endpoints are adjacent 20-digit decimals", + "source": "p15-full-price", + "informal_anchor": "0.84547981724898672067 < rho_star", + "does_not_claim": "that rho_star = 1/(3 - log(3e - 2)) lies between them (needs Real.exp/Real.log; Mathlib lane); Theorem F; prize status" + }, + { + "name": "UniversalLaw.P15.rho_star_upper_endpoint_below_six_sevenths", + "module": "UniversalLaw/P15/FullPrice.lean", + "title": "Upper endpoint below 6/7: …68·7 < 6·10^20", + "source": "p15-full-price", + "informal_anchor": "< 0.84547981724898672068 < 6/7", + "does_not_claim": "rho_star < 6/7 as a statement about the real number; h_star > 7/6; Theorem F; prize status" + }, + { + "name": "UniversalLaw.P15.sixteen_twentysevenths_below_six_sevenths", + "module": "UniversalLaw/P15/FullPrice.lean", + "title": "16/27 < 6/7 (16·7 < 6·27) and 16/27 below the published lower endpoint", + "source": "p15-full-price", + "informal_anchor": "gives the stronger factor16/27 on its smaller domain", + "does_not_claim": "Theorem (T1) or its domain p_v <= 1/4; that 16/27 < rho_star as a real-number statement; Theorem F; prize status" + }, + { + "name": "UniversalLaw.P15.minimal_block_size_instances", + "module": "UniversalLaw/P15/FullPrice.lean", + "title": "1·2+1 = 3 and 2a+1 <= ad+1 at five (a,d) instances with d >= 2", + "source": "p15-full-price", + "informal_anchor": "Our n=ad+1 and d>=2 imply n>=2a+1.", + "does_not_claim": "the implication for all a >= 1, d >= 2; the binomial tail comparison (F9)–(F11); the sharpness argument of section 5; Theorem F; prize status" + }, + { + "name": "UniversalLaw.P15.e_rational_bounds_ordering", + "module": "UniversalLaw/P15/FullPrice.lean", + "title": "31967/11760 < 87/32 and 87/32 − 31967/11760 = 11/23520, cross-multiplied", + "source": "p15-full-price", + "informal_anchor": "e < 31967/11760 < 87/32,\n 87/32-31967/11760=11/23520.", + "does_not_claim": "e < 31967/11760 (exponential series plus geometric tail); any statement about e; Theorem F; prize status" + }, + { + "name": "UniversalLaw.P15.exp_eleven_sixths_taylor_certificate", + "module": "UniversalLaw/P15/FullPrice.lean", + "title": "Degree-5 Taylor partial sum of exp(11/6) minus 197/32 equals 26081/933120 > 0", + "source": "p15-full-price", + "informal_anchor": "sum_(j=0)^5 (11/6)^j/j! -197/32=26081/933120>0", + "does_not_claim": "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" + }, + { + "name": "UniversalLaw.P15.h_star_rational_certificate_constants", + "module": "UniversalLaw/P15/FullPrice.lean", + "title": "3·87 − 2·32 = 197 and 3·6 − 11 = 7 behind 3e−2 < 197/32 and h_star > 7/6", + "source": "p15-full-price", + "informal_anchor": "Therefore 3e-2<197/327/6 and rho_star<6/7.", + "does_not_claim": "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" + }, + { + "name": "UniversalLaw.P15.t3_ratio_at_minimal_block", + "module": "UniversalLaw/P15/FullPrice.lean", + "title": "(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", + "source": "p15-price-budget", + "informal_anchor": "= (4^(a+1))/(3^n)\n <= (4/3)*(4/9)^a <=16/27.", + "does_not_claim": "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" + }, + { + "name": "UniversalLaw.P15.t3_bound_finite_instances", + "module": "UniversalLaw/P15/FullPrice.lean", + "title": "(T3) final inequalities at seven (a,n) pairs with n >= 2a+1 and at a = 1..6", + "source": "p15-price-budget", + "informal_anchor": "<= (4/3)*(4/9)^a <=16/27", + "does_not_claim": "the inequalities for all a >= 1, n >= 2a+1; (T2); Theorem (T1); prize status" + }, + { + "name": "UniversalLaw.P15.explicit_rational_price_above_p", + "module": "UniversalLaw/P15/FullPrice.lean", + "title": "c = p + p^2/2 = 81801/3345620000 at p = 1/40900, and c > p", + "source": "p15-price-budget", + "informal_anchor": "c=p+p^2/2=81801/3345620000", + "does_not_claim": "admissibility c <= phi(p) (the integral inequality); the price bound (T7); that the 816-label cover is valid at these prices; prize status" } ], "negative_controls": { @@ -360,6 +630,46 @@ "module": "UniversalLaw/Side24/Endpoints.lean", "replace": "d2Upper = d2Lower + 1", "with": "d2Upper = d2Lower + 2" + }, + "false_price_boundary_third": { + "module": "UniversalLaw/P15/PriceBoundary.lean", + "replace": "1 * 9 < 4 * 3", + "with": "1 * 9 < 2 * 3" + }, + "wrong_generator_prices": { + "module": "UniversalLaw/P15/PriceBoundary.lean", + "replace": "= [9, 6, 6, 4]", + "with": "= [9, 6, 6, 5]" + }, + "false_palette_815_count": { + "module": "UniversalLaw/P15/RealizedCovers.lean", + "replace": "815 * 3 < 2448", + "with": "816 * 3 < 2448" + }, + "wrong_transversal_count": { + "module": "UniversalLaw/P15/RealizedCovers.lean", + "replace": "= 419743994415", + "with": "= 419743994416" + }, + "false_union_bound_three_tenthousandths": { + "module": "UniversalLaw/P15/RealizedCovers.lean", + "replace": "2449227 * 10000 < 3 * 8180000000", + "with": "2449227 * 10000 < 2 * 8180000000" + }, + "false_rho_endpoint_adjacency": { + "module": "UniversalLaw/P15/FullPrice.lean", + "replace": "rhoUpper = rhoLower + 1", + "with": "rhoUpper = rhoLower + 2" + }, + "false_rho_upper_six_sevenths": { + "module": "UniversalLaw/P15/FullPrice.lean", + "replace": "rhoUpper * 7 < 6 * 10 ^ 20", + "with": "rhoUpper * 7 < 5 * 10 ^ 20" + }, + "wrong_taylor_certificate": { + "module": "UniversalLaw/P15/FullPrice.lean", + "replace": "= 197 * 29160 + 26081", + "with": "= 197 * 29160 + 26080" } } } diff --git a/formal/reviews/TEMPLATE_alignment_review.json b/formal/reviews/TEMPLATE_alignment_review.json index ba5a1b4c2..aa51b72ac 100644 --- a/formal/reviews/TEMPLATE_alignment_review.json +++ b/formal/reviews/TEMPLATE_alignment_review.json @@ -4,12 +4,12 @@ "scope_sha256": "REPLACE_WITH_THE_files[formal/SCOPE.md]_VALUE_FROM_THAT_MANIFEST", "targets": [ "UniversalLaw.Side24.pairing_sum_six", - "... exactly all 31 target names from manifest.json ..." + "... exactly all 59 target names from manifest.json ..." ], "author": { "provider": "Anthropic", "family": "Claude", - "agent": "Cursor cloud agent, 2026-09-27" + "agent": "Cursor cloud agent, 2026-09-27 (Side24 modules); Claude Code session_01Cz7WZybv8znP64SpPj6sWY, 2026-10-10 (P15 modules)" }, "reviewer": { "provider": "REPLACE (must differ from author)", diff --git a/formal/sources/p15_v1/full_price_20260924_PROOF.md b/formal/sources/p15_v1/full_price_20260924_PROOF.md new file mode 100644 index 000000000..582180e41 --- /dev/null +++ b/formal/sources/p15_v1/full_price_20260924_PROOF.md @@ -0,0 +1,153 @@ +# Full transformed-price budgets without a probability cutoff + +**Object:** P15-FULL-TRANSFORMED-PRICE-20260924-v1. +**Author:** OpenAI / ChatGPT. **Disposition:** author-side mathematical derivation; nonauthor review open. + +[Research home](https://github.com/d6g8k5htny-coder/main) · [Math index](../../README.md) · [Original realization](../three_fronts_20260924/P15_REALIZED_COVERS.md) · [Demand-one counterexample](../three_fronts_20260924/P15_PRICE_BOUNDARY.md) + +## 1. Exact scope and result + +Use the original realized family, not arbitrary P15 inputs. H is a finite clutter of block supports, every edge has size at least two (empty H is allowed). The original coordinate blocks are disjoint, with + + |X_i|=a_i d_i+1, a_i>=1, d_i>=2 integers. + +The decreasing family D consists of U with |U intersect X_i|<=a_i in each block and with occupied-block support containing no H-edge. Its complete minimal original forbidders and its actual local restrictions are proved in P15-REALIZED-COVERS-20260924-v1, SHA256 `c0dbb821fb57b685a20cc321e4074456f39a9697f3104afd1f728e4732179bb9`. + +Write O_K(D) for sets not partitionable into at most K members of D. Let K_H(d) be the least palette size with |P_i|>=d_i and empty intersection over every H-edge. For K>=K_H(d), the specified family of full-block generators {X_i} covers O_K(D), regardless of probabilities or prices. A generator g costs product_(v in g)c_v. The empty generator costs one; an empty family costs zero. + +Put phi(p)=min(1,-log(1-p)), with phi(1)=1. Define + + p_star=1-exp(-1), + h_star=3-log(3e-2), + rho_star=1/h_star. (F1) + +**Theorem F.** For EVERY independent original probability vector p in [0,1]^X, every price vector 0<=c_v<=phi(p_v), and the SAME palette K>=K_H(d), + + covercost_c(O_K(D)) <= min(1,rho_star[-log mu_p(D)]). (F2) + +Before capping, the union of full-block generators has price at most rho_star times the global hazard. The constant rho_star is optimal uniformly over this entire realized class, even when alternative generator covers are allowed. Explicitly, + + 0.84547981724898672067 < rho_star + < 0.84547981724898672068 < 6/7. (F3) + +Thus 6/7 is a simpler valid rational factor. The probability ceilings 1/4 and 3/7 are no longer required. Demand d_i>=2 is still essential to this uniform family guarantee. This is not an unrestricted downset/prize theorem; palette size remains K_H(d), which can depend on H and d. + +The prior probability<=1/4 theorem, SHA `3b79d2de60d77df9dd0d81cea60935d3dbceeb26fcf2d38d62667a425180a535`, gives the stronger factor16/27 on its smaller domain and should still be used there. The local-only3/7 note is a historical intermediate result, not a prerequisite here. No prior proof or counterexample is overwritten. + +## 2. A general hazard interpolation lemma + +Let A be any proper decreasing family on n>=1 coordinates containing the empty set. Put + + p_i(t)=1-exp(-t_i), t in [0,1]^n, + F_A(t)=-log mu_(p(t))(A), + H_A=F_A(1,...,1)>0. + +The probability is positive on this compact cube because the empty set is admitted and every p_i(t)<1. In one coordinate, after averaging over all others, its good-event probability is exactly + + mu(A)=A0+B0 exp(-t_i), A0>=0, B0>=0. (F4) + +Here A0 is the probability of membership when that coordinate is present, and A0+B0 is the probability when it is absent. The inequality B0>=0 follows from decreasingness. Their sum is positive. Direct differentiation yields + + partial_i F_A = B0 exp(-t_i)/(A0+B0 exp(-t_i)), + partial_i^2 F_A = -A0 B0 exp(-t_i) + /(A0+B0 exp(-t_i))^2 <= 0. (F5) + +Only SEPARATE coordinatewise concavity is asserted; joint concavity is not needed or claimed. Also F_A>=0. The chord inequality in coordinate i therefore gives + + F_A(t) >= t_i F_A(t with t_i=1). + +Iterating across coordinates, keeping all factors nonnegative, proves + + F_A(t) >= (product_i t_i) H_A. (F6) + +Now take arbitrary original probabilities p_i in [0,1], set t_i=phi(p_i), and let p'_i=1-exp(-t_i). Then p'_i<=p_i, including p_i=1. Decreasingness gives mu_p(A)<=mu_(p')(A), so + + -log mu_p(A) >= H_A product_i phi(p_i). (F7) + +This holds as an extended inequality if the left side is infinite. At a zero probability the product is zero; no division by it is performed. For any transformed prices, + + product_i c_i <= min(1, [-log mu_p(A)]/H_A). (F8) + +This is a PRICE estimate for the full-ground generator. It does not assert that this generator alone covers an arbitrary obstruction. That setwise property is supplied separately for the capacity construction below. + +The constant1/H_A in the uncapped hazard comparison is exact: at every p_i=p_star and every c_i=1, the two sides of (F7) are equal. In particular a full-ground generator universally meets the capped hazard budget precisely when H_A>=1. The necessity uses that same reference vector; it does not infer coverage of arbitrary A. + +## 3. Capacity families and the sharp worst case + +For a capacity restriction A={S:|S|<=a} on n coordinates, + + H_(n,a)=-log P(Bin(n,p_star)<=a). (F9) + +Our n=ad+1 and d>=2 imply n>=2a+1. Adding independent Bernoulli trials without raising the threshold can only decrease the good probability. It remains to compare odd majority tails. Let S~Bin(2a+1,p), with p>1/2. Directly adjoining two trials gives + + P(Bin(2a+3,p)<=a+1)-P(S<=a) + =(1-p)^2 P(S=a+1)-p^2 P(S=a) + =p(1-2p)P(S=a)<0. (F10) + +The ratio P(S=a+1)/P(S=a)=p/(1-p) proves the second equality. Since a>=1, the maximal odd-tail probability occurs at a=1,n=3. Consequently + + H_(n,a) >= H_(3,1) + =-log[3exp(-2)-2exp(-3)] + =3-log(3e-2)=h_star>1. (F11) + +For the last inequality, e>2 and + + e^2-(3e-2)=(e-1)(e-2)>0, + +so 3exp(-2)-2exp(-3)=K_H(d); (F13) gives its budget. If its union price exceeds one, use the empty generator. This proves (F2). If a local good probability is zero, global goodness has probability zero and the price-one cap proves the assertion. If global goodness is zero for crossing reasons alone, the same cap applies. Zero-price generators are kept for setwise completeness. + +For the established six blocks of409 coordinates (a_i=1,d_i=408, all15 four-block supports), the SAME816-label cover now works for every independent p_v in [0,1] and every c_v<=phi(p_v). Its whole-ground chromatic number remains818. No coordinates are cloned, and the full crossing family is retained. At sufficiently low probabilities the earlier16/27 budget is better; on the whole cube (F2) is valid. + +## 5. Sharpness and the exact demand boundary + +Take one block, a=1,d=2,n=3, no macro edges and K=2. Every proper subset is two-decomposable and the full triple is not. At p_i=p_star and c_i=1, every possible generator has price one, including the empty generator. Any cover of the nonempty obstruction therefore costs at least one, and one generator attains it. The available hazard is h_star. Replacing rho_star by any smaller constant in (F2) would make its right side strictly less than one. This proves sharpness even among alternative covers, not only for our chosen full-block cover. + +If d=1, n=a+1 and K=1, the sole obstruction is again the full block. At p_i=p_star,c_i=1 every cover costs at least one, but + + mu_p(D)=1-p_star^(a+1)>1-p_star=exp(-1), + +hence its hazard is less than one. The universal same-palette transformed-price guarantee is false in this demand-one family. This preserves and generalizes the earlier two-coordinate counterexample; it does not retract original P15-B, whose local-budget premise is missing in that case. + +Thus d>=2 is sufficient for the realized capacity family on the full probability cube, while a uniform statement admitting all d=1 examples would be false. This is not a necessity claim for every multi-block instance with some demand one; other constraints may change its budget. + +## 6. Exact numerical certificate and validation limits + +The proof of the simpler bound rho_star<6/7 can be made with short rational certificates. The exponential series and its positive geometric tail give + + e < 31967/11760 < 87/32, + 87/32-31967/11760=11/23520. + +The positive Taylor polynomial through degree5 satisfies + + sum_(j=0)^5 (11/6)^j/j! -197/32=26081/933120>0. + +Therefore 3e-2<197/327/6 and rho_star<6/7. + +For (F3), full_price.py bounds e by its positive series plus a geometric tail. It encloses logarithms using binary reduction and + + log x = 2 sum_(j>=0) t^(2j+1)/(2j+1), t=(x-1)/(x+1), + +on 1<=x<=2, with remainder bounded by2 t^(2m+1)/[(2m+1)(1-t^2)]. Exact Fraction endpoints are propagated monotonically through the binomial tail and logarithm, then reciprocated and rounded outward to20 decimal places. No floating-point value determines a certified endpoint. + +The finite suite checks the recurrence against subset enumeration, the odd-majority identity, the coordinatewise derivative sign, exact constants and endpoint conventions, heterogeneous probability grids, and preservation of the demand-one counterexample. These checks support algebra and implementation; the continuum hazard inequality is the written proof, not a conclusion from the grid. No independent reviewer, formal checker, Gaussian/RN closure or unrestricted prize acceptance is claimed. + +## 7. Source and reconnaissance + +Project inputs are the unchanged realized-cover and price-boundary sources linked above, original P15-B (Drive19D-eHQAIXMGGy2ThZUfZ0GGjIKWm5C2j; SHA9b18b6e9abc90d18deef06ab12e3aa7794dad40e1618d99daa88e369c300e8c3), and the published restricted-price note (Math-PR4). This proof derives (F4)-(F13) directly rather than importing a theorem from an abstract. + +Primary-source reconnaissance on24September2026 read the arXiv abstracts of Gunby–He–Narayanan, Down-set thresholds,2112.08525v2, and Warnke, Note on down-set thresholds,2310.11662v2. Their downset/expectation-threshold results provide neighboring context, not the hazard-transfer theorem above, and do not license arbitrary-downset closure. The bounded search did not establish novelty or historical priority. Attribution to classical separate concavity, Bernoulli conditioning, and binomial identities is not replaced by a project-specific invention claim. diff --git a/formal/sources/p15_v1/price_budget_20260924_PROOF.md b/formal/sources/p15_v1/price_budget_20260924_PROOF.md new file mode 100644 index 000000000..9b17d179d --- /dev/null +++ b/formal/sources/p15_v1/price_budget_20260924_PROOF.md @@ -0,0 +1,152 @@ +# Restoring the transformed-price budget under explicit hypotheses + +**Object:** P15-TRANSFORMED-PRICE-BUDGET-20260924-v1. +**Author:** OpenAI / ChatGPT. **Disposition:** author-side derivation; nonauthor review open. + +[Research home](https://github.com/d6g8k5htny-coder/main) · [Math index](../../README.md) · [Prior construction](../three_fronts_20260924/P15_REALIZED_COVERS.md) · [Unchanged counterexample](../three_fronts_20260924/P15_PRICE_BOUNDARY.md) + +## 1. What changes and what does not + +The exact original-coordinate construction in `P15_REALIZED_COVERS.md`, SHA256 +`c0dbb821fb57b685a20cc321e4074456f39a9697f3104afd1f728e4732179bb9`, proves a +cover theorem for prices c_v<=p_v. The separate two-coordinate counterexample, +SHA256 `498af650ef7139c39d2630561dbfd0822c495ce6308a6cac8b767aefe0c2a40b`, +refutes extending the SAME palette to every c_v<=phi(p_v) with no additional +hypotheses. Both sources remain unchanged. Here phi(p)=min(1,-log(1-p)), with +phi(1)=1. This note supplies additional sufficient hypotheses; it does not retract +that counterexample, accept an unrestricted prize, or claim new classical coloring theory. + +Use the prior construction exactly. H is a clutter of block supports, with every +edge of size at least two; the original disjoint blocks satisfy |X_i|=a_i*d_i+1. +The downset D consists of sets using at most a_i vertices of each block and whose +occupied-block support contains no H-edge. The complete crossing witnesses are +ALL H-edge transversals. K_H(d) is the integer demand-palette optimum. The specified +cover consists of the full blocks X_i; an obstructed set contains a generator. +A generator g costs product_(v in g)c_v, the empty generator costs one, and an +empty family costs zero. No random coordinates are copied. + +**Theorem (restricted transformed-price extension).** Suppose every a_i>=1, +every d_i>=2, and all independent original probabilities satisfy 0<=p_v<=1/4. +Then for EVERY set of prices 0<=c_v<=phi(p_v), at the SAME K>=K_H(d), + + covercost_c(O_K(D)) <= min(1,(16/27)*[-log mu_p(D)]). (T1) + +The uncapped full-block union has cost at most the expression inside the second +argument of this minimum. Cap with the empty generator when needed. The palette +and the original-coordinate support family are not enlarged. The constants in +this theorem are explicit; unlike the Gaussian lifetime remainder, there is no +unevaluated radius or error constant here. + +## 2. Local budget proof + +For 0<=p<1, elementary integration gives + + -log(1-p)=integral_0^p dt/(1-t) <= p/(1-p). (T2) + +Consider one block with capacity a>=1, demand d>=2 and n=ad+1. Its local failure +probability is q=P(number of selected original coordinates > a). If any p_v=0, +the full-block generator price is zero and the desired inequality is immediate; +the zero-price generator remains in the cover for setwise completeness. + +Otherwise choose any subset S of a+1 original coordinates. The event that all +members of S are selected is a local failure, regardless of the other coordinates. +By independence, q>=product_(v in S)p_v. Using (T2), p_v<=1/4, and n>=2a+1, + + product_(v in X)c_v / product_(v in S)p_v + <= product_(v notin S)p_v / product_(v in X)(1-p_v) + <= (1/4)^(n-a-1)/(3/4)^n + = (4^(a+1))/(3^n) + <= (4/3)*(4/9)^a <=16/27. (T3) + +Consequently the full-block generator satisfies + + price({X}) <= (16/27)q <= phi(q). (T4) + +This proof does not require equal probabilities. No independence of different +crossing-witness events is used. The extra demand hypothesis d>=2 is load-bearing: +when a=d=1, n=2, the ratio calculation does not supply (T3), and the earlier +counterexample applies. The bound p_v<=1/4 is a sufficient range, not an asserted +sharp threshold. + +A more general sufficient ratio, for any common upper bound p_*<1, is + + rho(a,d,p_*)=p_*^(ad-a)/(1-p_*)^(ad+1). (T5) + +If rho<=1 the same argument proves price({X})<=q for that block. This is only a +sufficient test; rho>1 is not a counterexample and must not be labeled infeasible. + +## 3. Global budget and unchanged palette + +Write q_i=P(U intersect X_i notin D_i) for the ACTUAL capacity restriction. +Disjoint original blocks make their local-good events independent. Global goodness +implies all local restrictions are good, even though crossing constraints may +create further failures. Therefore + + mu_p(D)<=product_i(1-q_i), + sum_i q_i<=-log(product_i(1-q_i))<=-log mu_p(D). (T6) + +Sum (T4), then use (T6). The exact setwise argument of the prior realization +shows that the union of full-block generators covers O_K(D) for K>=K_H(d), +independently of prices. This proves (T1). If mu_p(D)=0 the price-one cap applies; +if mu_p(D)=1 the union price is zero by the same estimates. This is the same +local-cover/budget interface as original P15-B, source SHA256 +`9b18b6e9abc90d18deef06ab12e3aa7794dad40e1618d99daa88e369c300e8c3`. + +## 4. Exact original-coordinate consequence for the 816-label example + +Use the prior six blocks of 409 original coordinates, a_i=1, d_i=408, and all +15 four-block forbidden supports. At p_v=1/40900, every hypothesis above holds. +Thus the SAME 816-label obstruction cover is valid for the FULL transformed range + + 0<=c_v<=log(40900/40899), + +not merely c_v<=1/40900. At maximal equal prices its nonzero union price is + + 6*log(40900/40899)^409 <=6/(40899^409). (T7) + +An explicit rational price strictly larger than p is + + c=p+p^2/2=81801/3345620000. + +It is admissible since integral_0^p 1/(1-t)dt > integral_0^p(1+t)dt for p>0. +Its cover price is exactly 6*c^409. The palette remains 816; the entire ground +set still requires 818 colors, and there are 2454 original coordinates. No large +witness enumeration or new claim about arbitrary old P15 instances is involved. + +## 5. A useful exact checker beyond the simple uniform hypothesis + +The supplied standard-library program computes q exactly for rational inputs via +a truncated Poisson-binomial recursion. If b_j denotes P(exactly j successes) for +j<=a, one new coordinate updates b_j to (1-p)b_j+p b_(j-1); discarded higher +counts never return. Hence q=1-sum_(j=0)^a b_j after all coordinates. + +It bounds every transformed generator price by + + U=product_v min(1,p_v/(1-p_v)), + +with the p_v=1 factor defined as one. It certifies a sufficient local budget if +U<=q, or if q>=2/3 (then phi(q)=1, since log3>1). The low-probability theorem +additionally verifies U<=(16/27)q. It rejects inexact inputs and explicitly limits +problem size; its arithmetic cost is O(n*a) rational operations, not a polynomial +bit-complexity or arbitrary-hypergraph optimization claim. + +A non-certified output means only these sufficient tests did not prove the budget. +The program is not a full cover optimizer, a logarithmic interval decision procedure, +a test of global scientific status, or an independent proof reviewer. The earlier +two-coordinate counterexample is correctly not certified. The proof of log3>1 +is 2*integral_0^(1/2)1/(1-t^2)dt>1, so the cap test is also exact. + +## 6. Review and attribution + +Review (T3)'s ratio exponents, the demand and probability conditions, (T6)'s +inequality direction, zero-price completeness, and the distinction between the +specified cover threshold and whole-ground colorability. Finite tests compare +the local recursion with subset enumeration and preserve the earlier counterexample. +They do not establish independent analytic acceptance. + +Primary-source reconnaissance on 24 September 2026 inspected Park–Pham, +*A Proof of the Kahn–Kalai Conjecture*, arXiv:2203.17207 abstract, and +Gunby–He–Narayanan, *Down-set thresholds*, arXiv:2112.08525 abstract. +These are neighboring threshold results, not inputs to (T1) and not evidence of +novelty. The proof here uses the named in-project sources and the explicitly derived +elementary inequalities. No theorem from those abstracts is imported. diff --git a/formal/sources/p15_v1/three_fronts_20260924_P15_PRICE_BOUNDARY.md b/formal/sources/p15_v1/three_fronts_20260924_P15_PRICE_BOUNDARY.md new file mode 100644 index 000000000..1d6946658 --- /dev/null +++ b/formal/sources/p15_v1/three_fronts_20260924_P15_PRICE_BOUNDARY.md @@ -0,0 +1,43 @@ +# Why the realized-cover theorem cannot simply use every transformed price + +**Object:** P15-PRICE-BOUNDARY-20260924-v1. Author: OpenAI / ChatGPT. +This is an exact counterexample to one proposed extension, not to P15-B or to +an unrestricted large-palette theorem. + +The realized-cover theorem deliberately assumes c_v<=p_v. Consider its smallest +one-block member: a_1=d_1=1, X={x,y}, no macro edges. Its good sets are the empty +set and singletons, its palette optimum is K_H(d)=1, and its one-piece obstruction +is exactly {X}. The prescribed cover is {{x,y}}. + +Take independent original probabilities p_x=p_y=1/2 and prices c_x=c_y=2/3. +These are admissible TRANSFORMED prices: phi(1/2)=log 2>2/3. For example, + + log 2=2 integral_0^(1/3) 1/(1-t^2) dt > 2/3. + +Nevertheless mu_p(D)=3/4, and + + min(1,-log mu_p(D))=log(4/3)<1/3, + +using log(1+x)0. Every cover of the obstruction {X} must contain a +generator g subset X. The possible generator costs are1,2/3,2/3,4/9 for the empty +set, the two singletons, and X respectively. Additional nonnegative-price +generators cannot reduce the minimum. Therefore the EXACT optimal cover price is + + covercost_c(O_1(D))=4/9 > 1/3 > log(4/3). + +Thus replacing c<=p by c<=phi(p) in the realized-family theorem while keeping its +same palette K_H(d) is FALSE in general, even if arbitrary alternative covers +rather than the prescribed cover are permitted. This is stronger than merely +saying that the existing proof does not establish the extension. + +It does not contradict the original P15-B amalgamation: that source separately +requires each local cover to meet its local phi(q_i) budget, which fails here. +It also does not refute a theorem allowing more colors: with two colors this +particular whole ground set is properly colorable, the obstruction is empty, +and the empty family has price zero. No conclusion about the original408-scale +or unrestricted prize follows from a one-color counterexample. + +The accompanying three finite tests enumerate all generator families on the +actual two-coordinate ground set, compute the product-measure probability exactly, +and check the rational comparisons used above. The two elementary logarithm +inequalities are proved in this note, not replaced by floating-point evaluations. diff --git a/formal/sources/p15_v1/three_fronts_20260924_P15_REALIZED_COVERS.md b/formal/sources/p15_v1/three_fronts_20260924_P15_REALIZED_COVERS.md new file mode 100644 index 000000000..173881916 --- /dev/null +++ b/formal/sources/p15_v1/three_fronts_20260924_P15_REALIZED_COVERS.md @@ -0,0 +1,140 @@ +# P15: actual-coordinate realizations with nonempty covers and exact palette demand + +**Object:** P15-REALIZED-COVERS-20260924-v1. +**Author:** OpenAI / ChatGPT. **Disposition:** author-side mathematical derivation; no unrestricted prize closure or independent review. + +## 1. The source interface, not a substitute hypergraph + +The original source is P15-B, `P15-B_PALETTE_SEPARATED_LOCALIZATION.md`, Drive `19D-eHQAIXMGGy2ThZUfZ0GGjIKWm5C2j`, 6286 bytes, SHA256 `9b18b6e9abc90d18deef06ab12e3aa7794dad40e1618d99daa88e369c300e8c3`. It was read in full. P15-B requires ACTUAL local restrictions, compatible local covers at the same original-coordinate prices, and palette separation on EVERY crossing minimal original forbidden set. Main issues59/61 and the later consecutive-palette construction left that application check open in general. + +This note supplies an explicit, nontrivial family for which all those inputs are proved, including NONEMPTY local generator covers. It does not claim that every existing P15 downset belongs to this family or that the previous abstract examples already specified these original coordinates. The price range is deliberately stated as 0<=c_v<=p_v, a subset of P15-B's possible transformed-price range c_v<=phi(p_v). No assertion is made here for the additional prices p_v=1; removing a vertex leaves a proper subset of e, which contains no H-edge by the clutter property. Thus it is minimal. Conversely, any bad set either exceeds a local capacity and contains a set in (a), or has support containing an H-edge and contains a transversal from (b). This proves completeness, not just existence of some witnesses. + +In particular the crossing-support hypergraph is EXACTLY H, and the actual local restriction is + + D_i=D intersect 2^(X_i)={S subset X_i: |S|<=a_i}. (P2) + +The restriction does not inherit an artificial stronger condition. Neither a sampled list of transversals nor an incomplete lifting can replace (b). + +## 3. Real, positive-price local obstruction covers + +The k-fold decomposability of a capacity family is exact: + + I_k(D_i)={S:|S|<=a_i k}. + +Necessity follows by summing the k capacities; sufficiency partitions S into successive groups of at most a_i elements. For k=d_i and n_i=a_i d_i+1, the only obstructed subset of X_i is X_i itself. Hence + + G_i={X_i} (P3) + +is an exact local obstruction cover. It is not the empty family arising from proper colorability of the entire block with d_i colors. + +Select the ORIGINAL coordinates independently with arbitrary probabilities p_v in [0,1], and let 0<=c_v<=p_v. With q_i=P(U_i notin D_i), + + price(G_i)=product_(v in X_i)c_v + <=product_(v in X_i)p_v + =P(U_i=X_i)<=q_i<=phi(q_i), (P4) + +where phi(t)=min(1,-log(1-t)), phi(1)=1. When all c_v>0 the local price is positive. When a zero price occurs the generator is still retained for setwise coverage. + +The independent-block calculation uses (P2), so + + mu_p(D)<=product_i(1-q_i), + sum_i price(G_i)<=sum_i q_i + <=-log(product_i(1-q_i))<=-log mu_p(D). (P5) + +If some q_i=1 the trivial price-one cover handles the endpoint. When the summed price exceeds1 use {empty set}; otherwise retain union_i G_i. This produces the capped hazard bound whenever the palette condition below holds. Crossing events are not declared independent, and no coordinates are cloned. + +## 4. The exact number of colors needed for this cover + +Let K_H(d) be the minimum size K of an integer palette universe admitting subsets P_i with |P_i|>=d_i and + + intersection_(i in e) P_i = empty, for every e in H. (P6) + +Equivalently each label's incident macro-indices form an independent set of H. By discarding excess labels within blocks, one may take |P_i|=d_i. This is the actual macro-demand coloring problem; fractional palettes are not used. + +**Theorem P2.** For D in (P1), the fixed family G={X_1,...,X_b} covers O_K(D) if and only if + + K>=K_H(d). (P7) + +For sufficiency take a set U avoiding all generators. Then |U_i|<=a_i d_i. Split U_i into at most d_i groups of size<=a_i and assign them distinct labels from P_i. A global label's block support is H-independent by (P6), and it uses at most a_i vertices in each block. Each resulting color class is in D. Thus U is K-decomposable. + +For necessity choose U with |U_i|=a_i d_i in EVERY block, omitting one original vertex per block. It avoids every generator X_i. Any D-coloring of U needs at least d_i distinct colors in block i because of its capacity a_i. If a label occurs in every block of an H-edge, completeness of the transversal forbidders makes that label class bad. Thus its used-color sets form palettes satisfying (P6); at least K_H(d) colors are necessary. For K=K_H(d), + + covercost_c(O_K(D)) <= min(1,-log mu_p(D)). (P8) + +Optimality in (P7) is for the SPECIFIED union-of-block-generators cover. It does not prove that no different cover with the same budget works at fewer colors. It is not unrestricted prize optimality. + +For comparison, the chromatic number of the ENTIRE ground set X is K_H(d+1), because ceil(n_i/a_i)=d_i+1. The same palette argument gives both inequalities. Therefore cover demand and whole-ground colorability are distinct quantities. + +## 5. Realized structural subclasses + +For any H whose independent sets form a loopless matroid, the established matroid palette formula in main issue59 can be applied to this actual family. It is not necessary to establish a new matroid theorem here. For a consecutive-capacity presentation, the corresponding consecutive-palette theorem can similarly be consumed only when its exact complete-support hypotheses hold. + +A fully elementary case is H consisting of all (s+1)-subsets of b indices, 1<=s<=b. Each label may occur in at most s blocks, and + + K_H(d)=max(max_i d_i, ceil(sum_i d_i/s)). (P9) + +The two lower bounds follow from one block and from total label incidences. For the matching construction, concatenate segments of lengths d_i along the cyclic word 0,1,...,K-1. Each block has distinct labels because d_i<=K. Each label occurs at most ceil(sum d_i/K)<=s times. This proves (P9) without enumerating individual labels when demands are large. + +The macro triangle at unit demands needs3 colors, although a formula considering only size-two edge loads would give2. The theorem uses K_H itself or a proved structural method, not an unrestricted edge-load formula. + +## 6. A nonempty-cover realization of the 816-label benchmark + +Take six blocks, a_i=1 and d_i=408. Thus EACH original block has409 vertices and the original ground set has2454 vertices. H consists of all15 four-block subsets. Every D-color class contains at most one vertex per block and occupies at most three blocks. + +The original minimal forbidders are exactly + + 6*binom(409,2)=500616 internal pairs, + 15*409^4=419743994415 crossing transversal quadruples. (P10) + +These are counts obtained from a proved complete structural formula, not a claim that the program enumerated more than four hundred billion sets. + +Use408 labels on macro-indices {0,2,4} and408 different labels on {1,3,5}, giving + + K_H(408,...,408)=816. + +The actual cover has six generators, the six FULL409-vertex blocks. At816 colors it covers the obstruction; at815 it does not, because omitting one vertex from each block leaves2448 vertices, each color holds at most3, and815*3<2448. Pairwise-disjoint local palettes would have used2448 labels. The whole ground set, unlike the cover-avoiding sets, needs818 colors, since2454/3=818. + +This is a NEW specified original-coordinate family instantiating the previous abstract benchmark; it is not a statement that every earlier six-block application had409 vertices per block or these complete transversals. + +A concrete low-failure, positive-price instance is p_v=c_v=1/40900. The cover price is exactly + + 6/(40900^409)>0. + +A union bound on internal pairs and four-block occupancy gives + + Q=1-mu_p(D) + <=500616/(40900^2)+15/(100^4) + =2449227/8180000000 < 3/10000. (P11) + +For the second term each block's occupancy probability is at most409p=1/100, and occupancies of distinct blocks are independent. This is only a union bound, not an equality of the global bad probability. Thus the hazard budget is not being satisfied solely in the trivial high-failure regime; the actual-good probability exceeds0.9997. The cost comparison (P5) supplies (P8), rather than comparing this positive price to an unproved numerical hazard lower bound. + +## 7. Exact verification and boundaries + +The executable finite checker constructs actual block coordinates for small cases. It independently enumerates minimal bad subsets, tests equality with (a)-(b), computes actual restrictions, compares original-coordinate colorability with residual-demand dynamic programming, and checks every cover-avoiding subset in declared bounded examples. A removed transversal is a negative control: its now-good original set still violates the macro support condition, so incomplete lifting is detected. The large816 example uses the proved formulas (P9)-(P11), not an unbounded enumeration. + +The original P15-D source (Drive `1z-vrL-f5tDBbqybco-ZiS7X9vJq70ifA`) was also read. It treats complete GRAPH-transversal coupling, arbitrary macro chromatic number and a different scalar/hazard budget. This note does not improve its256 factor or extend it to arbitrary hypergraphs at the same fixed palette. It supplies a separate actual-realization theorem whose palette remains K_H(d). + +The unrestricted P15 prize, full transformed-price range, arbitrary input support identification, and nonauthor review remain open. Classical coloring, hypergraph demand coloring, union bounds and the source P15-B amalgamation are not claimed as inventions. The contribution supplied here is the exact compatible original-coordinate family, nonempty covers, and source-hypothesis verification that were absent from a merely abstract palette output. diff --git a/tests/test_formal_gate.py b/tests/test_formal_gate.py index 0b36e5139..1b907ae18 100644 --- a/tests/test_formal_gate.py +++ b/tests/test_formal_gate.py @@ -328,7 +328,7 @@ def test_real_manifest_source_check(self): self.assertEqual(m["formalization_status"], "proved") self.assertEqual(m["alignment_status"], "PENDING_INDEPENDENT_REVIEW") self.assertIs(m["scientific_status_authority"], False) - self.assertEqual(len(m["targets"]), 31) + self.assertEqual(len(m["targets"]), 59) self.assertEqual(m["dependency_revisions"], {}) self.assertEqual((ROOT / "formal/ALIGNMENT.md").read_text(), gate.render_alignment(m))