abbrev definition def or abbrev

`Nothing`

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

formal statement (Lean)

   9abbrev Nothing := Empty

proof body

Definition body.

  10
  11/-- Minimal recognizer→recognized pairing. -/

used by (20)

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

mp_from_cost in IndisputableMonolith.Foundation.CostAxioms decl_use
unity_is_unique_existent in IndisputableMonolith.Foundation.CostAxioms decl_use
scaffolds_remaining in IndisputableMonolith.Foundation.InevitabilityEquivalence decl_use
economic_inevitability in IndisputableMonolith.Foundation.InevitabilityStructure decl_use
economic_inevitability_statement in IndisputableMonolith.Foundation.InevitabilityStructure decl_use
defect_pos_of_ne_one in IndisputableMonolith.Foundation.LawOfExistence decl_use
defect_tendsto_atTop_at_zero in IndisputableMonolith.Foundation.LawOfExistence decl_use
logic_from_cost_summary in IndisputableMonolith.Foundation.LogicFromCost decl_use
mp_from_cost_and_logic in IndisputableMonolith.Foundation.LogicFromCost decl_use
prelogical_boolean_fragment in IndisputableMonolith.Foundation.LogicFromCost decl_use
godel_not_obstruction in IndisputableMonolith.Foundation.OntologyPredicates decl_use
mp_physical in IndisputableMonolith.Foundation.OntologyPredicates decl_use
nothing_unbounded_defect in IndisputableMonolith.Foundation.OntologyPredicates decl_use
rs_exists_unique in IndisputableMonolith.Foundation.OntologyPredicates decl_use
rs_real_one in IndisputableMonolith.Foundation.OntologyPredicates decl_use
shimmerFactor_error_bound in IndisputableMonolith.Gap45.ShimmerFactor decl_use
impossible_is_non_positive in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
MP in IndisputableMonolith.Recognition decl_use
Recognize in IndisputableMonolith.Recognition decl_use
mp_holds in IndisputableMonolith.RRF.Core.Recognition decl_use