structure definition def or abbrev

`State`

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

formal statement (Lean)

  28structure State (siteCount : ℕ) where
  29  omega : Fin siteCount → ℝ
  30
  31/-- Sum of a scalar field over the finite lattice window. -/

used by (40)

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

OctaveLoop in IndisputableMonolith.Applied.CoherenceTechnology decl_use
RSNSBridgeSpec in IndisputableMonolith.ClassicalBridge.Fluids.Bridge decl_use
CPMBridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM decl_use
bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
bridgeNormSq in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
Functionals in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
Hypothesis in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
model in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
State in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
DiscreteModel in IndisputableMonolith.ClassicalBridge.Fluids.Discrete decl_use
EnergyFunctional in IndisputableMonolith.ClassicalBridge.Fluids.Discrete decl_use
LedgerComputation in IndisputableMonolith.Complexity.ComputationBridge decl_use
no_fine_tuning in IndisputableMonolith.Cosmology.DarkEnergy decl_use
phase_locked_energy_constant in IndisputableMonolith.Cosmology.DarkEnergyEOS decl_use
love_jensen_strict in IndisputableMonolith.Ethics.ThermodynamicInstabilityOfExtraction decl_use
mp_from_cost_and_logic in IndisputableMonolith.Foundation.LogicFromCost decl_use
rung_separation in IndisputableMonolith.Foundation.SpectralEmergence decl_use
ground_state_recognition_impossible in IndisputableMonolith.Foundation.StillnessGenerative decl_use
stillness_is_creative in IndisputableMonolith.Foundation.StillnessGenerative decl_use
t6_derived in IndisputableMonolith.Foundation.StillnessGenerative decl_use
tick_within_epoch in IndisputableMonolith.Foundation.TimeEmergence decl_use
utm_exists in IndisputableMonolith.Information.ChurchTuring decl_use
info_cost_symmetric in IndisputableMonolith.Information.InformationIsLedger decl_use
Map in IndisputableMonolith.Measurement decl_use
CoreNSOperator in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
IncompressibleNSOperator in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
pauli_core in IndisputableMonolith.QFT.PauliExclusion decl_use
Outcome in IndisputableMonolith.Quantum.BellInequality decl_use
EPRPair in IndisputableMonolith.Quantum.NonlocalityNoSignaling decl_use
neutral_windows_from_jcost in IndisputableMonolith.Quantum.PointerStates decl_use

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
State in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use