theorem proved term proof

`injectivity_of_observable_map`

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

formal statement (Lean)

  36theorem injectivity_of_observable_map {C E : Type*} (r : Recognizer C E) :
  37    Function.Injective (quotientEventMap r) :=

proof body

Term-mode proof.

  38  quotientEventMap_injective (r := r)
  39
  40/-! ## Paper Theorem: Refinement (Composition of Recognizers) -/
  41
  42/-- Paper theorem: the composite quotient maps surjectively to each component quotient. -/

depends on (9)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Composition in IndisputableMonolith.Foundation.CostAxioms decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
E in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
quotientEventMap in IndisputableMonolith.RecogGeom.Quotient decl_use
quotientEventMap_injective in IndisputableMonolith.RecogGeom.Quotient decl_use