theorem proved term proof

`probability_meaning_implies_lossy`

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

formal statement (Lean)

  80theorem probability_meaning_implies_lossy (h : probability_meaning_from_ledger) (obs : Observer) :
  81    ∃ x y : ℝ, x ≠ y ∧ project obs x = project obs y :=

proof body

Term-mode proof.

  82  h obs
  83
  84/-! ## Probability as Projection Weight -/
  85
  86/-- The fiber of outcome v: set of underlying states that project to v. -/

depends on (11)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
Observer in IndisputableMonolith.Foundation.Determinism decl_use
project in IndisputableMonolith.Foundation.Determinism decl_use
Observer in IndisputableMonolith.Foundation.ObserverForcing decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
probability_meaning_from_ledger in IndisputableMonolith.Philosophy.ProbabilityMeaningStructure decl_use