structure definition def or abbrev

`ConsistentConfig`

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

formal statement (Lean)

 182structure ConsistentConfig where
 183  /-- The proposition P -/
 184  P : Prop
 185  /-- The ratio for P -/
 186  ratio : ℝ
 187  /-- Ratio is positive -/
 188  ratio_pos : ratio > 0
 189
 190/-- The cost of a consistent configuration. -/

used by (6)

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

consistent_cost in IndisputableMonolith.Foundation.LogicFromCost decl_use
consistent_minimum_cost in IndisputableMonolith.Foundation.LogicFromCost decl_use
consistent_zero_cost_possible in IndisputableMonolith.Foundation.LogicFromCost decl_use
logic_from_cost in IndisputableMonolith.Foundation.LogicFromCost decl_use
logic_from_cost_summary in IndisputableMonolith.Foundation.LogicFromCost decl_use
why_logic_is_real in IndisputableMonolith.Foundation.LogicFromCost decl_use

depends on (13)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
consistent in IndisputableMonolith.Complexity.SAT.Backprop decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use