Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^333 The host reports the microphone faithfully

An assumption of yap 0.1.0.

Id
yap^333
Kind
assume
Reads as
assumed
Version
0.1.0

All of yap 0.1.0's claims

What it says

Audio reports name the clip they belong to and come between its start and stop; frames and peak are of the 16 kHz mono samples since the last report, and windows are the 320-sample windows those samples complete, counted from the start of the clip. A microphone that fails to start is reported once as `micFailed`.

Evidence

assumedStated, not proved. The proofs rely on it.
fuzzedNot shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95).

Where it's defined

Declaration
Yap.hostAudio
Module
Yap
Source
lean/Yap.lean:438 at v0.1.0
Statement hash
-

Ledger

yap^333 is active in this version's claims.lock. An id never moves or changes meaning.