feat(applications): haplotype collapsing as Echo fiber - #327
Merged
Merged
Conversation
- New Agda anchor EchoHaplotypeCollapsing: Clone -> Haplotype non-injective collapse, HaploFiber = Echo collapse h as structural lineage, no-canonical-clone-recovery via no-section-of-collapsing-map, aggregation-as-fold via sumMonoid, FiberBundle sidecar, HaploDist separation (domain = B not Echo f) - Applications directory: README index, haplotype-collapsing.adoc (full answer to Echo fiber + Nickel schema + Julia exacts matrix O(m^2) + JEG display + choreographic framing), choreographic-types.adoc carrier note - Nickel schema haplotype-collapsing.k9.ncl: CollapsedResult with m x m distance_matrix, fibers Dict as Σ B (Echo f) sidecar, contracts for count, keys, square matrix - Julia shadow haplotype-collapsing.jl: collapse_clones O(n) grouping + O(m^2) distances, fiber sidecar O(n) not in hot loop, tests for no-section and aggregation-as-fold, cost-model benchmark, JEG React sketch - Wired into All.agda + Smoke.agda, MAP.adoc applications section Answers: pass homotopy fiber witness through Nickel as validated sidecar, Julia exacts matrix stays O(m^2) on Haplotype representatives, JEG displays lineage by expanding fibers O(k) without recompute. Choreographic framing: Sequencer ⊑ Collapser ⊑ Visualizer = keep ≤ residue ≤ forget. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
Navigate logical layers of code changes, visualize relationships, and explore their blast radius. Note Currently processing new changes in this PR. This may take a few minutes, please wait... ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: 📒 Files selected for processing (9)
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. Comment |
hyperpolymath
pushed a commit
that referenced
this pull request
Sep 27, 2026
…rBundle (#328) 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`: ```agda 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. ```agda 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. #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. --------- Co-authored-by: arena-agent <agent@arena.ai> Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Answers: pass homotopy fiber witness through Nickel as validated sidecar, Julia exacts matrix stays O(m^2) on Haplotype representatives, JEG displays lineage by expanding fibers O(k) without recompute. Choreographic framing: Sequencer ⊑ Collapser ⊑ Visualizer = keep ≤ residue ≤ forget.
Summary
Closes #
Type of change
How has this been verified?
Checklist
git commit -S).SPDX-License-Identifier(code/configMPL-2.0,prose
CC-BY-SA-4.0); I did not relicense existing files.Notes for reviewers