feat(type-theory): exploratory dendrogram → bridge index → ProofTransport receipt panel - #83
Merged
Merged
Conversation
…port receipt panel Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
arena-ai-coding-agent
Bot
requested a review
from hyperpolymath
as a code owner
September 27, 2026 04:12
|
Important Review skippedBot user detected. To trigger a single review, invoke the ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
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
approved these changes
Sep 27, 2026
arena-ai-coding-agent Bot
pushed a commit
that referenced
this pull request
Sep 27, 2026
main was rewritten to a new root (4c2c79e, PR #83) that shares no history with the revision this audit was written against (4a848da), and the audited code moved: Execution.jl +125/-60, estimation.jl +231/-29. ilr_basis.jl, analysis.jl, provenance.jl and bench/ilr_bases/benchmark.jl are byte-identical, so their citations are untouched. Re-verifies all 21 findings against the new tree -- the four headline ones (M3 dead clr_table, M4 redundant copies, N1 mixed healing scales, W1 is_dangerous not updated on :not_run) by reading the new code rather than trusting the old line numbers -- and re-locates every citation into the two files that moved. Also corrects the catalogue for work that landed after the audit: glmGamPoi dispersion is now a pure-Julia port (SUPPORTED_DISPERSION gains "glmgampoi"; only local/mean/pooled remain refused), so estimation.dispersion_refused no longer says "use parametric" for it. Adds three entries: the port itself, its unported spline abundance trend, and its pass-1 fallback; and records in the audit that two pure-Julia kernels now exist, which bears on question 10 without changing the gate (CI still has no verdict on any of this code). Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
arena-ai-coding-agent Bot
added a commit
that referenced
this pull request
Sep 27, 2026
) Follow-up to #85, which restored workflow startup. With CI alive again, the **Source lint** step (`config/ci/lint_source.jl`) produced its first verdict in two days and failed on two files it had never been able to run against — neither of them touched by #85: 1. **`test/doi/fixtures.jl`** uses the suite aliases `B`/`P`, which are `const` bindings defined in `tests.jl` before `include("fixtures.jl")`. The lint check is deliberately textual and per-file, so an alias supplied by the includer is invisible to it. The three call sites (`B.write_checksums!`, `P.prepare!`, `P.publish!`) now go through `Target.DOIBundles` / `Target.DOIPublications` — the same bindings at runtime (tests.jl defines them from `Target`), legible in isolation. 2. **`test/unit/test_zero_replacement.jl:215`** broadcast `Float64.(parse.(Float64, ...))` — the outer map is an identity (`parse` with a `Float64` target already yields `Float64`), and the `Float64.(` spelling matches the lint's `Module.member` pattern over test files. Removing the outer conversion changes no value. **Validation:** replayed the lint's textual checks (escaped interpolation, adjacent docstrings, bare-alias member refs, the `Float64.( pattern`) over both files — all clean. Julia itself isn't available in this sandbox, so the definitive gate is the CI Source lint step on this PR. **Known-red checks NOT addressed here** (pre-existing, not introduced by this change): repo-hygiene `tsc --noEmit` (frontend, likely #83-era), the stale apt-Agda 2.6.4.3 `Proofs (Agda)` job inside ci.yml (proofs.yml — the real gate — is green), and the DOI contracts job. Co-authored-by: arena-agent <arena-agent@users.noreply.github.com> 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.
Adds an exploratory type-theory work section. It is not wired into app routes, the server or the release.
What
type-theory/README.md: what the section is for and how it's laid out.type-theory/dendrogram-receipts/DESIGN.md: the design, what already exists across the estate, the selection policy, the DOM-performance rules, a proposed Protoctist.jlexport_bridge_index, and open questions.frontend/src/type-theory/dendrogram-receipts/: minimal TS/JSON contract:metamanifold.bridge-index/v1: node →epistemic_domain→ receipt stubs. Domain lists are pre-summed over each clade, so a click is one lookup.metamanifold.proof-transport-receipt/v1: statuses, modes and gaps mirror epistemic-types'ProofTransport.a2ml.proofs/agda.frontend/tests/unit/type-theory-dendrogram-receipts.test.ts: 8 tests, all passing. The new files type-check under the repo's strict tsconfig.Not in this PR
epistemic_domain, the bridge index and JEG aren't defined anywhere in the estate yet, so this PR defines the first two and puts JEG behind a smallDendrogramHostinterface.The open questions are listed in DESIGN.md §7.