  92
  93open Recognition
  94
  95structure U where
  96  a : Unit
  97
  98/-- Recognition relation by structural equality -/
  99def recog : U → U → Prop := fun x y => x = y
 100
 101def M : RecognitionStructure := { U := U, R := recog }
 102
 103def L : Ledger M := { debit := fun _ => 1, credit := fun _ => 1 }
 104
 105def twoStep : Chain M :=
 106  { n := 1
 107  , f := fun _ => ⟨()⟩
 108  , ok := by intro i; trivial }
 109
 110example : chainFlux L twoStep = 0 := by
 111  have hbal : ∀ u, L.debit u = L.credit u := by intro _; rfl
 112  simpa [chainFlux_zero_of_balanced (M:=M) L twoStep hbal]
 113
 114end Demo
 115
 116-- Moved advanced Recognition sections (ClassicalBridge, Potential uniqueness) to Recognition/WIP.lean during modularization.

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.