pith. machine review for the scientific record. sign in
theorem proved term proof

propensity_vindicated

show as:
view Lean formalization →

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)

 209theorem propensity_vindicated :
 210    -- The J-cost structure is objective (doesn't depend on observers)
 211    Foundation.LawOfExistence.defect 1 = 0 ∧
 212    (∀ x : ℝ, 0 < x → 0 ≤ Foundation.LawOfExistence.defect x) :=

proof body

Term-mode proof.

 213  ⟨Foundation.LawOfExistence.defect_at_one,
 214   fun x hx => Foundation.LawOfExistence.defect_nonneg hx⟩
 215
 216/-! ## Born Rule Structure -/
 217
 218/-- **Theorem (Born Rule Structure)**:
 219    The fiber structure of the projection map is what gives rise to the
 220    Born rule. The probability of outcome v is determined by:
 221    p(v) ∝ J-cost-weighted measure of { x : project(x) = v }
 222
 223    This is formalized as: the fiber partition is complete (covers all states)
 224    and each fiber is nonempty. The specific probability weights come from
 225    the J-cost landscape, giving rise to the Born rule. -/

depends on (28)

Lean names referenced from this declaration's body.