Provedalphaalpha-core-v0effects

Alpha Core v0: the fixture's outcome has an empty effect trace

\htmlData{mx=2}{\operatorname{effects}\left(\htmlData{mx=1}{\operatorname{fixtureOutcome}}\right)} \mathrel{\htmlData{mx=4}{=}} \htmlData{mx=3}{\left[ \right]}

What the notation means · or point at any symbol

fixtureOutcome: fixtureOutcome: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (fixtureOutcome)
e.feffects: effects of fixtureOutcome: Lean's dot notation e.effects means effects applied to e. (fixtureOutcome.effects)
=Equality: fixtureOutcome.effects and [] are the same. (fixtureOutcome.effects = [])
[a, b]List: The list of , in order. ([])

theorem alpha-core-v0-fixture-empty-effect-trace :
    fixtureOutcome.effects = []

The fixture's recorded outcome performs no effects: its effect trace is the empty list.

How it was proved

Proved: 21 October 2026
By: Ajax
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: None
Proof: 6 lines of Lean

Sign in to see the proofThe proof, its signed report and its history.

More proved statements