abbrev definition def or abbrev

`MP`

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

formal statement (Lean)

  29abbrev MP := Recognition.MP

Definition body.

  30
  31/-- Re-export: MP holds. -/

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

ml_derivation_complete in IndisputableMonolith.Astrophysics.MassToLight decl_use
ml_derivation_falsifiable in IndisputableMonolith.Astrophysics.MassToLight decl_use
ml_from_geometry_only in IndisputableMonolith.Astrophysics.ObservabilityLimits decl_use
unity_is_unique_existent in IndisputableMonolith.Foundation.CostAxioms decl_use
prelogical_boolean_fragment in IndisputableMonolith.Foundation.LogicFromCost decl_use
unity_has_no_phi_structure in IndisputableMonolith.Foundation.StillnessGenerative decl_use
voice_berry_positive in IndisputableMonolith.Foundation.VoiceForcing decl_use
meta_principle_status in IndisputableMonolith.Meta.Axioms decl_use
recognition_distinguishability_status in IndisputableMonolith.Meta.Axioms decl_use
MP in IndisputableMonolith.Recognition decl_use
mp_holds in IndisputableMonolith.Recognition decl_use
NothingCannotRecognizeItself in IndisputableMonolith.Recognition decl_use
Recognize in IndisputableMonolith.Recognition decl_use
bridge_certificate in IndisputableMonolith.Relativity.Geometry.DiscreteBridge decl_use
mp_holds in IndisputableMonolith.RRF.Core.Recognition decl_use
Recognize in IndisputableMonolith.RRF.Core.Recognition decl_use
MinimalLedger in IndisputableMonolith.RRF.Foundation.MetaPrinciple decl_use
self_similarity_forces_phi in IndisputableMonolith.RRF.Foundation.MetaPrinciple decl_use

Lean names referenced from this declaration's body.