L-T27-CI-FIX: unblock #586 subtree bootstrap (compile-proofs, L1 TRACEABILITY, NOW Sync)

[gHashTag]

Mission

PR #586 (L-T27-SYNC-L1, subtree bootstrap from trios) is held by queen with 6 RED required checks. Subtree bootstrap of broken Coq into master would violate R10 (atomicity) and R7 (honest gates). Fix CI before merge.

Failing checks

Check	Workflow	Status
compile-proofs	Coq Proofs Validation	FAIL ×2
check-linked-issue	Issue Gate	FAIL
Check L1 TRACEABILITY	L1 TRACEABILITY Check	FAIL
check-now-freshness	NOW Sync Gate	FAIL
pr-dashboard	PR Dashboard	FAIL

Sub-lanes

L-T27-CI-FIX-L1: compile-proofs

Inspect run 25557517668 and 25557486715. Likely:

• Subtree imports paths that don't resolve in t27 _CoqProject
• Missing META / Makefile.coq regeneration
• Check assertions/manifest.json consistency

Acceptance: both Coq runs GREEN.

L-T27-CI-FIX-L2: L1 TRACEABILITY + NOW Sync

PR body must reference linked issue #559 in trios cross-ref format. Check now.json freshness (likely needs scripts/sync_now.sh or equivalent).

Acceptance: both gates GREEN.

L-T27-CI-FIX-L3: pr-dashboard + check-linked-issue

Lighter — likely missing PR body fields or issue ref. Inspect run 25557517538.

Acceptance: GREEN.

After CI green

Queen will --admin --squash merge #586 without override.

Honesty rules

• NO disabling checks
• NO --admin bypass on broken Coq
• If a proof is genuinely too hard for L1 bootstrap scope, narrow the subtree (move offending file to L2 lane and document)

Anchor

phi^2 + phi^-2 = 3 · DOI 10.5281/zenodo.19227877

cc trios#559 cc t27#586

[gHashTag]

Queen order — claim L-T27-CI-FIX (L1 first)

Army agent: claim this lane and execute in order L1 → L2 → L3.

Critical path: L1 (compile-proofs)

This is the gate. If subtree imports break Coq compilation in t27, fixing L2/L3 buys nothing — CI stays RED. Start here.

First diagnostic step (post results in heartbeat comment):

gh run view 25557517668 --repo gHashTag/t27 --log-failed | tail -200
gh run view 25557486715 --repo gHashTag/t27 --log-failed | tail -200

Look for:

• Missing Require Import paths (subtree namespace mismatch)
• _CoqProject not regenerated for subtree files
• Makefile.coq stale
• assertions/manifest.json referencing trios paths

Heartbeat protocol

• claim: comment with <!-- claim:L-T27-CI-FIX-L1 --> + agent codename
• progress: every 4h, <!-- heartbeat:LN --> with what was found / fixed
• DONE per sub-lane: <!-- done:L-T27-CI-FIX-LN --> with PR ref pushing to t27#586 head branch

Honesty rules (R7/R10)

• NO disabling compile-proofs workflow
• NO continue-on-error flags
• NO marking proofs Admitted to make them compile — if a proof is genuinely too hard for L1 scope, narrow the subtree (move offending .v file out of bootstrap, document in DEFER list)
• NO --admin bypass — only queen does that, and only on green CI

Anti-collision

Tag yourself with Greek-letter codename per trinity-mesh ACL (ALPHA..SHO). Check existing claims on t27#586 and t27#587 before claiming.

Reward

Unblocks t27#586 → unblocks trios#559 → -32 stale Admitted in trios trinity proofs.

Anchor

phi^2 + phi^-2 = 3 · DOI 10.5281/zenodo.19227877