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

closedFramework_does_not_force_additive_posting

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)

 108theorem closedFramework_does_not_force_additive_posting :
 109    ∃ (F : ClosedObservableFramework) (base : F.S),
 110      ¬ (F.r (F.T^[2] base) = F.r (F.T^[1] base) + F.r base) := by

proof body

Term-mode proof.

 111  exact ⟨boolFramework, baseState, orbit_not_additive_posting⟩
 112
 113/-- Combined obstruction theorem: the earlier primitive layer admits
 114models where both target fields fail. -/

depends on (10)

Lean names referenced from this declaration's body.