structure definition def or abbrev

`Configuration`

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

formal statement (Lean)

 111structure Configuration where
 112  value : ℝ
 113  pos : 0 < value
 114

used by (40)

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

J_nonneg in IndisputableMonolith.Astrophysics.StellarAssembly decl_use
delta_1_neg in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
no_singularity in IndisputableMonolith.Cosmology.EarlyUniverse decl_use
Configuration in IndisputableMonolith.Foundation.InitialCondition decl_use
entropy in IndisputableMonolith.Foundation.InitialCondition decl_use
nonunity_positive_entropy in IndisputableMonolith.Foundation.InitialCondition decl_use
past_theorem in IndisputableMonolith.Foundation.InitialCondition decl_use
total_defect in IndisputableMonolith.Foundation.InitialCondition decl_use
total_defect_nonneg in IndisputableMonolith.Foundation.InitialCondition decl_use
unity_config in IndisputableMonolith.Foundation.InitialCondition decl_use
unity_is_global_minimum in IndisputableMonolith.Foundation.InitialCondition decl_use
unity_unique_minimizer in IndisputableMonolith.Foundation.InitialCondition decl_use
zero_defect_iff_unity in IndisputableMonolith.Foundation.InitialCondition decl_use
rs_true_classical_iff in IndisputableMonolith.Foundation.OntologyPredicates decl_use
Stabilizes in IndisputableMonolith.Foundation.OntologyPredicates decl_use
config_to_recognition in IndisputableMonolith.Foundation.RecognitionForcing decl_use
cost_minima_are_recognition in IndisputableMonolith.Foundation.RecognitionForcing decl_use
recognition_forcing_complete in IndisputableMonolith.Foundation.RecognitionForcing decl_use
has_phi_structure in IndisputableMonolith.Foundation.StillnessGenerative decl_use
is_nontrivial in IndisputableMonolith.Foundation.StillnessGenerative decl_use
nontrivial_closed_has_phi_structure in IndisputableMonolith.Foundation.StillnessGenerative decl_use
static_ground_state_impossible in IndisputableMonolith.Foundation.StillnessGenerative decl_use
stillness_is_creative in IndisputableMonolith.Foundation.StillnessGenerative decl_use
T4_Recognition in IndisputableMonolith.Foundation.StillnessGenerative decl_use
t6_derived in IndisputableMonolith.Foundation.StillnessGenerative decl_use
conservation_is_unconditional in IndisputableMonolith.Foundation.TopologicalConservation decl_use
NoetherCharge in IndisputableMonolith.Foundation.TopologicalConservation decl_use
noether_not_necessarily_quantized in IndisputableMonolith.Foundation.TopologicalConservation decl_use
TopologicalCharge in IndisputableMonolith.Foundation.TopologicalConservation decl_use
topological_charge_quantized in IndisputableMonolith.Foundation.TopologicalConservation decl_use

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.

Configuration in IndisputableMonolith.Foundation.InitialCondition decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use