core-labs/core
core-labs/core
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

feat(deduction-serve): Band v3-MEM — member-chain band, Socrates syllogism decided (ADR-0258) #108

Merged
core-labs merged 1 commit from feat/member-chain-band into main 2026-07-24 02:36:04 +00:00
Conversation 0 Commits 1 Files changed 19 +1421 -42
core-labs commented 2026-07-24 02:35:43 +00:00
Owner
Copy link

What CORE can do now that it couldn't this morning

The classic instantiation syllogism — reserved as ADR-0257 §6.1's scope-out
when the English band merged as #107 — is decided end-to-end through the real
core chat spine, rendered over the user's own sentences:

Socrates is a man. All men are mortal. Therefore Socrates is mortal.
→ Given: socrates is a man; all men are mortal. Your premises entail: socrates is mortal.

Tweety is a canary. All canaries are birds. No birds are reptiles. Therefore Tweety is not a reptile.
→ …Your premises entail: tweety is not a reptile.

Socrates is mortal. All men are mortal. Therefore Socrates is a man.
→ …Reading each name as one individual and each class word at face value, your
premises don't settle whether socrates is a man — it holds in some cases and fails in others.

ds-en-0022, pinned declined in the v2_en lane purely for want of a reading
band, is promoted to entailed — this band's designed acceptance case.

Mechanism

One new module, generate/proof_chain/member.py: a closed sentence grammar
(singular <NAME> is [not] [a|an] <CLASS> facts; all/every/each and no
universals) plus per-individual propositional lowering — one opaque minted
atom per (individual, class) pair, every universal instantiated at every named
individual, decided by the same verified ROBDD engine. No new decision
procedure; only the lowering is new (same discipline as the v1b categorical
decider).

Composer tier strictly after v1 → v1b → v2-EN: monotone widening, so every
previously-served argument is served byte-identically (v1 lane 28/28 unchanged).

Why it's sound

Universal instantiation at named individuals is truth-preserving in every
first-order model, so ENTAILED / REFUTED / inconsistent verdicts hold in every
model of the original argument — served at full strength. They even survive
co-reference of two distinct names, since that only adds premises and
entailment is monotone.

For this closed fragment (singular literals + A/E universals, singular
conclusion, Boolean reading) the lowering is also complete: a propositional
countermodel lifts to a first-order countermodel whose domain is exactly the
named individuals. UNKNOWN is therefore genuinely "not forced," never an
artifact of instantiating too little — and its surface still scopes itself to
the disclosed reading.

