Commit graph

507 commits

Author SHA1 Message Date
Shay
991be784fa docs: field-reasoner wedge design + falsification dossier
Source-grounded design of the field<->symbol coherence-gate wedge, corrected by
an 11-agent adversarial review into a falsifiable experiment with a sanctioned
negative outcome (field stays a servant -> C3 two code-disjoint symbolic
readings). Records the substrate ledger (the CL(4,1) field has one exact strength
relevant to reasoning -- the conformal distance metric -- and no solver/incidence
machinery), the corrected design, the three adversarial verdicts, the falsifiable
experiment (ablation + per-class diversity), and the phased path.
2026-06-04 19:22:16 -07:00
Shay
f97fcaf453 docs: session record (2026-06-04) + mark runway PR-1/PR-2 shipped
Session journey: the deductive pivot (verified, not asserted), INV-25 independent-
gold ratification, the universal-structure + field<->symbol coherence-gate synthesis,
and the autonomous build of the foundation + 3-domain anti-overfit panel (#554-557).
Records the two field-as-reasoner findings (logic is combinatorial; independence must
live in the reading) that defer the geometric wedge to dedicated research.

Marks the deductive-logic runway's PR-1 (finite-entity grounding) and PR-2 (oracle
parity) as shipped via #556.
2026-06-04 16:54:03 -07:00
Shay
3e2a52870d feat: Phase 2 — finite-entity grounding compiler + Phase 1.5 finding
The first comprehension->structure compiler: evals/deductive_logic/grounding.py
lowers a typed finite-entity problem (finite entities + unary predicates +
single-variable universal rules) into the propositional regime the ADR-0206
entailment operator decides, refusal-first with a closed typed reason vocabulary
(unsafe_symbol / unknown_entity / unsupported_predicate_arity / unsupported_
quantifier / malformed_case / empty_case) and collision-safe atom slugging.

finite_entity/v1/cases.jsonl: 8 cases with INDEPENDENT (oracle-derived) gold
(4 entailed, 2 unknown, 1 refuted, 1 refused) — chained rules, conjunctive
bodies, negative heads, inconsistent premises. 20 tests gate engine==oracle==gold.

This is the second diversity-panel domain (distinct comprehension, same checkable
substrate) — the universal-structure thesis validated on a different problem shape,
with the anti-overfit >=2-domain discipline now live.

Phase 1.5 finding recorded: a clean geometric/algebraic propositional decoder
agrees 716/716 with the oracle but is O(2^n) (enumeration-class), so logic is the
wrong first domain for field-as-reasoner; the wedge redirects to quantitative-
relational structure where the field is the natural non-redundant decoder.
2026-06-04 16:32:03 -07:00
Shay
8d620d6257 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.
2026-06-04 16:20:12 -07:00
Shay
0ac725ccfd docs: plan — universal structure + field<->symbol coherence gate
Planning-only design doc for the comprehension->structure->solve->verify spine:
converge reading onto the binding-graph interlingua; field comprehends, structure
bridges, symbol verifies; their AGREEMENT is the wrong=0 gate and the genuine
second derivation that unblocks t2_precision. Field-as-reasoner must EARN each
domain against independent gold (Phase 1.5 wedge: field-decides-entailment vs
ROBDD oracle); never asserted unfalsifiably. INV-25 is Phase 0.
2026-06-04 15:56:28 -07:00
Shay
a447dce5d1 feat: ratify independent-gold invariant (INV-25) + SHA-pin deductive lane
INV-25 makes the GSM8K lesson structural: no capability claim is valid unless
its gold is computed by a procedure sharing no code with the system under test.
Three meaningfully-failing checks (proven able to fail): 25a oracle imports no
SUT module (AST); 25b every committed deductive gold is reproduced by the
independent oracle AND matched by the engine; 25c an unsound engine disagrees
on committed cases.

