# Proof audit, round 1

Verdict: automated proof SUPPORTS the stated selection claim at the hook/resolver boundary. Native capture UNVERIFIED. No blocking proof finding for that bounded claim; this is not an end-to-end mobile certification.

Target: [#24262](https://git.cafe/pingdotgg/t3code/pulls/24262), repository pingdotgg/t3code, branch t3/mobile-audit-pr-target-20261023, base main. Initial [6c78970e43](https://git.cafe/pingdotgg/t3code/commit/6c78970e437eecb357d070d6a8acf1c5e2ee3636); audited [3d2f19579d](https://git.cafe/pingdotgg/t3code/commit/3d2f19579d9e20648a5d8e31007be77b8827db6d).

Scope: read-only source audit in /home/ubuntu/wt/pr-24262. Full five-file PR diff reviewed from merge base 22dc1dabc6d3b1616d0fa5017268c086a77887bc (origin/main...HEAD). Local main is stale and gives an unrelated, very large diff; that was discarded. The actual delta changes only the mobile PR resolver, hook, their tests, and jsdom test registration. No protected-domain implementation changes found; existing client-runtime type imports do not change provider runtime behavior. No source edits or mutations performed.

Product decision: retain an enabled requested environment indefinitely while available/connecting/reconnecting, until explicit failure; no elapsed-time fallback. This is explicit in the [resolver comment and guard](/home/ubuntu/wt/pr-24262/apps/mobile/src/features/pull-requests/pullRequestEnvironmentFallback.ts:21). Catalog initialization is a separate isReady gate in the [hook](/home/ubuntu/wt/pr-24262/apps/mobile/src/features/pull-requests/usePullRequestEnvironmentFallback.ts:14). No invented initializing connection phase or timeout is required.

## Synthetic fixture matrix

Common fixture: requested/original and copy/copy-project have canonical identity github.com/owner/repo; copy is enabled and connected. Route requests requested/original with explicit host and repository. Test renders a Probe invoking the real hook/resolver, with mocked catalog/projects and navigation setParams updating React state.

| State class / transition | Expected result | Coverage |
| --- | --- | --- |
| Catalog initializing (isReady false), requested absent, connected copy present | requested/original remains; no setParams | [hook test](/home/ubuntu/wt/pr-24262/apps/mobile/src/features/pull-requests/usePullRequestEnvironmentFallback.test.tsx:89) |
| Enabled available -> connecting -> reconnecting -> connected | requested/original remains through every rerender; no setParams | [hook test](/home/ubuntu/wt/pr-24262/apps/mobile/src/features/pull-requests/usePullRequestEnvironmentFallback.test.tsx:98) |
| Open with enabled connecting, requested project unhydrated -> project hydrates and requested connects | requested/original remains before and after; connected copy cannot steal target | [hydration regression](/home/ubuntu/wt/pr-24262/apps/mobile/src/features/pull-requests/usePullRequestEnvironmentFallback.test.tsx:130) |
| Ready catalog, requested missing | copy/copy-project; exactly one setParams with both IDs | [fallback loop](/home/ubuntu/wt/pr-24262/apps/mobile/src/features/pull-requests/usePullRequestEnvironmentFallback.test.tsx:106) |
| Requested disabled (available phase) | copy/copy-project; exactly one setParams | same fallback loop |
| Requested enabled offline | copy/copy-project; exactly one setParams | same fallback loop |
| Requested enabled error | copy/copy-project; exactly one setParams | same fallback loop |
| Requested enabled unsupported | copy/copy-project; exactly one setParams | same fallback loop |
| Original connected; alternative connected | retain original | [resolver test](/home/ubuntu/wt/pr-24262/apps/mobile/src/features/pull-requests/pullRequestEnvironmentFallback.test.ts:42) |
| Original absent, only unrelated repository connected | no fallback | same resolver test |
| Host absent from route, original project identity available | derive host and select same-repository copy | [host regression](/home/ubuntu/wt/pr-24262/apps/mobile/src/features/pull-requests/pullRequestEnvironmentFallback.test.ts:55) |

The hook is called by the actual [PR route](/home/ubuntu/wt/pr-24262/apps/mobile/src/features/pull-requests/PullRequestRouteScreen.tsx:288). This is inspected wiring, not a mounted route proof. Fallback requires an enabled connected matching repository copy; missing host plus missing original identity cannot identify a copy and returns null.

## Test reduction and mutation evidence

Initial pinned source expands to 17 tests: 7 resolver cases (three ordinary tests, three pending-phase cases, one disabled-copy case), and 10 hook cases (three pending-phase cases, initialization, five failure cases, hydration). Current source has 6 tests: 3 resolver and 3 hook. Pending and failure states remain exercised inside loops; six named tests does not mean six state scenarios. Removed standalone disabled-copy rejection coverage is not retained elsewhere. The implementation still explicitly filters disabled destination copies, but that filter is not directly proven by the current suite. Disabled requested coverage uses available only, not every possible phase.

Independent current-head run: from apps/mobile, `vp test run src/features/pull-requests/pullRequestEnvironmentFallback.test.ts src/features/pull-requests/usePullRequestEnvironmentFallback.test.tsx` completed exit 0, 2 files passed, 6 tests passed (1.57 s). Synthetic fixtures only; no server/browser/device.

User-supplied mutation evidence: removing the retention guard yielded 2 failed / 4 passed; restoration yielded 6 passed. This is consistent with current code: the pending-state test and unhydrated-connecting test should fail without that guard; initialization is protected by a different gate and fallback tests should continue passing. This auditor did not reproduce mutation or find a saved mutation transcript among top-level evidence files. Therefore the 2/4 split is reported prior evidence, not independently witnessed proof. A guard-only mutation does not prove the readiness gate, candidate-enabled filter, every phase branch individually, or the entire pre-fix implementation. Independent 6/6 run corroborates the restored state. No additional tests are demanded solely to expand coverage.

## Proof limits and device status

Tests use React DOM/jsdom with mocked useWorkspaceEnvironments, useConnectionsReady, useProjects, and navigation. They do not mount React Native, React Navigation, the full PR screen, or real atom subscriptions; they do not establish cold-start event ordering, transport delivery, fetched PR content, native layout, Android/iOS visual behavior, or relay/tunnel operation. An offline/missing fixture proves fallback on initial render, not the pending->failure transition in a live connection. Source dependencies support recomputation on catalog changes, but that transition is not independently exercised. Indefinite retention is a product decision expressed by a state-only guard, not a wall-clock durability test.

Capture: UNVERIFIED. Per supplied device evidence, device_list returned exactly: "Agent device access is turned off for this environment." `command -v adb` and `command -v android-emulator` were absent; ~/Android/Sdk/platform-tools and /opt/android-sdk were absent. This auditor did not retry device access or independently re-run those availability checks. No servers or emulator started; no tools installed; no other machine contacted; no live ~/.t3/userdata accessed. iOS capture was not attempted. Capture unavailability is a disclosed evidence limit, not a blocker to the bounded automated-proof verdict.

FRICTION: Local main is stale; use the verified origin/main merge base for this PR diff.
FRICTION: Mutation split is supplied evidence without an inspected saved transcript; only restored 6/6 was independently rerun.
FRICTION: Disabled fallback-copy rejection test was removed; implementation inspection supports it, current automated coverage does not directly assert it.
FRICTION: Native capture UNVERIFIED because device access is disabled and local Android tooling is absent; no installation or remote workaround attempted.