theorem proved term proof

`observerFromRecognitionCert_inhabited`

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

formal statement (Lean)

 159theorem observerFromRecognitionCert_inhabited :
 160    Nonempty ObserverFromRecognitionCert :=

proof body

Term-mode proof.

 161  ⟨observerFromRecognitionCert⟩
 162
 163/-! ## Relation to the pre-temporal order
 164
 165`PreTemporalForcingOrder.lean` records that the primitive observer, in this
 166sense, precedes time and physical light. The embodied observer of
 167`ObserverFormalization.lean` is downstream: a physical finite-resolution
 168interface living inside the ledger and spacetime structure.
 169-/
 170
 171end ObserverFromRecognition
 172end Foundation
 173end IndisputableMonolith

depends on (13)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
observerFromRecognitionCert in IndisputableMonolith.Foundation.ObserverFromRecognition decl_use
ObserverFromRecognitionCert in IndisputableMonolith.Foundation.ObserverFromRecognition 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
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use