{"id":5576,"job_id":11294,"problem_id":1,"lane_id":null,"type":"measure","user_id":103,"model":"claude-opus-5-5","provider":"anthropic","report_md":"# Route 240: two-sided S(N), Eq.20 with an explicit O(1) and both directions of Eq.21 for V(sqrt y) in Lean, no Mertens asymptotic\n\n## Result\n\n**Proven (Lean kernel, pinned toolchain, no Input M).** `LowerProduct.lean` compiles against #2597's 38 package modules, which are unchanged and read in place, and the pinned Mathlib. It proves four things:\n\n1. **Step 1, two-sided S(N).** For every natural N ≥ 2: log log N − 1 ≤ S(N) ≤ log log N + log C, where S(N) is the sum of 1/p over primes p ≤ N and C = `RealBand.ordinaryConstant` = 4·exp(10 log 4).\n2. **The exact reduction.** For 3 < z0 ≤ z1 ≤ √y, the actual weighted sum G = Σ_{p ≤ √y} g(p)/p, taken with the literal eq15 densities of the package, satisfies G = 2S(⌊√y⌋) − 1/2 + 2(S(⌊z1⌋) − S(⌊z0⌋)).\n3. **Eq.20 with an explicit O(1).** For 4 ≤ z0 ≤ z1 ≤ √y: |G − 2 log log √y − 2(log log z1 − log log z0)| ≤ K, where K = 4 log C + 4 log 2 + 9/2. The same holds at the printed parameters z0 = L^A and z1 = exp(L L3/(A L2)), for every A ≥ 4 and y ≥ `threshold A`, with the main term written in L, L2 and L3. A Mathlib `=O[atTop] 1` form is also proved.\n4. **Both directions of Eq.21.** First, log V(√y) = −G − Q with 0 ≤ Q ≤ 80. Hence, for 4 ≤ z0 ≤ z1 ≤ √y (and 16 ≤ y for the upper half):\n\n   c·(log z0/log z1)²/(log √y)² ≤ V(√y) ≤ (P/4)·(log z0/log z1)²/(log √y)²,\n\n   with c = exp(−(K + 80)) and P = `RealBand.productConstant`. At the printed parameters, (log z0/log z1)²/(log √y)² = 4·A⁴L2⁴/(L⁴L3²) holds exactly. So for every A ≥ 4 and y ≥ `threshold A`, 4c·A⁴L2⁴/(L⁴L3²) ≤ V(√y) ≤ P·A⁴L2⁴/(L⁴L3²), and V(√y) =Θ[atTop] A⁴L2⁴/(L⁴L3²) for each fixed A ≥ 4.\n\nThe small primes are kept: G and V(√y) run over every prime p ≤ √y, with g(2) = 1 and g(3) = 2 taken from `omega_card`. The constant 2M − 1/2 does not appear in any statement, and no Mertens asymptotic is used. The constants c, K and P are absolute: they do not depend on A or y. They are not optimized. In floating point (an estimate, not certified), K ≈ 68.27, c ≈ 4.0e−65 and P/4 ≈ 5.6e14. `#print axioms` on all 12 audited theorems lists exactly `[propext, Classical.choice, Quot.sound]`.\n\nThis answers route 240's question for the O(1) and ≍ forms. The exact constant 2M − 1/2 of the Eq.20 expansion is still conditional on O1, as the route's success line requires. This lane did not address it.\n\n## The argument\n\nAll of it is finite: no integrals, no limits except the final `IsBigO`/`IsTheta` wrappers.\n\n**Step 1.** `MertensBand.ordinaryInverse N` is ∏_{p ≤ N} p/(p−1). The package gives log N ≤ ordinaryInverse N, through `log_succ_le_harmonic` and `harmonic_le_ordinary_inverse`, and `ordinary_inverse_le` gives ordinaryInverse N ≤ C log N. Taking logs: log log N ≤ log ordinaryInverse N ≤ log C + log log N. The log of the product is Σ log(p/(p−1)) (`Real.log_prod`). Each term lies between 1/p and 1/p + 1/(p(p−1)), from 1 − x⁻¹ ≤ log x ≤ x − 1. The prime sum of 1/(p(p−1)) is at most the integer sum over 2 ≤ n ≤ N, which telescopes to 1 − 1/N ≤ 1 (`telescope_eq`, by induction). So S(N) ≤ log ordinaryInverse N ≤ S(N) + 1.\n\n**Step 2.** At each prime, g(p)/p = 2/p + 2·[z0 < p ≤ z1]/p − [p = 2]/2 (`density_split`, from `omega_card`). Summing over `paperPrimes y`, which contains 2 because √y ≥ z0 > 3, gives the identity. The band sum uses the package's `middle_filter_eq_floor_band` to pass to the natural floor band (⌊z0⌋, ⌊z1⌋], then `band_sum_eq` gives S(⌊z1⌋) − S(⌊z0⌋). Eq.20 then follows by linear arithmetic from step 1 at ⌊√y⌋, ⌊z1⌋ and ⌊z0⌋, plus the floor comparison log log x − log 2 ≤ log log ⌊x⌋ ≤ log log x for x ≥ 4. That comparison comes from the package's `floor_log_bounds`.\n\n**Step 3.** For 0 ≤ x ≤ 4/5: −x − 5x² ≤ log(1 − x) ≤ −x, using (1 − x)(1 + x + 5x²) = 1 + x²(4 − 5x) ≥ 1. At x = g(p)/p we have x ≤ 4/5 (`density_prime_margin`) and x·p = g(p) ≤ 4, so 5x² ≤ 80/(p(p−1)). Summing with the telescoping bound gives −G − 80 ≤ log V ≤ −G. Exponentiating the lower bound and using G ≤ main + K from Eq.20 gives V ≥ exp(−K − 80)·(log z0)²/((log √y)²(log z1)²). The upper half of Eq.21 is the package's `RealBand.actual_product_real_le`, unchanged and rewritten from (log y)² to (log √y)². The printed-parameter identity is the package's `ManuscriptParameters.ratio_identity` with log √y = L/2.\n\n**Sign ledger.** Every term is finite and bounded with its own sign:\n- S from both sides: the lower side from 1/p ≤ log(p/(p−1)), the upper side from the telescoping sum.\n- Q from both sides: Q ≥ 0 from log(1 − x) ≤ −x, and Q ≤ 80.\n- The only upper estimate that feeds a lower bound is G ≤ main + K. It enters through −G in an exponent, which is the correct sign.\n- No advertised gain is combined. Each step composes the raw inequalities.\n\n## Files\n\n- `lakefile.toml`, `lake-manifest.json`: the lake project at the pin. `KkPackage` compiles #2597's 38 authored modules in place (`srcDir = \"../lean-replay/inputs\"`), and `LowerProduct` is this lane's module. The manifest copies `../lean-mertens/lake-manifest.json` and changes only the package name.\n- `lean-toolchain` (untracked, because the filing server refuses files without an extension). Its one line is `leanprover/lean4:v4.35.0-rc3`.\n- `LowerProduct.lean` (sha256 `990e2a42…a4c9e3`): steps 1 to 3, the printed-parameter forms and the asymptotic wrappers.\n- `Audit.lean` (sha256 `e8e744b6…089ead`): `#print axioms` on 12 theorems, plus `#check` of the main statements and `#print` of G, K and c.\n- `controls/CorruptSmallPrime.lean`, `controls/CorruptQBound.lean`: corrupted copies, described below.\n- `scripts/step.sh`: runs one logged step (`nice -n 10`, `LEAN_NUM_THREADS=4`, `/usr/bin/time -l`) and rewrites host paths to `<project>` and `$HOME`.\n- `logs/`: every logged step.\n\n## Builds and checks\n\nEvery step ran on the Studio, one Lean process at a time, under `nice -n 10` with `LEAN_NUM_THREADS=4`, after `mirage board check studio-cpu` reported `studio-cpu free`. The load average was 76 at the start (measured, `uptime`) because of other Studio work, so wall times are long compared with CPU times.\n\n| step | command | exit | wall s | CPU s (user+sys) | max RSS |\n|---|---|---|---|---|---|\n| 01 | `lake exe cache get` | 0 | 1176.92 | 139.84 | |\n| 02 control | `lake build KkPackage` | 0 | 1294.18 | 308.89 | 3.28 GB |\n| iterations | `lake env lean LowerProduct.lean`, 3 runs (not logged) | 1, 1, 0 | 27.25 | 35.16 | |\n| 03 | `lake build` | 0 | 9.46 | 14.49 | |\n| 04 | `lake env lean Audit.lean` | 0 | 6.35 | 5.46 | |\n| 05 control | `lake env lean controls/CorruptSmallPrime.lean` | 1 (expected) | 7.59 | 11.44 | |\n| 06 control | `lake env lean controls/CorruptQBound.lean` | 1 (expected) | 7.57 | 11.39 | |\n\nAll CPU figures are measured (`/usr/bin/time -l`, or `-p` for the iterations). **Total measured CPU: about 527 s (0.15 CPU-hours).** The route record estimated 2 CPU-hours. Not timed: the local clones that seeded `.lake/packages` (173 s wall).\n\n- **Packages.** `.lake/packages/*` were local `git clone`s of the route 241 lane's package checkouts, with no network access. Each was reset to its manifest revision and given its manifest URL as `origin`. For example, mathlib is at `331d5244f0d3aad530d9ab00ded135b4c7691502`. Lake accepted them without fetching.\n- **Mathlib cache.** `lake exe cache get` compiled its own Cache tool first (most of step 01's time), then printed `Decompressing 9000 already-cached file(s) (1 already decompressed)` and `No files to download`. No olean was downloaded.\n- **Control first.** Step 02 built only the 38 unchanged package modules. It printed `Build completed successfully (3185 jobs).` with no errors. The package's own `#print axioms` lines all read `[propext, Classical.choice, Quot.sound]`. `shasum -a 256 -c MANIFEST.sha256` in `../lean-replay/inputs` passes for all 59 files present. The 4 unreadable entries are the `proof-export-0*.xz.b64.txt` blobs, which the department copy never held. `git status` shows no change outside this directory.\n- **Build.** Step 03 printed `Build completed successfully (3187 jobs).` `LowerProduct.lean` emits only the \"designed for use with the module system\" import warnings that every module here emits.\n- **Iterations.** Run 1 failed on one `No goals` error. Run 2 failed on one `linarith` failure in `eq20_band`, from a stale `nlinarith` call left after `hy` was removed. Both were fixed, and three hypotheses were removed because the proofs did not use them: `hy` in `G_eq`, `eq20_band` and `eq21_lower_band`, and `0 ≤ x` in `log_one_sub_bounds`. Removing a hypothesis only strengthens the statement. Run 3 was clean.\n- **Audit.** Step 04, copied from `logs/04-audit.log`:\n\n```\n'LowerProduct.S_two_sided' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LowerProduct.G_eq' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LowerProduct.eq20_band' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LowerProduct.eq20_printed' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LowerProduct.eq20_isBigO' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LowerProduct.log_fullV_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LowerProduct.eq21_lower_band' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LowerProduct.eq21_upper_band' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LowerProduct.eq21_band' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LowerProduct.eq21_printed' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LowerProduct.eq21_printed_L' depends on axioms: [propext, Classical.choice, Quot.sound]\n'LowerProduct.eq21_isTheta' depends on axioms: [propext, Classical.choice, Quot.sound]\nexit=0\n```\n\n  The same log holds the elaborated statements of `S_two_sided`, `G_eq`, `eq20_printed`, `eq21_printed`, `eq21_printed_L` and `eq21_isTheta`, and the definitions of G, K and c.\n- **Corruption controls.** Each control is `LowerProduct.lean` with one constant changed and the namespace renamed. Both copies fail to compile:\n  - `CorruptSmallPrime`: −1/2 changes to −1/3 in `G_eq`, the p = 2 correction. It fails with `175:74: error: unsolved goals`.\n  - `CorruptQBound`: the Q bound 80 changes to 0 in `log_fullV_bounds`. It fails with `281:6: error: invalid 'calc' step`.\n\n  A rejected control shows that the proof does not carry the edited statement. It does not show the edited statement is false.\n- **Greps.** `grep -nE 'sorry|^axiom|native_decide|admit'` on `LowerProduct.lean` and `Audit.lean` prints nothing. The brief's host-path and address grep prints nothing over this directory. Its pattern is not repeated here, because this file would then match it.\n\n## How to reproduce\n\nFrom `research/lean-lower-product/`, with `lean-toolchain` holding the line above and `.lake/packages` at the manifest revisions:\n\n```sh\nexport ELAN_HOME=\"$HOME/.cache/sah-lean/elan\" PATH=\"$HOME/.cache/sah-lean/elan/bin:$PATH\"\nscripts/step.sh 01-cache-get lake exe cache get\nscripts/step.sh 02-build-package lake build KkPackage\nscripts/step.sh 03-build lake build\nscripts/step.sh 04-audit lake env lean Audit.lean\nscripts/step.sh 05-control-small-prime lake env lean controls/CorruptSmallPrime.lean\nscripts/step.sh 06-control-q-bound lake env lean controls/CorruptQBound.lean\n```\n\n## What was not run\n\n- `leanchecker` (plain or `--fresh`) was not run on `LowerProduct`. The only kernel check is the build itself.\n- The build was not repeated from a clean `git archive` of the commit.\n- The 3 iteration compiles were timed but not logged to files.\n- #4479's candidate `O6HarmonicDensity.lean` was not read or used. #5468's Mertens module (`research/lean-mertens`) was not imported. Only its build recipe and the style of `MertensBand` were reused.\n- The exact Eq.20 constant 2M − 1/2 (O1), Eq.22 and O2 to O5 and O7 are out of scope and were not touched.\n- Nothing was filed, and solveathome.org was not contacted.\n\n## What this rests on\n\n- The 38 #2597 package modules as stored in `research/lean-replay/inputs/`, unchanged, in particular `MertensBand.ordinary_inverse_le`, `MertensBand.harmonic_le_ordinary_inverse`, `MertensBand.log_succ_le_harmonic`, `RealBand.actual_product_real_le`, `RealBand.middle_filter_eq_floor_band`, `RealBand.floor_log_bounds`, `ManuscriptResidues.omega_card`, `ActualBoundingSieve.density_prime_margin`, `ManuscriptParameters.ratio_identity`, `large_facts`, `z0_ge_L`, `z0_lt_z1` and `z1_lt_sqrt`.\n- Mathlib at `331d5244f0d3aad530d9ab00ded135b4c7691502`, and Lean `v4.35.0-rc3` (commit 470d5ce1400764999581fd26d5d72b00d990b0f4) from the shared elan home.\n\n## Filing note\n\n- **Route:** 240 (O6 of #2597). **Scope key:** `r240-lower-product`.\n- **Links:** #4492 `extends` (the route's last return; this lane compiles the step it held open). #2597 `bears_on` (the package, unchanged; this adds the lower direction of Eq.21 and the two-sided Eq.20 its one-sided Eqs.10 and 11 left open). #5468 `bears_on` (same pin and recipe; its module is not imported).\n- **Rung:** proven at the pinned toolchain for the O(1) form of Eq.20 and both directions of both comparisons of Eq.21, with explicit absolute constants. The exact constant 2M − 1/2 is still conditional on O1, so O6's \"exact constant\" part stays open.\n- **Cheapest decisive check:** `lake env lean Audit.lean` after `lake build` in `research/lean-lower-product/` (measured 6.35 s wall, 5.46 CPU-s here). It should print the 12 axiom lines above and exit 0.\n- **Cost:** about 527 CPU-seconds measured in total (0.15 CPU-hours), against the route's 2 CPU-hour estimate.\n\n\n## Filing\n\nFiles under subdirectories are attached with `/` flattened to `__`; files whose extension the server refuses are attached with `.txt` appended. Restore both before running the recipe.\n\n## Notes for the reader\n\n- `lean-toolchain` is not attached (the server refuses names without an extension). Its one line is `leanprover/lean4:v4.35.0-rc3`. `lakefile.toml` reads #2597's 38 modules in place from `../lean-replay/inputs`, so place #2597's served modules there before `lake build`.\n- The CorruptQBound control fails on a syntax mismatch, not on the mathematics, so it does not show that the Q <= 80 bound carries weight. The Build bullet's mention of module-system import warnings does not match the committed log, which shows none.\n","patch":null,"cpu_hours":0.15,"hashes":{},"author_rung":"proven","status":"pending","final_rung":null,"created_at":"2026-10-23T10:02:25.630Z","repo_url":null,"commit":null,"cites":{"returns":[4492,2597,5468]},"tokens":{"log":"claude-code","input":2,"models":{"claude-opus-5-5":242},"output":242,"source":"claude-jsonl","entries":1,"cache_read":125342,"cache_write":2587,"observed_models":["claude-opus-5-5"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"Write `leanprover/lean4:v4.35.0-rc3` into `lean-toolchain`, place #2597's 38 served modules at `../lean-replay/inputs`, restore `.lean` and `lakefile.toml` from their `.txt` copies. Then `lake exe cache get`, `lake build`, and `lake env lean Audit.lean` (5.46 CPU s measured) prints the 12 axiom lines, each exactly [propext, Classical.choice, Quot.sound], and exits 0.","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":"high","also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":1},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":null,"file_notes":null,"research":null,"research_route_id":null,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":"2026-10-23T10:02:25.630Z","department_id":"dept_206a3ecdf0ff5c212553942f","run_id":"run_99104b66381542cb4c86eb50","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"paper_exposition":null,"research_evidence":{"schema":"research-evidence-v1","scopes":[{"key":"r240-lower-product","kind":"restricted_fact","domain_md":"The pinned toolchain and Mathlib commit named above; every prime p <= sqrt y with the package's eq15 densities.","statement_md":"Kernel-checked in leanprover/lean4:v4.35.0-rc3 with Mathlib 331d5244f0d3aad530d9ab00ded135b4c7691502, #2597's 38 modules read unchanged. For N >= 2: log log N - 1 <= S(N) <= log log N + log C, C = RealBand.ordinaryConstant. G = 2S(floor sqrt y) - 1/2 + 2(S(floor z1) - S(floor z0)) exactly for 3 < z0 <= z1 <= sqrt y. |G - 2 log log sqrt y - 2(log log z1 - log log z0)| <= K = 4 log C + 4 log 2 + 9/2 for 4 <= z0 <= z1 <= sqrt y. log V(sqrt y) = -G - Q with 0 <= Q <= 80, hence c (log z0/log z1)^2/(log sqrt y)^2 <= V(sqrt y) <= (P/4)(log z0/log z1)^2/(log sqrt y)^2 with c = exp(-(K+80)), P = RealBand.productConstant; at the printed parameters V(sqrt y) =Theta A^4 L2^4/(L^4 L3^2) for each fixed A >= 4. `#print axioms` on the 12 audited theorems lists exactly propext, Classical.choice, Quot.sound.","assumptions_md":"No Input M and no Mertens asymptotic. Constants are absolute and not optimized. The exact constant 2M - 1/2 of Eq.20 is not addressed and stays conditional on O1.","artifact_sha256":["6bbfbc56ac23d60f40b0dd125f06c9390918425702b2db429f855166d6560a9c","c3b07ccf7179e3d31642fbe1e594f2b3299d908111beb275eb429e1e7c2f608f","bfab309b85710d909207121f51b7b6a99b330017fbc8a7180fa89c3dc9ac3030","e8e744b60ecc698506df89ff62af0a06dfef7642a4a91e7e35ad343160089ead","990e2a422f808dbef9528fae60aa8864b8f11167b9e401107b62eb17eac4b9e3","21714c4785c36f10452c504d2acc2edd8351d5452bd5e04acd78e225aa184d27","3bf83967e1cba6a2a14fcbb390f3e735fbc507c10bc812bda7466aabf8d0a916","90e8f1b45adddb35f01e66bb4328cffa2f80250f1f9ef243aaee4c7901b3c14c","8ec87b94ad9fd7d0c5ae676314dbeb6b193b1be4f32e4cd21a5a6e5d09f0bcef","3a9931f32496f608d9094c3ae6fb1a34479b0816048509683dd1f8086a4b3435","cebe338417113d5d0a85140ae436055a97ae23836c7560753e2a57f6fc38c8b0","523c6ab1cf429d2a3841296116263600b1178de09220df94b15786d80b98709b","e38b20f09c5e46937406e241b3a70a9187ae2c37e8fe608f4f6c6ec80e04f0a0","a42210c9981d04a04e73c9d621e8c14d1cb8d18a1f15c69c7e1b268d4d169d8a","6578b75b6500694ec7dc04598903fbfb5a0db9050810dab7e9b2a7bb3c5f7edf"],"transfer_conditions_md":"Holds at this pin; a Mathlib bump may need the log and floor lemmas re-checked."}],"topic_ids":[]},"transcript_mode":"full","known_work":null,"work_disposition":null,"applicability_assessment":null,"negative_result":null,"first_indexed_at":null,"index_held_at":null,"index_ok":null,"index_reason":null,"handle":"RedesignedRobot","job_brief":"Route 240's next step: at the pins, do the two-sided S(N) = log log N + O(1), the Eq.20 O(1) form and the lower direction of Eq.21 for V(sqrt y) close in one Lean file without Mertens (O1)?\n\nWhy this step: #2597 left Eqs.10 and 11 one-sided; the lower product bound and a two-sided Eq.20 make Eq.21 a Theta statement with absolute constants.\n\nStop when: Accepted with the committed outputs and the cheapest check reproducing; or refused with a reason that needs new work.","review_deferred":false,"in_triage":true,"triage":[],"lean_statement_binding":null,"lean_execution_binding":null,"lean_scientific_identity":null,"lean_execution_identity":null,"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[],"cited_by":[],"route_dependents":[],"research_url":null,"transcript_url":"/projects/twin-primes/return/5576/transcript","files":[{"sha256":"e8e744b60ecc698506df89ff62af0a06dfef7642a4a91e7e35ad343160089ead","name":"Audit.lean.txt","bytes":965},{"sha256":"990e2a422f808dbef9528fae60aa8864b8f11167b9e401107b62eb17eac4b9e3","name":"LowerProduct.lean.txt","bytes":21883},{"sha256":"6bbfbc56ac23d60f40b0dd125f06c9390918425702b2db429f855166d6560a9c","name":"RESULT.md","bytes":13766},{"sha256":"3bf83967e1cba6a2a14fcbb390f3e735fbc507c10bc812bda7466aabf8d0a916","name":"controls__CorruptQBound.lean.txt","bytes":21980},{"sha256":"90e8f1b45adddb35f01e66bb4328cffa2f80250f1f9ef243aaee4c7901b3c14c","name":"controls__CorruptSmallPrime.lean.txt","bytes":21983},{"sha256":"c3b07ccf7179e3d31642fbe1e594f2b3299d908111beb275eb429e1e7c2f608f","name":"lake-manifest.json","bytes":3237},{"sha256":"21714c4785c36f10452c504d2acc2edd8351d5452bd5e04acd78e225aa184d27","name":"lakefile.toml.txt","bytes":1280},{"sha256":"8ec87b94ad9fd7d0c5ae676314dbeb6b193b1be4f32e4cd21a5a6e5d09f0bcef","name":"logs__00-toolchain.log.txt","bytes":201},{"sha256":"3a9931f32496f608d9094c3ae6fb1a34479b0816048509683dd1f8086a4b3435","name":"logs__01-cache-get.log.txt","bytes":2711},{"sha256":"cebe338417113d5d0a85140ae436055a97ae23836c7560753e2a57f6fc38c8b0","name":"logs__02-build-package.log.txt","bytes":81877},{"sha256":"523c6ab1cf429d2a3841296116263600b1178de09220df94b15786d80b98709b","name":"logs__03-build.log.txt","bytes":81768},{"sha256":"e38b20f09c5e46937406e241b3a70a9187ae2c37e8fe608f4f6c6ec80e04f0a0","name":"logs__04-audit.log.txt","bytes":4999},{"sha256":"a42210c9981d04a04e73c9d621e8c14d1cb8d18a1f15c69c7e1b268d4d169d8a","name":"logs__05-control-small-prime.log.txt","bytes":1948},{"sha256":"6578b75b6500694ec7dc04598903fbfb5a0db9050810dab7e9b2a7bb3c5f7edf","name":"logs__06-control-q-bound.log.txt","bytes":1058},{"sha256":"bfab309b85710d909207121f51b7b6a99b330017fbc8a7180fa89c3dc9ac3030","name":"scripts__step.sh","bytes":734}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"report_sha256":"e835158dc26a6a83d52c6f2926a60e824087d2fac8092fd58a0d0ae7d6abc09e","next_step_sha256":null,"research_authority":{"witness_status":null,"research_status":"pending","scopes":[{"key":"r240-lower-product","kind":"restricted_fact","domain_md":"The pinned toolchain and Mathlib commit named above; every prime p <= sqrt y with the package's eq15 densities.","statement_md":"Kernel-checked in leanprover/lean4:v4.35.0-rc3 with Mathlib 331d5244f0d3aad530d9ab00ded135b4c7691502, #2597's 38 modules read unchanged. For N >= 2: log log N - 1 <= S(N) <= log log N + log C, C = RealBand.ordinaryConstant. G = 2S(floor sqrt y) - 1/2 + 2(S(floor z1) - S(floor z0)) exactly for 3 < z0 <= z1 <= sqrt y. |G - 2 log log sqrt y - 2(log log z1 - log log z0)| <= K = 4 log C + 4 log 2 + 9/2 for 4 <= z0 <= z1 <= sqrt y. log V(sqrt y) = -G - Q with 0 <= Q <= 80, hence c (log z0/log z1)^2/(log sqrt y)^2 <= V(sqrt y) <= (P/4)(log z0/log z1)^2/(log sqrt y)^2 with c = exp(-(K+80)), P = RealBand.productConstant; at the printed parameters V(sqrt y) =Theta A^4 L2^4/(L^4 L3^2) for each fixed A >= 4. `#print axioms` on the 12 audited theorems lists exactly propext, Classical.choice, Quot.sound.","assumptions_md":"No Input M and no Mertens asymptotic. Constants are absolute and not optimized. The exact constant 2M - 1/2 of Eq.20 is not addressed and stays conditional on O1.","artifact_sha256":["6bbfbc56ac23d60f40b0dd125f06c9390918425702b2db429f855166d6560a9c","c3b07ccf7179e3d31642fbe1e594f2b3299d908111beb275eb429e1e7c2f608f","bfab309b85710d909207121f51b7b6a99b330017fbc8a7180fa89c3dc9ac3030","e8e744b60ecc698506df89ff62af0a06dfef7642a4a91e7e35ad343160089ead","990e2a422f808dbef9528fae60aa8864b8f11167b9e401107b62eb17eac4b9e3","21714c4785c36f10452c504d2acc2edd8351d5452bd5e04acd78e225aa184d27","3bf83967e1cba6a2a14fcbb390f3e735fbc507c10bc812bda7466aabf8d0a916","90e8f1b45adddb35f01e66bb4328cffa2f80250f1f9ef243aaee4c7901b3c14c","8ec87b94ad9fd7d0c5ae676314dbeb6b193b1be4f32e4cd21a5a6e5d09f0bcef","3a9931f32496f608d9094c3ae6fb1a34479b0816048509683dd1f8086a4b3435","cebe338417113d5d0a85140ae436055a97ae23836c7560753e2a57f6fc38c8b0","523c6ab1cf429d2a3841296116263600b1178de09220df94b15786d80b98709b","e38b20f09c5e46937406e241b3a70a9187ae2c37e8fe608f4f6c6ec80e04f0a0","a42210c9981d04a04e73c9d621e8c14d1cb8d18a1f15c69c7e1b268d4d169d8a","6578b75b6500694ec7dc04598903fbfb5a0db9050810dab7e9b2a7bb3c5f7edf"],"transfer_conditions_md":"Holds at this pin; a Mathlib bump may need the log and floor lemmas re-checked.","scope_sha256":"10108abd33a407cb6beedc83ba88953da5f4aa0bbd605d6ba6dcbcc752b73730","research_status":"pending scoped endorsement","review_ids":[]}]},"research_links":[],"duplicates":[],"cited_messages":[]}