Tier 3: design — IsStationary/IsStable/IsUnstable quantified-Prop vs explicit-g

[Xinze-Li-Moqian]

Part of umbrella #48. Design discussion — no code change until aligned.

Context

The explicit-g cascade (#9) lifted all of OpenGALib's Riemannian-stack theorems and definitions to take (g : RiemannianMetric I M) explicitly. Three GMT predicates remain typeclass-quantified:

• OpenGALib/GeometricMeasureTheory/Stationary.lean — def IsStationary (V : Varifold M) : Prop
• OpenGALib/GeometricMeasureTheory/Stable.lean — def IsStable ... (V : Varifold M) ... : Prop
• OpenGALib/GeometricMeasureTheory/Stable.lean — def IsUnstable ... (V : Varifold M) ... : Prop

These quantify [Riemannian.HasMetric I M] inside the ∀ so the predicate signature stays clean (Varifold M → Prop without exposing I to consumers).

Question

Should we lift to explicit-g (consistent with the rest of the stack) or keep as-is (consistent with V → Prop design choice)?

Option A — keep quantified-Prop (current)

• Pro: predicate signature stays V → Prop; consumers don't thread I/g
• Pro: matches the "for all smooth-manifold structures, every test direction satisfies …" reading
• Con: inconsistent with the rest of the explicit-g API surface

Option B — lift to explicit g

• Pro: API uniformity; future predicates follow the same shape
• Con: changes V → Prop to (g : RiemannianMetric I M) → V → Prop, breaking any current callsite that relies on the existential form

Acceptance

• Decision documented in this issue thread
• If B chosen: a follow-up sub-issue or PR opens
• If A chosen: a comment in each of the 3 files explaining the rationale (so future-Claude doesn't ask again)

Notes

Both maintainers assigned. Maintainer alignment first; no code until comment-thread reaches agreement.