probability_nonneg
plain-language theorem explainer
The declaration establishes non-negativity of outcome probabilities for any finite-resolution observer in the Recognition Science ledger model. A physicist examining epistemic interpretations of probability would cite it to confirm that projection weights remain non-negative even when derived from deterministic J-cost dynamics. The proof is a term-mode wrapper that unfolds the probability definition and invokes the positivity tactic.
Claim. Let $obs$ be an observer with finite positive resolution $N$ and let $v$ range over the $N$ distinguishable states. The observation probability $p(obs,v)$ satisfies $0 ≤ p(obs,v)$.
background
In this module an Observer is the structure from Foundation.Determinism consisting of a positive natural number resolution together with the proof that resolution exceeds zero; it models an agent that distinguishes only finitely many coarse-grained states of an underlying deterministic ledger. The function obs_probability expresses the probability of each distinguishable outcome as the normalized cardinality of the preimage fiber under the projection map, equivalently a J-cost projection weight. The local setting is PH-006, whose module document states that probability equals J-cost projection weight and is epistemic rather than ontic, with reality fixed by a unique J-minimizer at each ledger step.
proof idea
The term proof first unfolds obs_probability, exposing the quantity as a ratio of non-negative integers (fiber size over total states) or an equivalent non-negative J-cost weight. It then applies the positivity tactic, which discharges the inequality from the non-negativity of the underlying natural-number cardinalities and real-valued costs supplied by the imported cost definitions.
why it matters
The result supplies the non-negativity half of the PH-006 certificate that probability is the projection shadow of deterministic ledger dynamics rather than a fundamental ontic feature. It feeds the module's unification of frequentist, Bayesian, propensity and logical interpretations by guaranteeing that all derived fiber weights are admissible probabilities. The theorem rests on the Observer structure and the non-negativity of J-cost already recorded in ObserverForcing.cost and MultiplicativeRecognizerL4.cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.