Skip to content

§5 de-fork activation arbiter: grounded cross-tree admission witness (host-tagged ingest, no explicit MoreFundamental) - #5506

Merged
briansrls merged 1 commit into
mainfrom
session/still-deer-248-witness
Jun 22, 2026
Merged

briansrls merged 1 commit into
mainfrom
session/still-deer-248-witness

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Jun 22, 2026

Copy link
Copy Markdown
Contributor

What

The §5 de-fork activation arbiter: a by-execution witness proving cross-tree import is LIVE on the real grounded compile path, derived from filesystem-truth source_root tags — the gate that unblocks the de-fork collapse fan-out.

Why

#5473 + #5486 landed the grounded source_root carrier on DagSourceReadWitness + the grounded tree-pair relation (tree_fundamentality_order). The existing name_resolve_cross_tree_resolution_test proves resolve_with_admission_grounded admits v2→dsl given a hand-built index. The unproven leg was whether the carrier is actually consumed end-to-end: host tags → program-built index → grounded decision. "Structurally wired != proven until it runs green."

How (the real machinery, nothing supplied)

Feeds a host-tagged SourceRootIngest through:

  • program_assembly_fold_ingest → builds the QualifiedName → SourceRootRef index from each read's source_root tag,
  • source_root_set_from_ingest → builds the active source-root set from the same tags,
  • cross_tree_edge_decision → the exact fn admit_import_entry calls.

No explicit MoreFundamental anywhere — it is derived by tree_fundamentality_order. (That is the illusion the audit doc names: the explicit-supply test only passes because it hands the order in.)

Verdict (by execution, gunbc run --claim-run)

  • v2-subject (V2Tree) → dsl-target (DslTree) ⟹ EdgeCrossAdmitted (true)
  • tags reversed (dsl-subject → v2-target) ⟹ EdgeCrossDenied (true)

Asserts the exact decision variant (not a Bool proxy), so the RED leg cannot pass for a wrong reason. Flip either source_root tag and the witness goes the wrong way — the discriminating oracle. ⟹ cross-tree activation is live on current main; the de-fork fan-out is unblocked.

Floor-auto-enrolled via _test.dag naming.

🤖 Generated with Claude Code

…n from host tags

The remaining activation gate: prove by execution that the source_root carrier (#5473/#5486)
is CONSUMED on the real grounded compile path, not merely carried. Feeds a host-tagged
SourceRootIngest through the real machinery — program_assembly_fold_ingest builds the
QualifiedName->SourceRootRef index, source_root_set_from_ingest builds the active-root set —
then runs cross_tree_edge_decision (the exact fn admit_import_entry calls). Nothing about
fundamentality is supplied; MoreFundamental/LessFundamental is derived by tree_fundamentality_order.

By execution (gunbc run --claim-run):
- v2-subject (V2Tree) -> dsl-target (DslTree)  => EdgeCrossAdmitted  (true)
- tags reversed: dsl-subject -> v2-target       => EdgeCrossDenied    (true)
Asserts the exact decision variant (not a Bool proxy) so the RED leg cannot pass for a wrong
reason. Flip either source_root tag and the witness goes the wrong way (discriminating oracle).

Verdict: cross-tree import is ACTIVE on current main, grounded on filesystem-truth source-root
tags — the de-fork collapse fan-out is unblocked. Floor-auto-enrolled via _test.dag naming.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@briansrls
briansrls merged commit b14bd56 into main Jun 22, 2026
1 check passed
@briansrls
briansrls deleted the session/still-deer-248-witness branch June 22, 2026 14:31
briansrls pushed a commit that referenced this pull request Jun 22, 2026
…-forks + 7 grounding cluster) (#5511)

* §5 de-fork audit: re-verdict census by execution — 2 mirrors + 2 not-a-forks + 7 grounding cluster

The dsl↔v2 std fork is not "mostly temp v2 mirrors": by-execution decl-set comm
+ shared-type-body diff shows 2 true mirrors (reducible/measure), 2 pure
name-collisions (coercion/node), and 7 divergent groundings (algebra/logic/nat/
integer/float/effects/verification) — the same concept grounded on a different
axis/realization per tree (e.g. EffectShape: operation-axis in dsl vs
idempotency-class in v2; TestClaim simple-proposition vs grounded coproduct).
The grounding cluster is a single-authority unification DESIGN downstream of the
numeric tower (#5428) + model↔realization grounding, not a mechanical repoint.

Also: §1 updated — cross-tree import is ACTIVATED (#5473/#5486 grounded,
#5506 arbiter witness proves it live, #5504 fixed the abs-vs-rel admission bug);
the former "wired but off" blocker is dissolved. Structured §2 as operator
decision-input per concept (shared / shared-body-divergence / each-side-unique /
grounding-entanglement). DESIGN §6: a stale doc contradicting ground-truth is
parallel-representation debt.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* §5 audit: correct node/coercion to v1-artifact category (DEFER to v1-shrink)

verify-before-act caught a scoping error: importer greps omitted src/v1, and
src/v1 is a live consumer of dsl/std. node + coercion renames are NOT clean-lane
— both cascade into the v1 seed (04_infer inference stage import + emitted Rust
std_{node,coercion}.rs + a guard test). Per bright-stag's ruling, DEFER both to
v1-shrink: on v1-delete node self-dissolves (dead file → delete, no rename) and
coercion shrinks to a v1-free disambiguation (4 extdeps + v2). Census now has
THREE categories: (a) 2 true mirrors, (b) 7 grounding divergences, (c) 2
v1-artifact collisions. Recorded the dissolution trigger.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant