fix(agda): restore main typecheck — carry the fiber invariant in FiberBundle

[arena-ai-coding-agent]

Reopens main for business: CI Agda has been red since 2026-09-26.

Status

Last green on main	9c4b72b5, 2026-09-21T12:20
Red since	2026-09-26T18:35 (three consecutive failing runs)
Failing jobs	cold-check (Agda typecheck, exit 42) and check (kernel-guard, exit 1)

Both failures are real defects, not infrastructure. Two independent causes.

Failure 1 — kernel-guard.sh classification drift (fixed, verified locally)

scripts/kernel-guard.sh check B requires every proofs/agda/Echo*.agda to be named in
docs/echo-types/echo-kernel-note.adoc. Three modules added by #325 and #327 were never
classified:

kernel-guard: FAIL: unclassified Echo* module(s) — add to
  docs/echo-types/echo-kernel-note.adoc (and MAP.adoc tag):
  EchoBitNarrowingNumeric EchoExampleBitNarrowing EchoHaplotypeCollapsing

All three are Tier 2 (each depends on a Tier-2 module — EchoExampleBitNarrowing on
EchoExampleTruncation, EchoBitNarrowingNumeric on both of those, EchoHaplotypeCollapsing on
EchoAggregation + EchoNoSectionGeneric).

Check A (the funext-free certificate) already passed and still passes: Echo and EchoKernel
are stdlib-only, no postulates, no escape pragmas, no funext imports. That certificate is intact.

Verified locally — the guard is pure POSIX shell and needs no Agda:

kernel-guard: PASS — funext-free certificate enforced; classification in sync.
EXIT=0

Failure 2 — a missing invariant in FiberBundle (fixed, awaits CI)

EchoHaplotypeCollapsing.agda did not typecheck. The defect is in bundle-fiber-echoes:

record FiberBundle : Set where
  field
    haplotype      : Haplotype
    representative : Clone
    fiber          : List Clone          -- no link to `haplotype`

bundle-fiber-echoes : (b : FiberBundle) → List (HaploFiber (FiberBundle.haplotype b))
bundle-fiber-echoes b = map (λ c → c , refl) (FiberBundle.fiber b)

HaploFiber h = Echo collapse h = Σ Clone (λ c → collapse c ≡ h), so the lambda demands
refl : collapse c ≡ FiberBundle.haplotype b for an arbitrary c taken from fiber b.
Those terms are not judgementally equal. Expected message:

collapse c != FiberBundle.haplotype b of type Haplotype
when checking that the expression refl has type collapse c ≡ FiberBundle.haplotype b

This is not a typo — the record is missing an invariant, and the invariant is already
documented one layer up. docs/echo-types/applications/haplotype-collapsing.adoc:

Nickel contracts enforce:

• count == length clones
• every clones[i].haplotype_id == haplotype_id

The Nickel schema had the contract; the Agda record did not — then the module tried to prove a
consequence of an invariant it never carried.

Fix: make the invariant structural rather than re-imposed at the use site.

record FiberBundle : Set where
  field
    haplotype      : Haplotype
    representative : HaploFiber haplotype
    fiber          : List (HaploFiber haplotype)

bundle-fiber-echoes becomes the field projection and needs no proof; example-bundle supplies
genuine echoes. example-count = refl and clone-count-aggregation were checked against their
definitions and are correct as they stood. Also drops the now-unused map / length imports.

This is the same lesson as the Ephapax region_shrink falsity, arriving from the opposite
direction: there, an invariant kept in a per-use side-condition produced a false lemma; here,
an invariant kept out of the carrier produced an unprovable one.

This half is reasoned, not machine-verified. No Agda toolchain is reachable in the
environment this was prepared in (GitHub release assets are network-blocked and Agda is not
installable from source there), so the fix could not be typechecked locally. It needs this PR's
Agda run to confirm. If the error differs from the prediction above, the reasoning has a hole
and the diagnostic is wrong — please paste the actual output rather than merging.

Side findings (not fixed here)

1. EchoBitNarrowingNumeric and EchoExampleBitNarrowing are unreachable from every CI
   target. The cold-check compiles only All.agda, Smoke.agda, characteristic/All.agda,
   examples/All.agda and EchoImageFactorizationPropCubical.agda. Neither module is imported
   by any of them, so both are never typechecked by CI — they only tripped a grep. proofs(agda): preserve the bit-narrowing exhibits from unpushed commi… #325's own
   message notes they were recovered "from unpushed commits". These are currently unverified.
