structure
definition
def or abbrev
Observer
show as:
view Lean formalization →
formal statement (Lean)
96structure Observer where
97 /-- Number of distinguishable states -/
98 resolution : ℕ
99 /-- Resolution is finite and positive -/
100 res_pos : 0 < resolution
101
102/-- The projection map: a deterministic state maps to an observed state. -/
used by (30)
-
project -
projection_lossy -
cooper_paired_reference_yields_observer -
cooper_pairing_yields_persistent -
has_distinguishable_events -
nontrivial_recognition_forces_observer -
Observer -
observer_forcing_certificate -
observer_forcing_status -
reference_unit_state -
reference_zero_cost -
pointInterface_separates -
physical_light_not_first -
Recognizer -
bayesian_vindicated -
born_rule_structure -
each_fiber_nonempty -
Fiber -
fibers_cover -
frequentist_vindicated -
higher_resolution_finer_distinctions -
obs_probability -
ph006_probability_certificate -
probability_from_projection -
probability_is_relational -
probability_meaning_from_ledger -
probability_meaning_implies_lossy -
probability_nonneg -
probability_sums_to_one -
prob_is_epistemic