Special Functions · Lean source
SeedSizeCheck.lean
Selected results recorded Coverage and evidence
Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
Local imports (1)
guarded_majorant_controls/SeedSizeCheck.lean7 lines
Original source path
lean/guarded_majorant_controls/SeedSizeCheck.lean1 import CoupledGuardedMajorant
2 noncomputable section
3 open Komorebi.SpecialFunctions.Coupled.Scales
4
5 example : checkedMajorant (⟨1/2,1/2,1/2,1/2⟩ : RationalScales)
6 (3/4) (some 0) (some 1) = .error (.resource .bits) := by
7 norm_num [checkedMajorant,RationalScales.strictRational,guardedMajorant,buildLadder,guardedFold]
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: ce8b8866a49191c2960b99adfb4ed6829e0612e7b592d3c210fbbf0d378dd426