abbrev definition def or abbrev

`ConfigProp`

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

formal statement (Lean)

 308abbrev ConfigProp := Config → Prop

proof body

Definition body.

 309
 310/-- **MODAL NECESSITY (□)**: A property is necessary iff it holds in ALL possible futures.
 311
 312    □p at c ⟺ ∀ y ∈ P(c), p(y)
 313
 314    In RS, necessity means "forced by cost minimization." -/

used by (15)

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

adjoint_from_cost_monotonic in IndisputableMonolith.Modal.Actualization decl_use
Contingent in IndisputableMonolith.Modal.Actualization decl_use
CostMonotonic in IndisputableMonolith.Modal.Actualization decl_use
Determined in IndisputableMonolith.Modal.Actualization decl_use
determined_necessary_for_minimal in IndisputableMonolith.Modal.Actualization decl_use
H_adjoint_non_minimal in IndisputableMonolith.Modal.Actualization decl_use
possibility_actualization_adjoint in IndisputableMonolith.Modal.Actualization decl_use
possibility_actualization_adjoint_hypothesis in IndisputableMonolith.Modal.Actualization decl_use
possibility_actualization_adjoint_minimal in IndisputableMonolith.Modal.Actualization decl_use
possibility_actualization_adjoint_monotonic in IndisputableMonolith.Modal.Actualization decl_use
modal_duality in IndisputableMonolith.Modal.Possibility decl_use
modal_K in IndisputableMonolith.Modal.Possibility decl_use
modal_T_weak in IndisputableMonolith.Modal.Possibility decl_use
Necessary in IndisputableMonolith.Modal.Possibility decl_use
Possible in IndisputableMonolith.Modal.Possibility decl_use

depends on (11)

Lean names referenced from this declaration's body.

A in IndisputableMonolith.Foundation.IntegrationGap decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
Config in IndisputableMonolith.Gravity.ILG decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
Config in IndisputableMonolith.Modal.Possibility decl_use