250theorem probability_nonneg (obs : Observer) (v : Fin obs.resolution) : 251 0 ≤ obs_probability obs v := by
proof body
Term-mode proof.
252 unfold obs_probability 253 positivity 254 255/-! ## Summary Certificate -/ 256 257/-- **PH-006 Certificate**: The meaning of probability. 258 259 RESOLVED: Probability = J-cost projection weight. 260 261 1. Reality is deterministic (unique J-minimizer) — no ontic probability 262 2. Observations are projections through finite-resolution observers 263 3. "Probability" = the fiber structure of the projection map 264 4. Born rule emerges from the fiber partition structure 265 5. All four interpretations are partially correct: 266 - Frequentist: long-run frequencies are objective (fiber structure) 267 - Bayesian: probability depends on information state (resolution) 268 - Propensity: objective J-cost landscape determines propensities 269 - Logical: projection structure is a logical/mathematical relation 270 271 The RS resolution: probability is NOT fundamental — it is the 272 projection shadow of deterministic ledger dynamics. -/
depends on (22)
Lean names referenced from this declaration's body.