{"id":5561,"job_id":11258,"problem_id":1,"lane_id":null,"type":"measure","user_id":103,"model":"claude-opus-5-5","provider":"anthropic","report_md":"# Route 238: Nat-indexed two-sided PNT is equivalent to #4427's piReal hPNT in Lean; NatPNT -> Eq.10 compiles sorry-free with the three standard axioms\n\n## Result\n\n**Proven (kernel-checked, conditional on one named hypothesis).** In the pinned toolchain (`leanprover/lean4:v4.35.0-rc3`, Mathlib `331d5244f0d3aad530d9ab00ded135b4c7691502`), the Nat-indexed two-sided PNT\n\n```lean\n(fun n : ℕ => ((Nat.primeCounting n : ℕ) : ℝ)) ~[atTop] (fun n : ℕ => (n : ℝ) / Real.log (n : ℝ))\n```\n\nimplies the hypothesis `hPNT` of the served `O4aDyadic.dyadic_asymptotic` (return #4427), and conversely, so the two hypotheses are equivalent (`FloorAdapter.natPNT_iff_piReal`). Composing the adapter with the served theorem gives NatPNT -> Eq.10 (`FloorAdapter.dyadic_asymptotic_of_natPNT`): under the Nat-indexed PNT, `#{p prime : y/2 < p ≤ y} ~ y / (2 log y)`. `#print axioms` lists exactly `propext`, `Classical.choice` and `Quot.sound` for every new declaration and for `dyadic_asymptotic`. The served `O4aDyadicReduction.lean` compiles unchanged (sha256 `5ec2c501…` before and after) and its statement is not weakened. The sole remaining premise of Eq.10 is now a Nat-indexed two-sided PNT. No statement of that form appears in the pinned Mathlib under the search below.\n\n## Theorem statements\n\n`FloorAdapter.lean` (namespace `FloorAdapter`, `open Filter Asymptotics Topology PrimeReserveBudget O4aDyadic`):\n\n```lean\ntheorem floor_isEquivalent :\n    (fun x : ℝ => ((Nat.floor x : ℕ) : ℝ)) ~[atTop] (fun x => x)\n\ntheorem log_floor_isEquivalent :\n    (fun x : ℝ => Real.log ((Nat.floor x : ℕ) : ℝ)) ~[atTop] (fun x => Real.log x)\n\ntheorem floor_div_log_isEquivalent :\n    (fun x : ℝ => ((Nat.floor x : ℕ) : ℝ) / Real.log ((Nat.floor x : ℕ) : ℝ)) ~[atTop]\n      (fun x => x / Real.log x)\n\ntheorem piReal_of_natPNT\n    (hNat : (fun n : ℕ => ((Nat.primeCounting n : ℕ) : ℝ)) ~[atTop]\n      (fun n : ℕ => (n : ℝ) / Real.log (n : ℝ))) :\n    (fun x => (piReal x : ℝ)) ~[atTop] (fun x => x / Real.log x)\n\ntheorem natPNT_of_piReal\n    (hPNT : (fun x => (piReal x : ℝ)) ~[atTop] (fun x => x / Real.log x)) :\n    (fun n : ℕ => ((Nat.primeCounting n : ℕ) : ℝ)) ~[atTop]\n      (fun n : ℕ => (n : ℝ) / Real.log (n : ℝ))\n\n-- natPNT_iff_piReal: the hypothesis of piReal_of_natPNT ↔ the hypothesis of natPNT_of_piReal,\n-- proved as ⟨piReal_of_natPNT, natPNT_of_piReal⟩\n\ntheorem dyadic_asymptotic_of_natPNT\n    (hNat : (fun n : ℕ => ((Nat.primeCounting n : ℕ) : ℝ)) ~[atTop]\n      (fun n : ℕ => (n : ℝ) / Real.log (n : ℝ))) :\n    (fun y => ((dyadicPrimes y).card : ℝ)) ~[atTop]\n      (fun y => y / (2 * Real.log y))\n```\n\nThe hypothesis is written inline, not behind a definition, so the audited statement shows it. Its form is the one in route 238's `next_step.question` (`research/sah-state/2026-10-23/routes-100.json`, route id `\"238\"`). `dyadic_asymptotic_of_natPNT` is the one line `dyadic_asymptotic (piReal_of_natPNT hNat)`; the right-hand side `y / (2 * Real.log y)` is the served one, character for character.\n\n## Proof route\n\n`piReal x` is defined in the served module as `Nat.primeCounting ⌊x⌋₊`. So `fun x => (piReal x : ℝ)` is, by definition, the Nat-indexed count composed with `Nat.floor`. The proof uses that directly and needs no monotone sandwich:\n\n1. `hNat.comp_tendsto tendsto_nat_floor_atTop` gives `π ⌊x⌋₊ ~ ⌊x⌋₊ / log ⌊x⌋₊` along `atTop` in ℝ.\n2. `floor_isEquivalent`: `isEquivalent_of_tendsto_one` applied to Mathlib's `tendsto_nat_floor_div_atTop` (`⌊x⌋₊ / x → 1`).\n3. `log_floor_isEquivalent`: for `x ≥ 1`, `⌊x⌋₊ ≥ 1 > 0`, so `log ⌊x⌋₊ - log x = log (⌊x⌋₊ / x)` (`Real.log_div`). By continuity of `log` at 1 this tends to `log 1 = 0`. So it is `O(1)` (`Tendsto.isBigO_one`), and `O(1)` is `o(log x)` (`Real.isLittleO_const_log_atTop`). That is the definition of `log ⌊x⌋₊ ~ log x`.\n4. `floor_div_log_isEquivalent`: `IsEquivalent.div` of steps 2 and 3.\n5. `piReal_of_natPNT`: step 1, then `IsEquivalent.trans` with step 4.\n6. `natPNT_of_piReal`: compose `hPNT` with `Nat.cast` (`tendsto_natCast_atTop_atTop`) and rewrite `⌊(n : ℝ)⌋₊ = n` (`Nat.floor_natCast`).\n\n**Deviation from the route's method, disclosed.** Route 238's `next_step.method` proposes a sandwich between `Nat.floor x` and `Nat.floor x + 1` using `Nat.monotone_primeCounting`. That is not needed here, because `piReal` is already floor-indexed: no value of `π` at a non-integer argument appears, and the `+1` shift never arises. `Nat.monotone_primeCounting` is not used. A sandwich would matter for a count indexed by a real cutoff that is not literally `π ∘ floor`. The #4427 module header bounds the gap between `piReal x` and the literal real inclusive count `#{p prime : (p : ℝ) ≤ x}` by one prime. The gap is in fact zero, because a natural number `p` satisfies `(p : ℝ) ≤ x` iff `p ≤ ⌊x⌋₊` for `x ≥ 0` (`Nat.le_floor_iff`); this lane does not formalize that remark, and nothing here depends on it.\n\n## Builds and checks\n\nEvery step ran on the Studio from `research/lean-floor-adapter/` via `scripts/run.sh`, under `nice -n 10` with `LEAN_NUM_THREADS=4`, one Lean process at a time, after `mirage board check studio-cpu` reported `studio-cpu free` (07:57:50Z; the integrate-round2 hold had ended early). The load average was about 38 at the start (measured, `uptime`), from other Studio work, so wall times are long relative to CPU.\n\n| step | command | exit | wall s | CPU s (user+sys) | max RSS |\n|---|---|---|---|---|---|\n| attempt 1, 01 | `lake exe cache get` | 0 | 63.72 | 121.93 | 0.87 GB |\n| attempt 1, 02 to 05 | (failed at configuration, below) | 1 | 24.38 | 12.68 | |\n| 01 | `lake exe cache get` | 0 | 18.57 | 6.63 | 0.70 GB |\n| 02 control | `lake build O4a` | 0 | 481.35 | 219.71 | 3.27 GB |\n| 03 | `lake build` | 0 | 22.98 | 12.89 | 3.12 GB |\n| 04 | `lake env lean Audit.lean` | 0 | 15.90 | 6.13 | 3.09 GB |\n| 05 control | `lake env lean controls/FloorAdapterCorrupt.lean` | 1 (expected) | 14.14 | 6.80 | 3.12 GB |\n| 06 | `lake build` and `lake env lean Audit.lean` with the final lakefile | 0 | 18.09 | 12.34 | |\n| fetch | `git fetch --depth 1` of Mathlib at the pin | 0 | 11.10 | 0.81 | |\n\nAll CPU figures are measured (`/usr/bin/time -l`, or `-p` for step 06 and the fetch). **Total measured CPU: about 400 s (0.11 CPU-hours).** The triage estimate was 0.2 CPU-hours (`TRIAGE-2026-10-23.md`, row R238). The shallow fetches of the other eight dependency packages were not timed.\n\n- **Attempt 1.** With `roots = [\"PrimeReserveBudget\"]`, Lake stopped at `PrimeReserveBudget.lean:5:0: unknown module prefix 'PrimePowerTail'`: Lake at this pin builds only modules a library lists. The roots are now the 36-module import closure of `PrimeReserveBudget` (computed from the `import` lines of `research/lean-replay/inputs/`; the two modules outside it are `PrimaryMain` and `IntegerMainBinding`). Logs in `logs/attempt1/`.\n- **Mathlib cache.** `lake exe cache get` printed `Decompressing 9000 already-cached file(s) (1 already decompressed)` and `No files to download` in attempt 1, then `No files to download` in step 01. It did not download any oleans.\n- **Control first.** Step 02 builds only the 36 package modules and the served module. It printed `Build completed successfully (3184 jobs).` and the served file's own four `#print axioms` lines, each `[propext, Classical.choice, Quot.sound]`, matching #4427's `o4a_iso4.out`. The served file was compiled in place from `research/sah-state/2026-10-23/attachments/04427/` (lakefile `srcDir`), with sha256 `5ec2c501bcf97533ccae0f232119db84d395d39f7bcc912374de7bd817acd9e2` before (`logs/served-sha256-before.txt`) and after (`logs/served-sha256-after.txt`); that equals the served `SHA256SUMS.txt`. `O4aCorrupt.lean` in the same directory is not a root and was not built.\n- **Adapter build.** Step 03 printed `Build completed successfully (3187 jobs).` `FloorAdapter.lean` emits only the \"designed for use with the module system\" import warnings, the same kind every module here emits.\n- **Audit.** Step 04, copied from `logs/04-audit.log`:\n\n```\n'O4aDyadic.dyadic_asymptotic' depends on axioms: [propext, Classical.choice, Quot.sound]\n'FloorAdapter.floor_isEquivalent' depends on axioms: [propext, Classical.choice, Quot.sound]\n'FloorAdapter.log_floor_isEquivalent' depends on axioms: [propext, Classical.choice, Quot.sound]\n'FloorAdapter.floor_div_log_isEquivalent' depends on axioms: [propext, Classical.choice, Quot.sound]\n'FloorAdapter.piReal_of_natPNT' depends on axioms: [propext, Classical.choice, Quot.sound]\n'FloorAdapter.natPNT_of_piReal' depends on axioms: [propext, Classical.choice, Quot.sound]\n'FloorAdapter.natPNT_iff_piReal' depends on axioms: [propext, Classical.choice, Quot.sound]\n'FloorAdapter.dyadic_asymptotic_of_natPNT' depends on axioms: [propext, Classical.choice, Quot.sound]\nexit=0\n```\n\n- **Corruption control.** `controls/FloorAdapterCorrupt.lean` is `FloorAdapter.lean` with the composed statement's target changed from `2 * Real.log y` to `3 * Real.log y` (and the namespace renamed). It fails with one error, `controls/FloorAdapterCorrupt.lean:83:2: error: Type mismatch`, showing `dyadic_asymptotic (piReal_of_natPNT hNat)` has the `2 *` type. This shows the pipeline reads the statement. It does not show the `3 *` statement is false (it is, under PNT, but that is not what the control checks).\n- **Final lakefile.** A comment in `lakefile.toml` was rewrapped after step 05. Step 06 rebuilt (`Build completed successfully (3187 jobs).`, FloorAdapter replayed) and re-ran the audit with the committed lakefile (sha256 `3e25bd98…`), with the same eight lines and exit 0 (`logs/06-final.log`).\n- **Greps.** `grep -nE 'sorry|^axiom|native_decide'` on `FloorAdapter.lean`, `Audit.lean` and `controls/FloorAdapterCorrupt.lean` prints nothing. The brief's host-path and address grep over the committed files prints nothing; its pattern is not repeated here, because this file would then match it. Host paths in the logs were rewritten to `<project>` and `$HOME` by `scripts/run.sh` after each run. Trailing whitespace was then stripped from the logs so that `git diff --check` is clean; no other edit was made to them.\n\n## Search for a PNT in the pinned Mathlib\n\n`grep -rlnE \"primeCounting.*(~\\[|IsEquivalent|isEquivalent)|(~\\[|IsEquivalent).*primeCounting\" Mathlib` at `331d5244` prints nothing. The theorems about `primeCounting` in `Mathlib/NumberTheory/` that mention a limit or an asymptotic class are `Nat.tendsto_primeCounting'`, `Nat.tendsto_primeCounting` (`π → ∞`) and `primeCounting_sub_theta_div_log_isBigO` in `Chebyshev.lean`. So no two-sided PNT for `Nat.primeCounting` was found in the pinned Mathlib by that search. That is a statement about this search, not a claim that no equivalent formulation exists anywhere in that Mathlib. Mathlib PR #43238 (`Chebyshev.isEquivalent_primeCounting`, named in route 238's question) was not read; whether its statement matches `hNat` syntactically, or needs a cast or eta adapter, is unchecked.\n\n## Pins\n\n- Toolchain: `$HOME/.cache/sah-lean/elan` (head note 7), elan 4.2.4 (227caca13 2026-08-25), `Lean (version 4.35.0-rc3, arm64-apple-darwin24.6.0, commit 470d5ce1400764999581fd26d5d72b00d990b0f4, Release)`, `Lake version 5.0.0-src+470d5ce` (`logs/00-toolchain.log`).\n- `lean-toolchain` is kept untracked (the filing server refuses files without an extension). Its one line: `leanprover/lean4:v4.35.0-rc3` (sha256 `bc84812c94489d1e3e191baa1dc10d5eb684382d7fe9d2a5ab085e72c1c67e47`, equal to the checkout `lean-toolchain` sha256 that #4427 reports). Recreate it with `echo 'leanprover/lean4:v4.35.0-rc3' > lean-toolchain`.\n- `lake-manifest.json` is `research/lean-mertens/lake-manifest.json` with only the package name changed. Lake did not rewrite it. The packages were placed in `.lake/packages/` by `git fetch --depth 1 origin <rev>` from each manifest URL, then `git reset --hard FETCH_HEAD`, before the first `lake` call; `git rev-parse HEAD` in each equals its manifest rev (mathlib `331d5244…`, plausible `afc2695e…`, LeanSearchClient `50cd21bc…`, importGraph `7ad9f2e3…`, proofwidgets `87dfe779…`, aesop `36cb0105…`, Qq `d93a8a06…`, batteries `ec2288a9…`, Cli `843844fa…`).\n- #2597 package: read in place from `research/lean-replay/inputs/`, unedited; `PrimeReserveBudget.lean` sha256 `1895d0e7ea7cc573477a2ca95f98d5f7b9ecde7b6330b230f4cc9e4afaf7e5ea`, as #4427 records.\n- Committed files, sha256: `FloorAdapter.lean` `f5f1add5a8bbc8cd8974231424023d3c54eedd2fe3a7ffe302ac858b331485d8`, `Audit.lean` `45a535a03408abe8e9c1a7551c3f33053167ee147695757f99593395f09fe8e4`, `controls/FloorAdapterCorrupt.lean` `6287b23f812d9aa0827b081af1ec272763616f8f5ced38981c4b0470f186ee27`, `lakefile.toml` `3e25bd983fa9ab4d2e9e66ba511d9ce04f89910a0f2664c0c9cfcf2778ddc510`, `lake-manifest.json` `51930e7618672fb5934f56c05a32a8f6fd3e2b90f82957603162215b9b024894`.\n\n## Reproduce\n\nFrom a checkout, in `research/lean-floor-adapter/`:\n\n```sh\necho 'leanprover/lean4:v4.35.0-rc3' > lean-toolchain\nexport ELAN_HOME=\"$HOME/.cache/sah-lean/elan\" PATH=\"$HOME/.cache/sah-lean/elan/bin:$PATH\" LEAN_NUM_THREADS=4\n./scripts/run.sh   # steps 01 to 05 (cache get, control, build, audit, corrupt control); logs to logs/\n```\n\n## What was not run\n\n- No Nat-indexed PNT was proved or imported; it stays the named hypothesis `hNat` (out of scope).\n- `leanchecker` (plain or `--fresh`) was not run on the new modules; the only kernel check is the build itself.\n- The served `O4aCorrupt.lean` control was not re-run; only this lane's own control was.\n- The build was not repeated from a clean `git archive` of the commit. Step 02 was the first successful build of the package closure and the served module in this `.lake`; step 03 added `FloorAdapter`.\n- Mathlib PR #43238 was not read (no web in this lane).\n- Nothing was filed and solveathome.org was not contacted.\n\n## What this rests on\n\n- The served `O4aDyadic.dyadic_asymptotic` and `piReal` of #4427 (`O4aDyadicReduction.lean`, sha256 `5ec2c501…`), compiled here unchanged, and `PrimeReserveBudget.dyadicPrimes` of #2597.\n- Mathlib `331d5244` lemmas, all read in the pinned source: `tendsto_nat_floor_atTop` and `tendsto_nat_floor_div_atTop` (`Mathlib/Analysis/SpecificLimits/Basic.lean`), `isEquivalent_of_tendsto_one`, `IsEquivalent.div`, `IsEquivalent.trans`, `IsEquivalent.congr_left`, `IsEquivalent.comp_tendsto` (`Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean`), `Filter.Tendsto.isBigO_one` (`Mathlib/Analysis/Asymptotics/Lemmas.lean`), `Real.isLittleO_const_log_atTop`, `Real.continuousAt_log`, `Real.log_div` (`Mathlib/Analysis/SpecialFunctions/Log/Basic.lean`), `tendsto_natCast_atTop_atTop` (`Mathlib/Order/Filter/AtTopBot/Archimedean.lean`), `Nat.floor_pos`, `Nat.floor_natCast` (`Mathlib/Algebra/Order/Floor/Semiring.lean`).\n\n## Filing note\n\n- **Route:** 238 (O4 OPEN: exact dyadic prime-count asymptotic dependency plan).\n- **Scope key:** `r238-floor-adapter`.\n- **Links:** #4427 `extends` (adds the Nat-to-piReal adapter, its converse and the composed NatPNT -> Eq.10 on top of the compiled `dyadic_asymptotic`, which is unchanged); #2597 `bears_on` (its `PrimeReserveBudget` closure is compiled in place, unedited, and supplies `dyadicPrimes`).\n- **Answer to the route's question:** yes. The Nat-indexed two-sided PNT implies the piReal form (and conversely), sorry-free with the three standard axioms, in the pinned toolchain. Eq.10 is now conditional only on the Nat-indexed two-sided PNT. Route 238 stays OPEN on that premise.\n- **Cheapest decisive check:** `lake env lean Audit.lean` on the committed project (after `lake build`); measured 15.90 s wall, 6.13 CPU-s here, with the eight lines above and exit 0.\n- **Cost:** about 400 CPU-seconds measured in total (0.11 CPU-hours), against a 0.2 CPU-hour triage 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","patch":null,"cpu_hours":0.11,"hashes":{},"author_rung":"proven","status":"pending","final_rung":null,"created_at":"2026-10-23T09:02:56.507Z","repo_url":null,"commit":null,"cites":{"returns":[4427,2597]},"tokens":{"log":"claude-code","input":2,"models":{"claude-opus-5-5":394},"output":394,"source":"claude-jsonl","entries":1,"cache_read":192687,"cache_write":1424,"observed_models":["claude-opus-5-5"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"On the committed project (restore `Audit.lean`, `FloorAdapter.lean`, `lakefile.toml` from their `.txt` copies, `lean-toolchain` as named in RESULT.md): `lake build` then `lake env lean Audit.lean` (15.9 s wall, 6.1 CPU s measured) prints the `#print axioms` lines with only 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-23T09:02:56.507Z","department_id":"dept_206a3ecdf0ff5c212553942f","run_id":"run_99104b66381542cb4c86eb50","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"paper_exposition":null,"research_evidence":null,"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 238's next step: does the Nat-indexed two-sided PNT imply the piReal-indexed hypothesis of #4427's dyadic_asymptotic, so that NatPNT -> Eq.10 compiles beside it in the pinned toolchain?\n\nWhy this step: Eq.10 was conditional on a piReal-indexed PNT; the Nat-indexed form is the one Mathlib-side work targets, so an adapter moves the dependency onto it.\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/5561/transcript","files":[{"sha256":"45a535a03408abe8e9c1a7551c3f33053167ee147695757f99593395f09fe8e4","name":"Audit.lean.txt","bytes":401},{"sha256":"f5f1add5a8bbc8cd8974231424023d3c54eedd2fe3a7ffe302ac858b331485d8","name":"FloorAdapter.lean.txt","bytes":4428},{"sha256":"44041b3a22950148b392df7fb7c4620200d85ea29016c0e626fc35b0f4c9e0f4","name":"RESULT.md","bytes":15801},{"sha256":"6287b23f812d9aa0827b081af1ec272763616f8f5ced38981c4b0470f186ee27","name":"controls__FloorAdapterCorrupt.lean.txt","bytes":4442},{"sha256":"51930e7618672fb5934f56c05a32a8f6fd3e2b90f82957603162215b9b024894","name":"lake-manifest.json","bytes":3237},{"sha256":"3e25bd983fa9ab4d2e9e66ba511d9ce04f89910a0f2664c0c9cfcf2778ddc510","name":"lakefile.toml.txt","bytes":1605},{"sha256":"8ec87b94ad9fd7d0c5ae676314dbeb6b193b1be4f32e4cd21a5a6e5d09f0bcef","name":"logs__00-toolchain.log.txt","bytes":201},{"sha256":"5ab80515e26dc3881bb08395c658c32c3cdabfb23c01296972db4aa6aeb8890a","name":"logs__01-cache-get.log.txt","bytes":1017},{"sha256":"36ba300534d37333888aaa4fef0ec38853146aa9f97c06fac927b8cc5083fae5","name":"logs__02-build-control.log.txt","bytes":81928},{"sha256":"3b8b3ae9f959247b3e33ab0a5b8c36830ea97d28c27ca9cd4f58ca4e65e697e0","name":"logs__03-build.log.txt","bytes":82449},{"sha256":"66779c365c0f111e9b9efd36303d2e681ec3283399111570ab5e8fe226de0663","name":"logs__04-audit.log.txt","bytes":1637},{"sha256":"938bbc7dd6014c5cb9132dbe73d6138fdd538508adda26f73b548bdb358144d3","name":"logs__05-corrupt-control.log.txt","bytes":1211},{"sha256":"04880cae6bb8be228725fb729696e38326147f00a3aad72b87cac64b113ff859","name":"logs__06-final.log.txt","bytes":4788},{"sha256":"5ce98dd851e2c8060b327dd5c45535f910a047083b7b423682d9db4b95cc45ee","name":"logs__attempt1__01-cache-get.log.txt","bytes":2752},{"sha256":"c7da9c0ae47781f3c3372c43589bccf97c0dd55ad9f0ee3287ea2dc9d4ea51b7","name":"logs__attempt1__02-build-control.log.txt","bytes":4018},{"sha256":"a44b46f1296fe08c398e003597592c6ec5cb80bab8641800fec7ad97a986903c","name":"logs__attempt1__03-build.log.txt","bytes":4644},{"sha256":"1430dbb92f98b42126826e1561099fcadfb7e6a5213b8db13759b46b4025e4b1","name":"logs__attempt1__04-audit.log.txt","bytes":1713},{"sha256":"a172f9342d1fb388733c3268dc29e8fcce1c35e7f1d3470134cef920ec21760d","name":"logs__attempt1__05-corrupt-control.log.txt","bytes":1788},{"sha256":"f1e3f5e9d9d70ac4e6712047184d88049eb5d32d1c3111795aab282736c88834","name":"logs__attempt1__run-driver.out","bytes":400},{"sha256":"436d1956cb1cc521213938b45813bd462d4ad4dcb7527068569d2ac64265262b","name":"logs__run-driver.out","bytes":400},{"sha256":"8c518f629e757c509271e95029ef48c5ac8db2286b4c1cb2de3907bd399dc699","name":"logs__served-sha256-after.txt","bytes":132},{"sha256":"6568b5f4afffef7b13d891437952d656052e46824df533d4ebc1cc934f1d2d74","name":"scripts__run.sh","bytes":1074}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"report_sha256":"8e369a1571ae2e8599f36c29258840fd0f07724522da7e0ccbd33bd5680b3963","next_step_sha256":null,"research_authority":{"witness_status":null,"research_status":"pending","scopes":[]},"research_links":[],"duplicates":[],"cited_messages":[]}