Modal operators

box(P) and diamond(P) read “necessarily” and “possibly” over a frame of worlds — either the standpoints in scope, ordered by <:, or the configurations an individual passes through as the store mutates. Over the classification frame the two connect back to fixed classification. A type introduced by a fixed metatype carries forward rigidity: once an individual is a member, the mutation gate preserves that membership forward. So box(x : T) over a fixed-introduced T reduces to x : T — necessity is the property itself. The discharge is polarity-asymmetric: forward rigidity grips the positive box(x : T) but gives no grip on box(¬(x : T)), since a current non-member may still be constructed into the type later. The Lean proves both the discharge (box_fixed_discharge) and its asymmetry (isRigidIn_does_not_discharge_box_neg).

The engine evaluates this static-discharge case under fixed-default semantics: box and diamond parse, classify at the modal tier, and evaluate by stripping the wrapper and reading the inner atom. That is exact for fixed-introduced types — the common case — and conservative for dynamic ones, which a full Kripke evaluator would settle precisely. The evaluator, the desugaring to quantification over a World carrier, and the interaction of modal operators with federation are designed in the reference under standpoints and modal operators, and not yet wired.