feat: Phase 1 — canonize binding-graph interlingua + INV-26 neutrality

Declares SemanticSymbolicBindingGraph the universal problem-structure interlingua
(the corpus callosum where the geometric field and symbolic ROBDD decodings meet
and must agree). INV-26 enforces that neutrality structurally: 26a no binding-graph
module imports field/algebra/eval/vault/chat/core/sensorium; 26b the core imports
no domain reader (only allowlisted bridges adapter/question_target may); 26c proven
non-vacuous (flags pipeline.py's field import + the adapter's domain import).

Amends the plan doc with the structurally-diverse checkable panel (logic/grounding/
dimensional/execution/constraint, each with independent gold) and the 'a capability
change must move >=2 structurally-distinct domains or it is suspected overfitting'
rule, woven in from Phase 2 — the anti-overfit instrument the train_sample breach
proved we need.

Validated: architectural invariants 49 + binding_graph model = 118 passed.
This commit is contained in:
Shay 2026-06-04 16:20:12 -07:00
parent 0932c0e92e
commit 8d620d6257
3 changed files with 193 additions and 2 deletions

View file

@ -137,7 +137,9 @@ genuine second derivation. Cannot → we learned it cheaply and honestly.
gold. Gate to everything geometric.
- **Phase 2 — comprehension compiler → binding graph** (finite-entity grounding
first), with **field ⟂ symbol agreement** as the admission gate from the moment
Phase 1.5 succeeds.
Phase 1.5 succeeds. **The diversity panel starts here** (see cross-cutting): the
compiler is validated against ≥2 structurally-distinct golded domains from its
first commit, so it cannot overfit to math-shaped problems.
- **Phase 3 — activate `t2_precision`.** The field⟂symbol agreement *is* the t2
signal; wire the propose-loop consuming `checker="t2_precision"`. No invented
second derivation needed — it is real now.
@ -152,7 +154,35 @@ genuine second derivation. Cannot → we learned it cheaply and honestly.
modality becomes "just another reader" grounding into the universal structure;
stays afferent/gated per ADR-0198.
### Cross-cutting (every phase) — checkable budgets, adjoints, phenomenology
### Cross-cutting (every phase) — diversity panel, checkable budgets, adjoints, phenomenology
- **Structurally-diverse checkable panel (the anti-overfit instrument) — woven in
from Phase 2, not deferred to Phase 5.** Multi-domain diversity is not a morale
tool bolted onto the plan; it *is* the experiment that confirms or refutes the
central thesis (that *different* subjects compile into the *same* universal
structure and are handled by the *same* solve/verify machinery). The defining
failure of this project was a single gameable ruler (the 50-case train_sample)
hiding unsoundness for weeks; the antidote is a panel of **structurally distinct**
domains, each with a **genuine independent gold** (the INV-25 bar — a verifier
sharing no code with the engine). Adding a domain *without* real independent gold
is worse than useless: it is another gameable ruler. The cheap, strong starting
panel (logic / grounding / dimensional / execution / constraint, all with real
gold):
- **deductive logic** (ROBDD vs. truth-table oracle) — shipped.
- **finite-entity grounding** (ROBDD/oracle gold; Phase 2).
- **units / dimensional analysis***nearly free*: the binding graph already
carries dimensional algebra, so "does the answer's dimension check out" is an
independent structural gold.
- **systems/software** (execution = gold; Phase 5) — the strongest verifier.
- **a small constraint/scheduling domain** (brute-force/SMT gold).
**The discipline (adopt now):** *a capability change must move ≥2 structurally-
distinct domains, or it is suspected overfitting until proven otherwise.* Make the
panel a first-class CI signal alongside GSM8K so progress is never read from one
flat number. Honesty note: a domain with no adequate pack yet simply refuses
everything — that is a *coverage* signal (a breadth map), not a *capability*
signal. Capability credit counts only where there is a real pack **and** a real
gold **and** committed (non-refused) agreement.
- **Distortion budgets as first-class CI gates**, but *only checkable ones*:
grounding completeness %, unit-proof coverage, acyclicity, and **structural