Number linking is the one semantic identification the band performs ("all
men" must bind "a man"): two attested class forms identify iff related
token-wise by a closed relation — an irregular/invariant table consulted first
(table membership makes it the sole authority for that token, which is what
keeps specie/species and new/news unlinked), then three regular suffix
rules. Under-linking costs coverage; it can never cost soundness. This is
CORE's first morphology table, flagged in ADR-0258 §5 as the artifact class that
moves into a ratified pack when the grc/he sibling bands land.

Refusal-first throughout: existential quantifiers and quantifier pronouns, bare
plurals ("Dogs are loyal"), definite descriptions, relative clauses, tense,
mixed connectives, and universal conclusions all refuse with typed reasons.

Earned, not flagged

Four new shape-bands (en_member_single / _chain / _negative / _atomic),
each earning its own SERVE license through the ADR-0199 arena:
13 bands × 720 = 9,360 cases, wrong=0, reliability 0.99087 ≥ θ_SERVE=0.99.
Ledger re-sealed at 13 bands. Arena gold is by-construction and cross-checked
against the truth-table oracle over each template's intended instantiated
formulas — no reader in the loop (INV-25). The synthetic class lexicon
deliberately exercises every row-type of the number table, so the license
certifies the linking relation, not just the sentence grammar.

New hand-authored real-English lane evals/deduction_serve/v2_member/ (26
cases, content-disjoint from the synthetic lexicon) keeps that honest.

Scope-outs (deliberate, ADR-0258 §6)

Conditional–membership fusion ("If Socrates is a man then…"), existential
premises, tense and verb predicates ("Socrates runs"), identity/co-reference.
Each refuses typed today; refusal telemetry marks which band pays next.
deduction_serving_enabled stays default-off — no flag change in this PR.

Files

generate/proof_chain/member.py (new), shape.py (+4 bands),
render.py (+render_entailment_member), chat/deduction_surface.py (tier),
evals/deduction_serve/practice/gold.py (+4 template families, solver
fallback), v2_member/cases.jsonl (new), runner.py (+split, +fallback),
v2_en/cases.jsonl (ds-en-0022 promoted), contract.md (refreshed to the
4-band cascade — it was two arcs stale), report.json + verify_lane_shas.py
(re-pinned), core/cli_test.py, tests/test_member_argument_reader.py (new,
41 tests), plus surface/lane/e2e test updates.
Records: docs/adr/ADR-0258-member-chain-band.md,
docs/research/member-chain-band-2026-07-23.md.

[Verification]: deductive 127 passed / smoke 180 passed / warmed_session 10
passed; arena all_bands_serve_licensed=True wrong_is_zero=True (13 bands);
lanes v1 28/28, v2_en 26/26, v2_member 26/26.

## What CORE can do now that it couldn't this morning The classic instantiation syllogism — reserved as ADR-0257 §6.1's scope-out when the English band merged as #107 — is decided end-to-end through the real `core chat` spine, rendered over the user's own sentences: > **Socrates is a man. All men are mortal. Therefore Socrates is mortal.** > → Given: socrates is a man; all men are mortal. Your premises entail: socrates is mortal. > **Tweety is a canary. All canaries are birds. No birds are reptiles. Therefore Tweety is not a reptile.** > → …Your premises entail: tweety is not a reptile. > **Socrates is mortal. All men are mortal. Therefore Socrates is a man.** > → …Reading each name as one individual and each class word at face value, your > premises don't settle whether socrates is a man — it holds in some cases and fails in others. `ds-en-0022`, pinned `declined` in the v2_en lane purely for want of a reading band, is promoted to `entailed` — this band's designed acceptance case. ## Mechanism One new module, `generate/proof_chain/member.py`: a closed sentence grammar (singular `<NAME> is [not] [a|an] <CLASS>` facts; `all`/`every`/`each` and `no` universals) plus **per-individual propositional lowering** — one opaque minted atom per *(individual, class)* pair, every universal instantiated at every named individual, decided by the same verified ROBDD engine. No new decision procedure; only the lowering is new (same discipline as the v1b categorical decider). Composer tier strictly after v1 → v1b → v2-EN: monotone widening, so every previously-served argument is served byte-identically (v1 lane 28/28 unchanged). ## Why it's sound Universal instantiation at named individuals is truth-preserving in every first-order model, so ENTAILED / REFUTED / inconsistent verdicts hold in every model of the original argument — served at full strength. They even survive co-reference of two distinct names, since that only *adds* premises and entailment is monotone. For this closed fragment (singular literals + A/E universals, singular conclusion, Boolean reading) the lowering is also **complete**: a propositional countermodel lifts to a first-order countermodel whose domain is exactly the named individuals. UNKNOWN is therefore genuinely "not forced," never an artifact of instantiating too little — and its surface still scopes itself to the disclosed reading. **Number linking** is the one semantic identification the band performs ("all men" must bind "a man"): two *attested* class forms identify iff related token-wise by a closed relation — an irregular/invariant table consulted first (table membership makes it the sole authority for that token, which is what keeps `specie`/`species` and `new`/`news` unlinked), then three regular suffix rules. Under-linking costs coverage; it can never cost soundness. This is CORE's first morphology table, flagged in ADR-0258 §5 as the artifact class that moves into a ratified pack when the grc/he sibling bands land. Refusal-first throughout: existential quantifiers and quantifier pronouns, bare plurals ("Dogs are loyal"), definite descriptions, relative clauses, tense, mixed connectives, and universal conclusions all refuse with typed reasons. ## Earned, not flagged Four new shape-bands (`en_member_single` / `_chain` / `_negative` / `_atomic`), each earning its own SERVE license through the ADR-0199 arena: **13 bands × 720 = 9,360 cases, wrong=0**, reliability 0.99087 ≥ θ_SERVE=0.99. Ledger re-sealed at 13 bands. Arena gold is by-construction and cross-checked against the truth-table oracle over each template's *intended* instantiated formulas — no reader in the loop (INV-25). The synthetic class lexicon deliberately exercises every row-type of the number table, so the license certifies the linking relation, not just the sentence grammar. New hand-authored real-English lane `evals/deduction_serve/v2_member/` (26 cases, content-disjoint from the synthetic lexicon) keeps that honest. ## Scope-outs (deliberate, ADR-0258 §6) Conditional–membership fusion ("If Socrates is a man then…"), existential premises, tense and verb predicates ("Socrates runs"), identity/co-reference. Each refuses typed today; refusal telemetry marks which band pays next. `deduction_serving_enabled` stays default-off — no flag change in this PR. ## Files `generate/proof_chain/member.py` (new), `shape.py` (+4 bands), `render.py` (+`render_entailment_member`), `chat/deduction_surface.py` (tier), `evals/deduction_serve/practice/gold.py` (+4 template families, solver fallback), `v2_member/cases.jsonl` (new), `runner.py` (+split, +fallback), `v2_en/cases.jsonl` (ds-en-0022 promoted), `contract.md` (refreshed to the 4-band cascade — it was two arcs stale), `report.json` + `verify_lane_shas.py` (re-pinned), `core/cli_test.py`, `tests/test_member_argument_reader.py` (new, 41 tests), plus surface/lane/e2e test updates. Records: `docs/adr/ADR-0258-member-chain-band.md`, `docs/research/member-chain-band-2026-07-23.md`. [Verification]: deductive 127 passed / smoke 180 passed / warmed_session 10 passed; arena `all_bands_serve_licensed=True wrong_is_zero=True` (13 bands); lanes v1 28/28, v2_en 26/26, v2_member 26/26.
core-labs added 1 commit 2026-07-24 02:35:45 +00:00 
Per-individual propositional lowering over minted (individual, class)
atoms: singular membership/predicate facts + all/every/each/no universals,
instantiated at every named individual, decided by the same verified ROBDD
engine. Closed-table number linking (irregular/invariant priority + three
regular suffix rules) is the one semantic identification — attested-pair
linking only, under-link over over-link. Composer tier strictly after
v1/v1b/v2-EN: monotone widening, v1 lane byte-identical.

- 4 new shape-bands (en_member_single/chain/negative/atomic) each earned
  SERVE at the arena: 13 bands x 720 = 9,360 wrong=0; ledger re-sealed.
- New hand-authored lane evals/deduction_serve/v2_member (26/26); ds-en-0022
  promoted declined->entailed (the designed acceptance case); report
  re-pinned; contract.md refreshed to the 4-band cascade.
- Typed refusals: quantifier pronouns, bare plurals, definite descriptions,
  relative clauses, tense, mixed connectives, universal conclusions.
- Flag posture unchanged (deduction_serving_enabled default off).

[Verification]: deductive 127 / smoke 180 / warmed_session 10; arena
all_bands_serve_licensed wrong_is_zero; lanes v1 28/28, v2_en 26/26,
v2_member 26/26.
core-labs merged commit dd2245a722 into main 2026-07-24 02:36:04 +00:00
core-labs deleted branch feat/member-chain-band 2026-07-24 02:36:05 +00:00
Sign in to join this conversation.
Reviewers
No reviewers
Labels
Clear labels
No items
No labels
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference: core-labs/core#108
No description provided.
Delete branch "feat/member-chain-band"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?