No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
18structure TwoOutcomeMeasurement where
19 C₁ : ℝ -- Recognition cost for outcome 1
20 C₂ : ℝ -- Recognition cost for outcome 2
21 C₁_nonneg : 0 ≤ C₁
22 C₂_nonneg : 0 ≤ C₂
23
24/-- Probability of outcome 1 -/
used by (6)
From the project-wide theorem graph. These declarations reference this one in their body.
-
born_rule_from_C
in IndisputableMonolith.Measurement.BornRule
decl_use
-
prob₁
in IndisputableMonolith.Measurement.BornRule
decl_use
-
prob₁_nonneg
in IndisputableMonolith.Measurement.BornRule
decl_use
-
prob₂
in IndisputableMonolith.Measurement.BornRule
decl_use
-
prob₂_nonneg
in IndisputableMonolith.Measurement.BornRule
decl_use
-
probabilities_normalized
in IndisputableMonolith.Measurement.BornRule
decl_use
depends on (8)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use