View file

@ -1,5 +1,24 @@
"""ADR-0132/0133/0134/0135 — Semantic-Symbolic Binding Graph.
**The universal problem-structure interlingua** (see
``docs/analysis/universal-structure-and-field-symbol-coherence-gate-2026-06-04.md``).
This is the one typed, field-agnostic structure that every reader (math,
deductive logic, future modalities) compiles *into* and every solver/verifier
operates *on*: a unit-aware, provenance-carrying (:class:`SourceSpanLink`),
acyclic, refusal-first DAG. It is the corpus callosum where holistic
comprehension commits to an inspectable, checkable form and hands off to
analysis not the master and not a mere servant.
**Neutrality doctrine (enforced by INV-26).** The interlingua must depend on
neither the field engine, nor any one domain's reader, nor the eval/runtime: the
core model imports nothing from ``field`` / ``algebra`` / ``evals`` / ``vault`` /
``chat``, and only the designated *bridge* modules (:mod:`.adapter`,
:mod:`.question_target`) may import a domain reader. Servants propose into the
structure and check it; they never become the structure. Keeping the meeting
point neutral is what lets two independent decodings (geometric field and
symbolic ROBDD) agree *here* the coherence that makes a committed answer
``wrong == 0``-safe.
Phase 1 (ADR-0132): pure data layer (frozen dataclasses, deterministic
allocator, refusal-first construction; no I/O, no parser, no algebra,
no ``Polynomial`` coupling symbolic expressions held as canonical

View file

@ -1242,3 +1242,145 @@ class TestINV25IndependentGold:
"entailed/refuted signal, so INV-25b cannot catch a soundness break. "
"Add non-trivial cases before claiming the lane proves capability."
)
# ===========================================================================
# INV-26 Interlingua neutrality — the universal problem-structure does not
# depend on the field engine, any one domain reader, or eval/runtime
# ===========================================================================
#
# Claim (docs/analysis/universal-structure-and-field-symbol-coherence-gate-
# 2026-06-04.md §2; ADR-0132 "no algebra" rule made structural):
#
# The binding graph is the corpus callosum where two independent decodings
# (the geometric field and the symbolic ROBDD) must be able to meet and
# AGREE. That is only sound if the meeting point is NEUTRAL: if the
# interlingua imported the field engine, a benchmark, or a single domain's
# reader, "agreement at the interlingua" would be agreement-with-oneself —
# the same blind spot INV-25 guards for gold. So:
#
# 26a No binding-graph module imports the field engine, eval, vault, or the
# runtime (``field`` / ``algebra`` / ``evals`` / ``vault`` / ``chat`` /
# ``core`` / ``sensorium``). The structure is engine/benchmark/runtime-
# neutral.
# 26b The binding-graph CORE (everything but the allowlisted bridge modules)
# imports nothing outside the standard library and its own package —
# in particular no domain reader. Only the bridges (``adapter``,
# ``question_target``) may translate a domain reader into the structure.
# 26c Non-vacuity: a module that imports a forbidden family is shown to be
# flagged, proving 26a/26b can fail.
#
# A new bridge (a new domain reader translated into the structure) is allowed,
# but must be added to BINDING_GRAPH_BRIDGES explicitly — that is the reviewable
# seam where a domain couples to the universal structure.
_BINDING_GRAPH_DIR = "generate/binding_graph"
# Engine / benchmark / runtime families the interlingua must never import.
_INTERLINGUA_FORBIDDEN_PREFIXES: tuple[str, ...] = (
"field", "algebra", "evals", "vault", "chat", "core", "sensorium",
)
# The only modules permitted to import a domain reader (they translate one
# domain's reader output into the neutral structure).
BINDING_GRAPH_BRIDGES: frozenset[str] = frozenset({
"adapter.py",
"question_target.py",
})
def _binding_graph_modules() -> list[Path]:
return sorted((_REPO_ROOT / _BINDING_GRAPH_DIR).glob("*.py"))
def _is_internal_or_stdlib(mod: str) -> bool:
"""True if an imported module name is the structure's own package."""
return mod == "generate.binding_graph" or mod.startswith("generate.binding_graph.")
class TestINV26InterlinguaNeutrality:
"""The universal problem-structure stays neutral to engine, benchmark, and
runtime, and its core depends on no single domain reader."""
def test_binding_graph_dir_exists(self):
mods = _binding_graph_modules()
assert mods, (
f"no binding-graph modules found under {_BINDING_GRAPH_DIR}"
"INV-26 would be vacuous (did the package move?)."
)
def test_no_module_imports_engine_eval_or_runtime(self):
"""26a — the interlingua never touches field/algebra/eval/vault/chat/
core/sensorium. Agreement at a neutral meeting point is real; agreement
at a point coupled to one engine is agreement-with-oneself."""
offenders: list[str] = []
for path in _binding_graph_modules():
mods = _module_imports(path)
hits = _imports_any_prefix(mods, _INTERLINGUA_FORBIDDEN_PREFIXES)
if hits:
offenders.append(f"{path.name} imports {hits}")
assert not offenders, (
"Binding-graph (interlingua) module couples to the engine/eval/"
"runtime:\n " + "\n ".join(offenders)
+ "\n\nThe universal structure must stay neutral so two independent "
"decodings can meet and agree there (INV-26a). Move the coupling out, "
"or it is not an interlingua."
)
def test_core_imports_no_domain_reader(self):
"""26b — only the allowlisted bridges may import a domain reader; the
core imports nothing outside stdlib + its own package."""
offenders: list[str] = []
for path in _binding_graph_modules():
if path.name in BINDING_GRAPH_BRIDGES or path.name == "__init__.py":
continue
external = [
m for m in _module_imports(path)
if m.startswith("generate.") and not _is_internal_or_stdlib(m)
]
if external:
offenders.append(f"{path.name} imports domain module(s) {sorted(external)}")
assert not offenders, (
"Binding-graph CORE imports a domain reader (couples the universal "
"structure to one domain):\n " + "\n ".join(offenders)
+ "\n\nTranslate the domain via a bridge module and add it to "
"BINDING_GRAPH_BRIDGES, or keep the core domain-agnostic (INV-26b)."
)
def test_bridges_exist_and_are_used(self):
"""Drift guard: every allowlisted bridge must exist and actually import a
domain reader, else the allowlist is stale and 26b is weakened."""
present = {p.name for p in _binding_graph_modules()}
missing = BINDING_GRAPH_BRIDGES - present
assert not missing, f"BINDING_GRAPH_BRIDGES names non-existent module(s): {missing}"
unused: list[str] = []
for name in sorted(BINDING_GRAPH_BRIDGES):
mods = _module_imports(_REPO_ROOT / _BINDING_GRAPH_DIR / name)
if not any(m.startswith("generate.") and not _is_internal_or_stdlib(m) for m in mods):
unused.append(name)
assert not unused, (
f"Allowlisted bridge(s) no longer import a domain reader: {unused}. "
"Remove from BINDING_GRAPH_BRIDGES to keep the coupling seam tight."
)
def test_neutrality_check_is_non_vacuous(self):
"""26c — prove 26a/26b can fail: a real module that imports a forbidden
family must be flagged by the same predicate."""
# core/cognition/pipeline.py imports field.state (engine) — 26a must flag it.
pipeline = _REPO_ROOT / "core" / "cognition" / "pipeline.py"
if pipeline.is_file():
hits = _imports_any_prefix(_module_imports(pipeline), _INTERLINGUA_FORBIDDEN_PREFIXES)
assert hits, (
"INV-26a predicate failed to flag a module known to import the "
"field engine — the neutrality check is vacuous."
)
# The bridge adapter imports a domain reader — 26b's predicate must see it.
adapter = _REPO_ROOT / _BINDING_GRAPH_DIR / "adapter.py"
external = [
m for m in _module_imports(adapter)
if m.startswith("generate.") and not _is_internal_or_stdlib(m)
]
assert external, (
"INV-26b predicate failed to detect the adapter's domain-reader "
"import — the core-isolation check is vacuous."
)