Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^321 Only the first 25 terms are sent

An invariant of yap 0.1.0.

Id
yap^321
Kind
invariant
Reads as
proved
Version
0.1.0

All of yap 0.1.0's claims

What it says

Every upload is a transcription, of a whole clip or a preview chunk, whose prompt is the one a dictionary of just its first 25 terms would give (`app_prompt`, `step_prompt`).

Evidence

provedinitYap.first25Terms.init
provedstepYap.first25Terms.step
provedreceiveYap.first25Terms.receive
provedreachableYap.first25Terms.reachable
provedreachableAllYap.first25Terms.reachableAll
fuzzedNot shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95).
testedNot shown yet: the running app matched the model at every step that exercised it (docs/conformance.md). A CI step will publish it (#95).

Where it's defined

Declaration
Yap.first25Terms
Module
Yap
Source
lean/Yap.lean:371 at v0.1.0
Machine
Yap.machine
Statement
Yap.first25Terms.holds
Statement hash
006cb628f2f0b864

Ledger

yap^321 is active in this version's claims.lock, statement 006cb628f2f0b864. An id never moves or changes meaning.