theorem proved decidable or rfl

`photonEM_before_embodiedObserver`

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

formal statement (Lean)

 113theorem photonEM_before_embodiedObserver :
 114    Before Stage.photonEM Stage.embodiedObserver := by

proof body

Decided by rfl or decide.

 115  decide
 116
 117/-! ## Light: two senses -/
 118
 119/-- Recognition-light: the revealing act of an interface making distinction
 120available. This is pre-temporal. -/

depends on (12)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
Before in IndisputableMonolith.Foundation.PreTemporalForcingOrder decl_use
Stage in IndisputableMonolith.Foundation.PreTemporalForcingOrder 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
two in IndisputableMonolith.QFT.SpinStatistics decl_use