abbrev definition def or abbrev

`Pot`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  12abbrev Pot (M : Recognition.RecognitionStructure) := M.U → ℤ

Definition body.

  13
  14/-- Discrete edge rule: along any edge, `p` increases by `δ` on `M.R`. -/

From the project-wide theorem graph. These declarations reference this one in their body.

DE in IndisputableMonolith.Potential decl_use
diff_const_on_component in IndisputableMonolith.Potential decl_use
diff_const_on_ReachN in IndisputableMonolith.Potential decl_use
diff_in_deltaSub in IndisputableMonolith.Potential decl_use
edge_diff_invariant in IndisputableMonolith.Potential decl_use
increment_on_ReachN in IndisputableMonolith.Potential decl_use
T4_unique_on_component in IndisputableMonolith.Potential decl_use
T4_unique_on_inBall in IndisputableMonolith.Potential decl_use
T4_unique_on_reachN in IndisputableMonolith.Potential decl_use
T4_unique_up_to_const_on_component in IndisputableMonolith.Potential decl_use
ZenoProtection in IndisputableMonolith.Quantum.ZenoEffect decl_use

Lean names referenced from this declaration's body.

RecognitionStructure in IndisputableMonolith.Chain decl_use
U in IndisputableMonolith.Constants.RSNativeUnits decl_use
RecognitionStructure in IndisputableMonolith.Foundation.RecognitionForcing decl_use
M in IndisputableMonolith.Recognition decl_use
RecognitionStructure in IndisputableMonolith.Recognition decl_use
U in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use
RecognitionStructure in IndisputableMonolith.RRF.Core.Recognition decl_use
RecognitionStructure in IndisputableMonolith.RRF.Foundation.MetaPrinciple decl_use