SHA-pin the deductive lane (deductive_logic_v1, dev+holdout+external 716/716,
wrong=0, refused=0) via a deterministic --report writer + run_as_module (the
lane dir's local generate.py shadows the package in script mode) + CLAIMS regen.

Fix drift the review surfaced: contract.md + pivot doc claimed an 8,000/7,340
fuzz and an 'external mirror' -> corrected to the real gated 3,000-case fuzz
(2,796 definite) and 'hand-authored, NOT a published-benchmark mirror'; pivot
doc GSM8K holdout 0->5 (all 5 are R1 reconstruction; composer scored 0).

Validated: smoke 78, deductive 23, proof 29, invariants 44, lane-sha+claims 9.
2026-06-04 15:56:28 -07:00
Shay
d4a07f23b1 docs: define deductive logic phase 2 benchmark runway 2026-06-04 09:33:23 -07:00
Shay
602a76221a docs: record the GSM8K->deductive-logic pivot, post-mortem, and plan
Load-bearing strategic record: what the GSM8K chase got wrong (overfit
50-case ruler hiding a sealed wrong=0 breach), the held-out measurement
that exposed real capability=0% / composer 17% wrong, why GSM8K is the
wrong terrain for a deterministic verifiable engine, and the deductive-
logic path now (Phase 1 done: 500/500 held-out wrong=0, independent-
oracle verified) with phases 2-4 and the anti-recurrence disciplines.
2026-06-04 07:51:36 -07:00
Shay
f301f3a928
Merge pull request #548 from AssetOverflow/feat/holdout-dev-set
feat(eval): held-out dev lane — honest iteration metric (real GSM8K capability = 0/500)
2026-06-04 07:14:58 -07:00
Shay
f56a0cfdba
Merge pull request #546 from AssetOverflow/docs/reconcile-current-state-2026-06-03
docs: reconcile current-state claims after GSM8K + sensorium progress
2026-06-04 07:14:39 -07:00
Shay
d4a002e626 docs: fourth lift attempt falsified (strict sum-reader 0/2) — exhaustive
Four genuine build-and-measure attempts on held-out, all falsified:
- composer 87 wrong, narrow reader 61 wrong, strict sum-reader 2 wrong (100%),
  candidate-graph 0 admissible. Even 'exactly 2 numbers + total cue' cases are
  multi-step in disguise. No sound committing strategy exists in this substrate.
2026-06-04 02:52:24 -07:00
Shay
c31bc82621 docs: third leg — candidate-graph builds 0 admissible candidates on held-out
All three GSM8K paths exhausted on the held-out 500:
- candidate-graph (sound filter): 0 admissible candidates built (498/500 build nothing)
- composer (open): 87 wrong
- narrow reader (open): 61 wrong
The sound path is wrong=0 only because it constructs no reading to commit. No sound
lift exists in the current substrate; confirmed empirically, three ways.
2026-06-04 02:49:00 -07:00
Shay
92e9631467 docs: two lift attempts falsified + the ADR-0207 architectural impasse
Built and measured two committing readers on held-out (not just diagnosed):
- resolve_pooled composer: 2 correct / 87 wrong (17%)
- maximally-narrow forced reader: 0 correct / 61 wrong (100% when it fires)

Shallow committing CANNOT be sound on real GSM8K (measured). The impasse:
- candidate-graph path is SOUND (wrong=0) but FROZEN by ADR-0207 §4, covers 0 real
- composer is OPEN (ADR-0207 §5) but UNSOUND (17% wrong, no separating gate)
ADR-0207's premise (composer is the wrong=0-safe path) is FALSIFIED by held-out data;
'feed the composer' is a path to more confabulation. Needs a follow-up ADR.
2026-06-04 02:47:03 -07:00
Shay
c2e74fe2fd docs: the honest real-GSM8K capability measurement (0% sound; composer 17% wrong on held-out)
The result that should have been visible for weeks. Measured on the new holdout_dev
lane (500 real held-out cases) + sealed test:
- real capability 0% (train_sample's 4 correct generalize to 0/500 held-out)
- resolve_pooled (the composition substrate) commits 17.4% WRONG on held-out
- NO structural gate (step/pool/op) separates its 2 correct from 87 wrong -> the
  composer cannot tell right readings from wrong; gating it is overfitting
- the only wrong=0 policy on real GSM8K is refusal (current serving 0/0/500)

Real lift needs a verifiable reading mechanism, not composer tuning. Non-serving (docs).
2026-06-04 02:42:14 -07:00
Shay
763c46d2f4 fix(gsm8k): disable unsound serving bridges — restore sealed wrong=0 (0/5 -> 0/0)
The FIRST real sealed measurement (operator-decrypted 1,319 held-out GSM8K)
found `0 correct / 5 WRONG` — a wrong=0 breach hidden for weeks because the
working metric was the 50-case train sample the bridges were tuned to. Bisection
isolated it to the product_bridge serving promotion (ADR-0195).

- generate/math_candidate_graph.py: REMOVE both serving promotion bridges
  (product_bridge + goal_residual/ADR-0207 §5 step 2). Serving = main-graph-only.
  Restores sealed 0/0/1319 (verified by bisect: disabling product_bridge -> 0 wrong).
  Production modules remain in generate/derivation/; only serving promotion is
  unwired, until a gate is proven wrong=0 on the SEALED set (never the train sample).
- Honest numbers everywhere: train_sample 7/43/0 -> 4/46/0 (the bridges' "correct"
  was train-overfit). report.json + coverage probe regenerated. 7 ADR test lanes
  de-pinned from the inflated count. corpus: cv-0005 (R4) reverts to refuse; cv-0020
  (a "baseline control" that solved ONLY via product_bridge) reclassified.
- docs/claims_ledger.md: dated wrong=0-breach-and-remediation note + the rule:
  the train_sample number had ZERO predictive validity for the exam; never the score.
- docs/analysis/gsm8k-lift-program-strategy: the program to actually move the 1,319.

NOTE the exit gate stays `correct>=10 AND wrong==0` — refusing-everything is an
explicit FAIL, not a wrong=0 pass; serving still commits (main graph). Verified:
broad regression 848 passed, smoke 73 passed.
2026-06-04 01:55:05 -07:00
Shay
399720817f docs: reconcile ADR-0207 execution status 2026-06-03 22:45:07 -07:00
Shay
e7392f118e docs: reconcile claims ledger with current state 2026-06-03 22:41:19 -07:00
Shay
3a72d69678
Merge pull request #545 from AssetOverflow/docs/ratify-sensorium-afferent
docs: ratify sensorium afferent ADRs + work-sequencing acknowledgment
2026-06-03 22:29:50 -07:00
Shay
7160e5e77f
Merge pull request #544 from AssetOverflow/feat/r4-goal-residual
feat(r4): cv-0005 goal-residual to serving — train_sample 6/44/0 → 7/43/0 (ADR-0207 §5 step 2)
2026-06-03 22:29:21 -07:00
Shay
bd6e0377e1 docs: ratify sensorium afferent ADRs + acknowledge arc in work-sequencing
Authority-ratified per the ADR-0207 convention (Accepted (ratified DATE)):
- ADR-0181 (audio), ADR-0197 (vision), ADR-0208 (environmental loop),
  ADR-0209 (sensorimotor afferent) -> Accepted (ratified 2026-06-03).
  All four are implemented + test-backed (0208/0209 falsifiability deeply
  verified in the lookback; 0181/0197 backed by CRDT-merge/compiler/mount/
  eval-gate suites, all green in the 182-test sweep).
- ADR-0198 deliberately NOT ratified: partially-implemented spike (Gap A +
  fail-closed efferent gate landed; \xc2\xa73 verdict-lowering + motor decoder
  deferred behind a dedicated motor governance ADR).

CLAUDE.md Work Sequencing now records the sensorium/modalities arc as a
sanctioned parallel track that does not displace the near-term sequence and
is disjoint from the GSM8K serving path. Markdown only; no test asserts ADR
status or the work-sequencing text.
2026-06-03 22:21:50 -07:00
Shay
ad9cf57069 feat(r4): flip cv-0005 to serving — train_sample 6/44/0 -> 7/43/0 (ADR-0207 §5 step 2)
Wires the R4 goal-residual production to serving via
resolve_promotable_goal_residual (math_candidate_graph.py, mirroring
product_bridge). cv-0005 / train_sample 0037 now solves on serving as
goal - Σprogress = 10 - 3 - 4 = 3. First Phase-5b composition lift on serving.

wrong=0 preserved on every runnable surface:
- train_sample 6/44/0 -> 7/43/0 (0037 added; 6 prior correct intact; wrong=0).
- Fires on 2/455 visible GSM8K cases, both correct, ZERO wrong.
- Gain-goal divergence firewall proves it reads the GOAL, not a possession.
- smoke 73, math+invariants 53, derivation/pool/practice 341, corpus, all green.

Lockstep updates (the ratified metric move, 6/44/0 -> 7/43/0):
- report.json; 7 ADR test lanes that pinned 6/44/0; corpus cv-0005 baseline
  fields + snapshot (4/18 -> 5/17) + contract; plan-doc cv-0018 control fix.

⚠ SEALED MEASUREMENT REQUIRED — NOT DONE. The sealed 1,319 (encrypted, not
CI-reproducible) is the real bar (ADR-0207 §6) and was NOT re-measured. The
operator/CI must decrypt+run it and confirm sealed wrong==0; if wrong>0, revert
the resolve_promotable_goal_residual block (isolated). See
docs/handoff/sealed-measurement-obligation-2026-06-04.md.
2026-06-03 22:20:12 -07:00
Shay
b4fb9df8e7 feat(sensorium): fail-closed efferent gate for actuating decode (ADR-0198 §3)
DefaultEfferentGate is a capability/shape pre-filter only; it does not
lower decoded actions into safety/ethics pack verdicts (ADR-0198 §3 /
§1.2 Gap B). ModalityRegistry.decode/decode_batch now refuse fail-closed
any emission through a gate whose enforces_action_verdicts is False,
unless an explicit allow_unverified_efferent sandbox opt-in is set.

A real motor decoder thus cannot emit through the capability-only gate;
the §3 verdict-lowering gate must be built and installed first. No
production caller of the decode path exists today, so this closes the
latent hazard before a motor decoder makes it load-bearing. Adds two
falsifiable tests (fail-closed refusal; verdict-enforcing gate allowed).
Disjoint from the GSM8K serving path.
2026-06-03 22:03:35 -07:00
Shay
e5bc73ebb9 docs: reconcile sensorium ADR statuses with shipped implementation
ADR-0181/0197/0208/0209 were marked Proposed despite test-backed
afferent implementations merged to main; flip to Accepted with
verifiable Implementation lines (paths + PRs + falsifiable tests).
ADR-0198's 'no implementation' status was stale (Gap A protocol
change + baseline efferent gate landed in #541); correct it and
document the deferred §3 safety/ethics verdict-lowering as an
explicit blocking obligation before any motor decoder mounts.
2026-06-03 21:51:59 -07:00
Shay
5ae377065e docs: composition-wall execution scope (ADR-0207 §5 step 2)
Three reviewed, non-serving analysis/handoff docs for the COMPOSITION lever.
Read-only; no serving code; train_sample 6/44/0 untouched.

- analysis/wiring-promotion-gate-brief: product_bridge is the only serving
  derivation tendril (two-token target whitelist); resolve_pooled refuses all
  ten R1/R4/R5/R6 positives and wrong-commits 0016 -> 510. Wiring is trivial;
  the gate is the work.
- analysis/composition-wall-execution-plan: per-case stage taxonomy (A/B/C/D)
  for all 15 corpus positives, reproduced live; R4-first scope (new
  goal-residual production, verified by code-read of accumulate.py, NOT a
  target tweak); promotion gate generalizes product_bridge, never disagreement
  alone; gates inherit ADR-0207 §6 (corpus + sealed 1,319).
- handoff/stage-c-composition-investigation: dispatch task for the execution
  lane to pin the per-case bail for the production-wrong shapes (the real
  grouping/op-order wall), read-only, in-tree.
2026-06-03 21:14:02 -07:00
Shay
d9fc7f9e56
Merge pull request #540 from AssetOverflow/codex/vision-eval-environment-sensorimotor
[codex] Add vision evidence and sensorimotor contracts
2026-06-03 20:41:10 -07:00
Shay
2d2b096784 Add vision evidence and sensorimotor contracts 2026-06-03 20:27:46 -07:00
Shay
a6c36cc26f docs: amend ADR-0207 §5 step 1 — WIRING not the lowest-risk crux (tree-verified)
Reading the actual gate logic (product_bridge/pool/verify) corrected §5's
sequencing optimism, before merge:

- The safe wire is already done (product_bridge at :530); its safety is a
  two-token target whitelist (money+make/earn, weight+total/move) hardcoded to
  0003/0021 — it generalizes nothing.
- Verified live (2026-06-03): the general composer resolve_pooled refuses ALL
  ten R1/R4/R5/R6 corpus positives (R1/R4 build zero candidates; R5 only wrong
  ones) -> wiring yields +0 correct; and it wrong-commits 0016 -> 510, so wiring
  it wholesale is a live wrong=0 regression the disagreement rule does not catch.

So WIRING and COMPOSITION are the same task: composer production per shape, each
behind a structural promotion gate (extract_target + target_units, not
disagreement alone); the wire is the trivial last step. Core ratification
(freeze, design-of-record, gates, sealed-set measurement) unchanged.
2026-06-03 20:13:03 -07:00
Shay
fc01be715c
Merge pull request #537 from AssetOverflow/codex/sensorium-compiler-vision
[codex] Add sensorium compiler law and tile vision
2026-06-03 20:09:31 -07:00
Shay
282679bd85 Add sensorium compiler law and tile vision 2026-06-03 19:58:36 -07:00
Shay
94bf1be1bc docs: ratify ADR-0207 — GSM8K comprehension/composition substrate
Consolidating ratification of the GSM8K design of record. Ratify the built
comprehension/derivation substrate, freeze the serving regex recognizer/
injector path to lexemes + refusal-only, pin Phase 5b execution to
WIRING -> COMPOSITION -> LEXICON.

- ADR-0207: new consolidating decision (Accepted, ratified 2026-06-03).
  Supersedes ADR-0163 §Phase B-E + ADR-0136 regex sentence-template
  prescriptions. Freeze + wrong=0 gates (22-case corpus + sealed 1,319).
- ADR-0164/0165/0174/0178/0179: -> Accepted (ratified by ADR-0207,
  2026-06-03). 0164 keeps its implementation clause (Phase 1+2 shipped;
  remainder per §5) so Accepted != fully built.
- composition_validation/v1: 20 -> 22 cases (2nd R4/R5 positives,
  dataset-sourced golds), +contract invariants 6-7, +dataset-gold test.
  Baseline 4/18/0; 47 passed.
- docs/analysis: extraction-richness audit (read-only) reconciling
  ADR-0179 to the tree (EX-1/2/4/5/6 landed; EX-3 deferred).

Non-serving (evals/docs/tests only). train_sample 6/44/0 unchanged;
no-ref <N> times hazard stays refused. GB3b/0136 untouched.
2026-06-03 19:42:47 -07:00
Shay
b2b3678deb docs: mark ADR-0174 Phase 5a shipped in composition-capability-scope
Phase 5a (retire the inert GSM8K scoring-path comprehension-reader
dispatch, -1,038 LOC) landed in 3fd3172, an ancestor of HEAD 8327c6b,
but composition-capability-scope.md still listed it as remaining work --
drift that mis-scoped a downstream brief. Re-anchor the canonical doc to
the tree:

- §1: the lifecycle.py GSM8K-scoring dispatch row now reads "retired in
  Phase 5a (3fd3172)" instead of "inert ... retirable in 5a".
- §2: Phase 5a marked SHIPPED with a runway-status banner; the §9
  completeness-gate precondition marked LANDED (PR #534, e1bcdf6).
- §4: sequencing restructured -- items 0 (§9 precondition), 1 (gating
  analysis), 3 (5a) are DONE; the live runway starts at item 2 (the
  <=20-case validation sub-corpus), then Phase 5b.
- §9: status banner noting the recommended guard landed (#534); the
  "RED on main" statements are the pre-landing measurement, kept for
  provenance.

Docs-only. No code/eval/serving change. Baseline re-verified at HEAD:
train_sample 6/44/0 (all 44 refusals at branches_enumerated=0),
completeness-guard suite 21 passed.
2026-06-03 16:23:53 -07:00
Shay
018181c95b Add canonical composition analysis docs 2026-06-03 15:35:58 -07:00
Shay
e1bcdf6286 Harden no-reference n-times comparative guard 2026-06-03 15:22:42 -07:00
Shay
d5872a2e96 feat(adr-0206): response-governance bridge scaffold (STRICT-only, inert)
Adds the first consumer of CORE's two built epistemic substrates — the
decode-state taxonomy (core/epistemic_state.py) and the risk-reward
reliability gate (core/reliability_gate/, ADR-0175) — beginning to close
the LABEL-ONLY consumption gap they sat behind.

Ships the scaffold only:
- core/response_governance/policy.py — ReachLevel (STRICT < APPROXIMATE <
  EXTRAPOLATE < CREATIVE), ReachPolicy, govern_response (STRICT-only stub),
  shape_surface (STRICT = identity transform; higher levels real but
  unreachable in production), and the 9/5/1 EpistemicState partition.
- chat/runtime.py — cognition-path seam: the response surface now flows
  through shape_surface(govern_response(...)). STRICT = identity, so the
  path is byte-identical to pre-bridge. reach_level carried on ChatResponse.
- core/physics/identity.py — reach_level on TurnEvent (default "strict").

wrong==0 untouched: select_self_verified is NOT touched (ADR-0206 §5);
reach_level is NOT added to the telemetry JSONL dict, so pinned lane SHAs
stay byte-identical. Widening, SITUATE/FEED-BACK, the math-serving seam,
and the EVIDENCED reconcile are deferred to their own PRs.

Tests (tests/test_response_governance.py): STRICT-only contract over all
states x license x stakes, STRICT identity, live-wiring proof (forces
APPROXIMATE -> policy-sensitive surface), total+disjoint taxonomy
partition. Each fails loudly under the violation it guards.
2026-06-03 10:39:12 -07:00
Shay
64f3da18a7 feat: modus_ponens + disagreement rule — proof_chain wrong=0 mechanism (ADR-0205)
Phase 2.3: the first inference rule + the wrong=0 mechanism for proofs.

- generate/proof_chain/rules.py: evaluate_modus_ponens / evaluate_proof_conclusion.
  Proof-layer dispatch (Option B) over proposition FORMULAS via the canonicalizer;
  never touches check_admissibility/_resolve_dep_units (proofs have no units).
  Disagreement rule = the select_self_verified twin: pool ALL admissible single-step
  MP derivations, require a unique canonical key == declared conclusion. Pooling (not
  filter-to-declared-first) is the soundness mechanism.
- generate/logic_canonical.py: parse_top_implication (+ _unparse) — recovers an
  implication's syntactic antecedent/consequent (the ROBDD form doesn't preserve it).
- Closed typed-reason set; the corpus's finer labels consolidate (6 disagreement
  refuse-labels -> conclusion_disagreement; 4 antecedent-flavor labels ->
  unestablished_antecedent — same redundancy, same mechanism-makes-one-distinction
  principle).
- Honesty boundary (exact scope): guarantees a unique conclusion among SINGLE-STEP MP
  over the premises, NOT "uniquely entailed" by all strategies.

Cross-check: all 24 GPT-5.5 adversarial corpus cases agree on OUTCOME against the real
rule (no rule bug / no corpus outcome-misread); reasons consolidate as above.
Mutation: filter-to-declared-first makes DISAGREE-007/010 wrongly admit -> pooling
tests fail (pooling load-bearing).

Drive-by fix (cleanup-as-you-find): merged ADR-0204 ProofNode.__post_init__ was
dedented to module level -> all ProofNode validation was silently DEAD (smoke skips
the dedicated test file; the smoke != full-suite hazard). Re-indented; validation
restored.

Additive (math lane untouched). Full binding-graph surface green; smoke 67.
2026-06-02 20:56:57 -07:00
Shay
0850e6fde7
Merge pull request #527 from AssetOverflow/feat/adr-0204-proof-builder
proof_chain 2.2: proof-graph builder (ADR-0204)
2026-06-02 20:22:34 -07:00
Shay
4cae904563 feat: proof-graph builder — proof_chain's first binding-graph consumer (ADR-0204)
Phase 2.2, structure only (no inference rule — modus_ponens is 2.3). Translates a
Proof into a SemanticSymbolicBindingGraph; the ADR-0203 acyclicity guard + ADR-0132
referential integrity fire at construction.

- generate/proof_chain/model.py: the one canonical proof input shape (ProofNode/Proof
  + proof_from_premises desugaring of the corpus premises/conclusion shape).
- generate/proof_chain/builder.py: build_proof_graph — node→symbol+equation;
  canonical_key→rhs_canonical, depends_on→dependencies, rule→operation_kind;
  premises = empty-deps/op="premise"; unit_proof=PROOF_NO_UNIT, admissibility="pending";
  conclusion tracked as conclusion_symbol_id.
- tests: 9 — valid DAG (PC-MP-001 desugared) + multistep construct; PC-CYCLE-001
  refuses THROUGH the real builder (circular_dependency); canonical_key round-trips
  byte-identical + equivalent formulas share rhs_canonical; admissibility-dispatch
  confirmation; self/dangling refusals; out-of-regime node refuses. Mutation-verified
  (drop dep-wiring -> cycle admitted -> test fails).

Admissibility dispatch confirmed graceful on proof operation_kinds: unknown kinds
-> AdmissibilityError(unknown_operation), unitless deps -> unit_unbound; NEVER
misroutes into _check_additive. Named 2.3 constraint: check_admissibility runs
_resolve_dep_units before dispatch, so modus_ponens must bypass unit-resolution.

Open items named for 2.3 (ADR-0204): conclusion typing (BoundUnknown revisit),
semantic_role="unknown" (closed vocab has no "proposition"), unit_proof sentinel.

Additive (first consumer; math lane untouched). Full binding-graph surface green;
smoke 67. Honesty boundary: through 2.3, sound over declared atoms, not grounded in input.
2026-06-02 19:53:41 -07:00
Shay
15307ca1f3 Add proof-chain corpus fixtures 2026-06-02 19:26:46 -07:00
Shay
69a7d8bae8 feat: principled out-of-regime detector — typed out_of_decidable_regime (ADR-0201.1)
GPT-5.5's independent corpus caught that the canonicalizer refused quantified/
predicate input only by accident (tokenizer chokes on '.'), not by design — a
by-luck-not-by-design refusal the wrong=0 discipline rejects. ADR-0202 §3 names a
typed `out_of_decidable_regime` refusal; the keystone emitted a generic grammar error.

- logic_canonical.py: LogicRegimeError(LogicError) + OUT_OF_DECIDABLE_REGIME;
  _reject_out_of_regime_text (quantifier words forall/exists + symbols ∀/∃, pre-scan)
  and _reject_out_of_regime_tokens (predicate-application ATOM-then-LPAREN), run BEFORE
  the generic grammar error. Refusal only — no predicate/FOL capability added.
- logic_equivalence.py: typed regime branch (before the generic LogicError branch).
- tests: 43 total (10 new) — OOR refuses with typed reason; equivalence path too;
  genuine grammar errors stay plain LogicError (no over-fire); `not (P)` not mistaken
  for predicate application. Mutation-verified by-design (neuter -> falls through to
  generic grammar error).
- ADR-0201.1: additive sub-ADR of 0201 (not an amendment; sub-number preserves the
  landed ADR-0203 forward refs + phase-2 plan numbering). Honesty boundary load-bearing.

Corpus now 22/22 (PC-OOR-001/002 agree on the principled reason). Full canonicalizer
suite green; smoke 67 passed. modus_ponens rule-reasons remain deferred to ADR-0205 (2.3).
2026-06-02 19:12:41 -07:00
Shay
451c4b1e17 feat: binding-graph acyclicity invariant — circular_dependency guard (ADR-0203)
proof_chain phase 2.1: the acyclicity guard at the shared binding-graph
construction boundary, before phase 2.2 wiring can build a cyclic-capable structure.

- generate/binding_graph/acyclicity.py: pure find_cycle(adjacency) detector
  (deterministic three-colour DFS; isolated, no model import).
- model.py __post_init__: builds {lhs: deps} adjacency over equations and raises
  BindingGraphError(circular_dependency ...) on a cycle. Runs on every binding
  graph (math + future proof) — illegal states unrepresentable for all consumers.
- tests/test_binding_graph_acyclicity.py: 17 tests (pure checker + construction
  enforcement); mutation-verified non-vacuous.
- ADR-0203: new ADDITIVE invariant referencing ADR-0132 (not an amendment —
  preserves the why-added-later history).

Math-lane regression proof: the only producer (math adapter) is acyclic by
construction (fresh result symbol per op, deps point backward); full
binding-graph + admissibility surface 392 green; guard refuses no existing graph.

Honesty boundary (load-bearing): through phase 2.3, proof_chain is SOUND OVER
DECLARED ATOMS, not grounded in recognized input (grounding is phase 2.4).

full binding-graph/admissibility surface: 392 passed. smoke: 67 passed.
2026-06-02 18:42:40 -07:00
Shay
e8e0fbb014 feat: propositional canonicalizer keystone + representation contract (ADR-0201/0202)
The proof_chain keystone: a hand-rolled ROBDD canonicalizer mirroring
math_symbolic_equivalence one domain over (normalize -> canonical key ->
byte-equality -> three-valued verdict; REFUSED preserves wrong=0).

- generate/logic_canonical.py: formula -> ROBDD identity under sorted-atom
  ordering; LogicError/LogicBudgetError refusals; inspectable canonical key.
- generate/logic_equivalence.py: EQUIVALENT/NOT_EQUIVALENT/REFUSED wrapper.
- tests/test_logic_canonical.py: 33 standalone tests (canonicity laws,
  discrimination, terminals, determinism, refusals); mutation-verified non-vacuous.
- ADR-0201: canonicalizer decision (ROBDD not CNF/DNF; hand-rolled;
  propositional-only honesty boundary).
- ADR-0202: proposition representation contract — single source the canonicalizer
  and the proof corpus conform to (formula grammar + atom layer binding to ADR-0144
  EpistemicNode + honesty boundary).

Additive: no existing file touched, zero consumers. Standalone keystone only;
binding-graph wiring, acyclicity refusal, and inference rules deferred. smoke: 67 passed.
2026-06-02 16:24:32 -07:00
Shay
b2d1125743 Add Brain Corp technical brief
1-page exec + backing brief for a first technical conversation, written to
survive a skeptical CTO. Every number/status sourced to docs/claims_ledger.md;
substrate-beneath-BrainOS framing held (not perception/motor); verify block is
fresh-clone-green. Prepared for internal review — not for distribution.
2026-06-02 12:07:32 -07:00
Shay
f3680aa302 reconcile amr demo wording with claims ledger 2026-06-02 10:38:00 -07:00
Shay
99c94f71f0 add amr decision substrate demo 2026-06-02 10:38:00 -07:00
Shay
2d18976fa4 docs(claims): ADR-0200 reconciliation — expert claim to audit-passed truth
Reconcile every artifact that asserted the (since auto-reverted) mathematics_logic
expert promotion to the live machine state. Determinism proven intact (Week-1a):
the digest divergence is genuine single-source evidence-drift (GSM8K coverage probe
3/47 -> 4/46 via #310/#488), not a non-determinism defect. ADR-0120's fail-closed
property fired as designed; CORE revoked its own expert claim.

History keeps receipts; current-state reconciles to truth:
- Regenerate expert_claims_math_v1_signed.json -> promote_admitted:false,
  reviewer_signature_matches:false, digest 02f6d3c8.
- reviewers.yaml math_expert_claims: quarantine note; entry kept (mismatch-refusal
  keeps firing); intentionally NOT re-signed.
- ADR-0120-math-expert-ledger-flip: dated valid-at/auto-reverted header note.
- README: "next gate" narrative -> built-attempted-reverted; refresh stale count.
- docs/decisions/README: revert note + ADR-0200 index row.
- 3 fail-closed tests (2 files): "is-expert" -> fail-closed-revert assertions.
  Were RED on main; now green (30 passed).

No eval gate, threshold, or safety boundary changed.
2026-06-02 10:06:16 -07:00
Shay
96b6c5e4b2 docs(claims): ADR-0200 + claims ledger — single source of truth (additive)
Add docs/claims_ledger.md (every public claim -> in-repo evidence, with the
four GSM8K numbers separated and labeled) and ADR-0200 recording the
mathematics_logic expert fail-closed revert as designed behavior (proven
single-source evidence-drift; determinism intact).

Additive only: no existing claim, eval gate, or test is touched. The
review-gated reconciliation diffs (reviewers.yaml quarantine note, ADR-0120
header note, signed-JSON regen, README narrative, 3 test reconciliations) are
listed in ADR-0200 section 4 and await operator ratification.
2026-06-02 09:35:44 -07:00
Shay
ab9e1afe04 docs(adr): backfill ADR index — add 0184-0195 + 0197-0199 (12 missing rows)
The decisions README index table stopped at ADR-0183 then jumped to
ADR-0196, omitting every top-level ADR that landed in between plus the
three newest. PRs #513/#514/#515 added ADR-0197/0198/0199 files without
touching the index; the 0184-0195 gap predates them.

Adds 12 rows in numeric order with title + status pulled from each ADR
header. No content/runtime change; pure index backfill.

- files-vs-index drift check: now empty (was 12)
- all 12 new link targets verified to resolve
2026-06-01 12:14:44 -07:00
Shay
1d12c3b01e
docs(adr): ADR-0199 cross-domain learning arena contract (#515) 2026-05-31 20:36:56 -07:00
Shay
918eb5552d
docs(adr): ADR-0198 motor efferent decoder spike (#514) 2026-05-31 20:32:26 -07:00
Shay
81062bb0fb
ADR-0197: vision compiler over Delta-CRDT (docs only) (#513) 2026-05-31 20:32:08 -07:00