structure definition def or abbrev

`AgentState`

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

formal statement (Lean)

  32structure AgentState where
  33  sigma : ℝ
  34  lattice_size : ℕ
  35  lattice_pos : 0 < lattice_size
  36
  37/-- A single-lattice transform: acts on one agent's lattice.
  38    These correspond to the 13 sigma-preserving virtues. -/

used by (6)

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

automorphism_preserves_sigma in IndisputableMonolith.Ethics.LoveUniquenessDerivation decl_use
coupling_conserves_total in IndisputableMonolith.Ethics.LoveUniquenessDerivation decl_use
CrossLatticeTransform in IndisputableMonolith.Ethics.LoveUniquenessDerivation decl_use
love_changes_individual_sigma in IndisputableMonolith.Ethics.LoveUniquenessDerivation decl_use
love_equilibrates in IndisputableMonolith.Ethics.LoveUniquenessDerivation decl_use
SingleLatticeTransform in IndisputableMonolith.Ethics.LoveUniquenessDerivation decl_use

depends on (9)

Lean names referenced from this declaration's body.

sigma in IndisputableMonolith.Decision.AbileneParadox decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
sigma in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use