The K-COS Method · Lean source

MissingBudget.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)

verification/controls/MissingBudget.lean6 lines

Original source path

lean/verification/controls/MissingBudget.lean

1 import KomorebiQCOS
2 open KomorebiQCOS
3 example {x middle estimate a b tolerance : ℝ}
4     (ha : ErrorBound x middle a) (hb : ErrorBound middle estimate b) :
5     ErrorBound x estimate tolerance := by
6   exact errorBound_accept ha hb

Back to source controls

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: ff9c06f1f521eea4ee4af12d13806d23dc93da4523a39e499627808e623c498f

Original source on GitHub

Back to COS Method