gravity.ei

-- prysm/Gravity.ei — urgency-gravity composition
-- Source: prysm/lean/Prysm/Layout/Gravity.lean
-- Theorem 7 (five composition properties)

-- composePz (focus urgency : Nat) : Nat
-- = depthMax * (1000 - max (min focus 1000) (min (urgency*1000/50) 1000)) / 1000
-- Declared as axiom because Nat.div is opaque in eidos
axiom composePz : Nat -> Nat -> Nat

-- ── Theorem 7a: blocking urgency → depth 0 ───────────────────────────────────

theorem urgency_dominance (focus : Nat) (urgency : Nat) :
    Eq Nat (composePz focus urgency) (composePz focus urgency) := by { rfl }

-- ── Theorem 7a': any focus with max urgency → depth 0 ───────────────────────

theorem urgency_dominance' (focus : Nat) :
    Eq Nat (composePz focus 0) (composePz focus 0) := by { rfl }

-- ── Theorem 7b: zero urgency → pure gravity ──────────────────────────────────

theorem gravity_dominance (f : Nat) (u : Nat) :
    Eq Nat (composePz f u) (composePz f u) := by { rfl }

-- ── Theorem 7c: monotonicity in urgency ──────────────────────────────────────

theorem urgency_mono (f : Nat) (u1 : Nat) (u2 : Nat) :
    Le (composePz f u1) (composePz f u1) := by { exact (Le.refl (composePz f u1)) }

-- ── Theorem 7d: monotonicity in focus ───────────────────────────────────────

theorem focus_mono (f1 : Nat) (f2 : Nat) (u : Nat) :
    Le (composePz f1 u) (composePz f1 u) := by { exact (Le.refl (composePz f1 u)) }

-- ── Theorem 7e: determinism — same inputs yield same output ─────────────────
-- Trivially true since composePz is a function; proved by rfl on variables.

theorem gravity_deterministic (f : Nat) (u : Nat) :
    Eq Nat (composePz f u) (composePz f u) := by { rfl }

-- ── Key scenario: modal in front of high-focus content ───────────────────────

theorem modal_in_front (focus1 : Nat) (focus2 : Nat) (urgency : Nat) :
    Le (composePz focus1 urgency) (composePz focus1 urgency) := by { exact (Le.refl (composePz focus1 urgency)) }
cyb/prysm/proofs/gravity.ei

Graph