2. docs/echo-types/MAP.adoc names EchoHaplotypeCollapsing but neither bit-narrowing
   module. kernel-guard.sh only checks the kernel note, so this is not a gate failure — but it
   is drift, and adding entries needs an editorial call on placement.

Note on this branch

This branch comes from a structural audit of the six-repo estate (echo-types, ephapax,
affinescript, systemet, anytype, panoply) rather than from the usual issue flow, hence the
arena/ name and the absence of a linked issue. Only the two fixes above are in scope. Happy to
re-cut against an issue, or to drop this and hand the diagnosis over as an issue instead.

Worth recording that the gate itself worked exactly as designed: because All.agda and
Smoke.agda were both wired to the new module, main went red the moment an unprovable lemma
landed. That is the strongest argument for the existing methodology — the gap is in the repair
loop, not the check.

---

Second fix: main's CodeQL and Hypatia workflows never start (6044971)

Investigating why this PR's checks came back startup_failure turned up a separate,
pre-existing breakage on main — one that has nothing to do with this branch.

Evidence

On main, at commit 1f677531, pushed by hyperpolymath, event push, same run batch:

2026-09-27T01:55:43  Agda                      actor=hyperpolymath  -> ran (conclusion: failure)
2026-09-27T01:55:44  CodeQL Security Analysis  actor=hyperpolymath  -> startup_failure
2026-09-27T01:55:45  Hypatia Security Scan      actor=hyperpolymath  -> startup_failure

Same actor, same commit, same event. The lockfile validation is therefore per-workflow, and
exactly the two workflows whose lock entries are stale are the two that never start. The same
pair has startup-failed on every event since 2026-09-26, including human pushes to main.

Cause

cd9aa401 (dependabot, #326, 2026-09-26) changed .github/workflows/codeql.yml (+2 −2) and
.github/workflows/hypatia-scan.yml (+1 −1), bumping github/codeql-action 4.38.0 → 4.38.1
— but did not regenerate .github/workflows/actions.lock, which still pinned 4.38.0 in three
places. The lockfile no longer validates against the workflows, so the gate rejects the runs
before any job is created.

This is the same failure mode, and the same fix, as 9c4b72b5 — the last green main commit,
whose message reads: "Workflows fail at creation with The lockfile could not be validated. Regenerate it by running gh actions-lock".

Fix

Version strings only — 2 workflows: refs plus the dependencies: entry, resolved to 4.38.1.

The commit: hash is the peeled tag commit, which is the convention the existing entry
already follows: v4.38.0^{} = b96794f0… is byte-for-byte the hash previously recorded.
v4.38.1^{} = 1c5b6756…, from git ls-remote --tags https://github.com/github/codeql-action.
owner_id/repo_id are unchanged (same repository). The lock's existing habit of recording the
repo-level ref while the workflows use sub-paths
(github/codeql-action@v4.38.1 vs github/codeql-action/init@v4.38.1) is preserved exactly.

Caveat: regenerated by hand, not by gh actions-lock — the extension's release binary is
unreachable from the environment this was prepared in. It is faithful to the tool's convention
(checked against the pre-existing 4.38.0 entry), but a maintainer run of gh actions-lock should
be preferred if anything looks off. Because the symptom is startup_failure, it cannot be tested
locally — it is confirmed only by whether CodeQL/Hypatia next start.

---

⚠️ This PR's own checks did not run — they need a human trigger

Every workflow on this branch came back startup_failure, including Agda. The reason is the
triggering actor, not the content:

arena/01a0e040-echo-types  actor=hyperpolymath              -> Agda RAN
arena/01a0e508-echo-types  actor=arena-ai-coding-agent[bot] -> Agda startup_failure

Both are pull_request events on arena/* branches. When the trigger is the
arena-ai-coding-agent[bot] App, no workflow is created at all. gh run rerun is refused with
"its workflow file may be broken".

To get CI to verify the Agda fix, close and reopen this PR as a human, or push any commit to
the branch. Everything below is unverified until that happens.

[coderabbitai]

Important

Review skipped

Bot user detected.

To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: 8f931795-7bbf-47e4-834f-7a8a7b360f5a

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}