theorem proved term proof

`recognition_structure_nonempty`

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

formal statement (Lean)

  68theorem recognition_structure_nonempty {X : Type*}
  69    (R : RecognitionStructure X) : Nonempty X :=

proof body

Term-mode proof.

  70  MetaPrinciple X ⟨R.recognizes, R.has_self_recognition⟩
  71
  72/-! ## From Recognition to Ledger -/
  73
  74/-- A minimal ledger: balanced debits and credits. -/

depends on (11)

Lean names referenced from this declaration's body.

RecognitionStructure in IndisputableMonolith.Chain decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
balanced in IndisputableMonolith.Foundation.LedgerForcing decl_use
RecognitionStructure in IndisputableMonolith.Foundation.RecognitionForcing decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
RecognitionStructure in IndisputableMonolith.Recognition decl_use
RecognitionStructure in IndisputableMonolith.RRF.Core.Recognition decl_use
MetaPrinciple in IndisputableMonolith.RRF.Foundation.MetaPrinciple decl_use
RecognitionStructure in IndisputableMonolith.RRF.Foundation.MetaPrinciple decl_use