Cairn Docs Claims Blog Packages

Claim ยท pairs 0.1.3

pairs^26 Best scores only improve

An invariant of pairs 0.1.3.

Id
pairs^26
Kind
invariant
Reads as
proved
Version
0.1.3

All of pairs 0.1.3's claims

What it says

A pack's best moves and best time only ever get better: a win records the better of each, and scores read from disk are merged the same way, never overwriting a better one.

Evidence

provedinitPairs.bestImproves.init
provedstepPairs.bestImproves.step
provedreceivePairs.bestImproves.receive
provedreachablePairs.bestImproves.reachable
provedreachableAllPairs.bestImproves.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
Pairs.bestImproves
Module
Pairs.Claims
Source
lean/Pairs/Claims.lean:419 at v0.1.3
Machine
Pairs.machine
Statement
Pairs.bestImproves.holds
Statement hash
fce5e9eb41fe82b2

Ledger

pairs^26 is active in this version's claims.lock, statement fce5e9eb41fe82b2. An id never moves or changes meaning.