structure definition def or abbrev

`LatticeState`

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

formal statement (Lean)

  16structure LatticeState where
  17  jbar : ℝ
  18  spectral_gap : ℝ
  19  energy : ℝ
  20  jbar_pos : jbar > 0
  21  gap_pos : spectral_gap > 0
  22  energy_pos : energy > 0
  23

used by (7)

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

applyCourage in IndisputableMonolith.Ethics.VirtueLatticeEffect decl_use
applyLove in IndisputableMonolith.Ethics.VirtueLatticeEffect decl_use
applyWisdom in IndisputableMonolith.Ethics.VirtueLatticeEffect decl_use
courage_enables_high_gradient_action in IndisputableMonolith.Ethics.VirtueLatticeEffect decl_use
love_reduces_collective_jbar in IndisputableMonolith.Ethics.VirtueLatticeEffect decl_use
love_widens_gap in IndisputableMonolith.Ethics.VirtueLatticeEffect decl_use
wisdom_preserves_energy in IndisputableMonolith.Ethics.VirtueLatticeEffect decl_use

depends on (4)

Lean names referenced from this declaration's body.

energy_pos in IndisputableMonolith.Foundation.OscillatoryDynamicsDeep decl_use
gap_pos in IndisputableMonolith.Information.LDPCCodeRateFromPhi decl_use
energy_pos in IndisputableMonolith.Information.RecognitionBremermann decl_use
spectral_gap in IndisputableMonolith.Unification.YangMillsMassGap decl_use