Android: Ephapax region-calculus modelling of long-lived Service handles

[hyperpolymath]

Context

Gossamer.ABI.AndroidComponents (new) models the Android component lifecycles and proves the unambiguous safety properties:

• terminal teardown (svcDestroyedTerminal / rcvCompleteTerminal / wdgDisabledTerminal);
• dispatch-only-while-live (SvcLive / WidgetUpdateBorrow uninhabited in the terminal state);
• the long-lived Service as a LinearHandle over the same Allocated/Active/Consumed machine as the webview (LinearService, allocateService, consumeForStop).

That is enough to land the component hosts safely. It deliberately does not settle the deeper region question.

The open question

The webview handle lives in a relatively short-lived region (an Activity). A foreground Service is JVM-owned and long-lived — it can outlive every Activity, and it commonly holds references that cross into other components (e.g. a Service pushing an AppWidget update; a BroadcastReceiver starting the Service).

Under the Ephapax region-calculus, how should these be modelled?

1. Does the Service get its own region with a lifetime that nests outside the webview region, or a sibling region with explicit cross-region capabilities?
2. How are cross-region references (Service → Widget, Receiver → Service) typed so they can't dangle when one component is torn down by the JVM out from under the other?
3. Is the runtime "is this component still live?" check (today: handler simply absent from the process-global registry) reflected at the type level as a region-membership witness, the way MainThreadProof reflects thread affinity?

Why it's deferred

This is genuine type-system design, not a mechanical change, and getting it wrong would push an unsound model onto downstream apps. Tracking it here rather than rushing a speculative refactor (per the PR's remit). Input from the Ephapax side welcome.

Refs: docs/architecture/android-components.adoc (linearity section), src/interface/abi/AndroidComponents.idr.