# Simplex schema: a semantic relation joining roles

Here **simplex** means the owner's multi-role relation pattern: one statement relates
objects, assumptions and a conclusion. The implementation does not construct geometric
simplices, faces, boundaries or a mathematical simplicial complex.

## The model

| Concept | Representation | Meaning |
|---|---|---|
| Reusable role definition | `Role` | A semantic slot type with optional textual type/context and finite `choices` |
| Statement/relation pattern | `Simplex` | A named mapping from at least two local aliases to roles |
| Object or assumption supplied by a caller | `Fact` | A role plus a non-None value |
| Requested result | `Goal` | A role whose value is not supplied yet |
| Application to particular objects | `SimplexInstance` | Facts and goals bound by local slot alias |
| Explicit composition | A `Simplex` used as a role | A supplied nested pattern; no proof dependency is discovered automatically |
| Persistent catalog | `SchemaRegistry` | JSON/SQLite nodes and alias-to-definition references |

`kind` separates `object`, `fact`, `goal`, `own` and nested `simplex` roles.
A role's `attrs.references` may name other aliases in the same simplex; unknown aliases
are rejected. These references can describe the objects mentioned in an assumption or
conclusion. They are not geometric edges. Their provenance must distinguish manually
supplied relationships from incomplete syntactic candidates.

`type_text` is descriptive Lean/mathematical text, not an executable type checker.
`choices` is a finite set of admissible values, not a replacement for arbitrary Lean typeclass
constraints. Supplied fact and resolved goal values are checked against explicit choices.
No registry method establishes that a string is a proof or that a mathematical premise is true.

## Concrete example: two groups and a homomorphism

One schema joins these slots:

| Local alias | Role | Type/claim | References |
|---|---|---|---|
| `left` | object | group carrier | none |
| `right` | object | group carrier | none |
| `map` | object | `left →* right` | left, right |
| `bijective` | fact | `Bijective map` | map |
| `goal` | goal | `Nonempty (left ≃* right)` | left, right |

The simplex is this complete relation pattern, not an individual role or an asserted
geometric object. `left` and `right` may explicitly reuse the same `role:group` definition
while binding to different group objects. Reusing a role definition does not equate their values.

Run the synthetic, offline example:

```sh
PYTHONPATH=. python3 examples/simplex_registry.py
```

It binds symbolic caller values for the input slots, leaves the goal unresolved, and returns
a structurally ready candidate. It does not run a Lean proof.

## Scope, persistence and reuse

`SchemaRegistry.set_simplex` assigns every child a scoped key by default:
`<schema-key>/slot/<escaped-alias>`. Thus `G` in one theorem is not the same object as `G`
in another. Corpus keys also include the frozen annotation hash and item identity.

To reuse a definition, register it with `set_role` and explicitly pass a `role_keys` mapping
to `set_simplex`. The referenced definition must match the supplied role exactly. A shared
definition still has distinct occurrence keys for every alias. No role is semantically merged
merely because its spelling, type text or keywords resemble another role.

Keys are immutable within a registry. Identical registration is idempotent; changed content
or changed definition references require a new version key. `get_role` and `get_simplex`
resolve exact keys, not ambiguous bare names. `search_roles` returns literal-substring candidates
for a caller to review; it does not approve semantic reuse.

Serialization includes names, kinds, context, types, choices, attributes and nested aliases.
`role_from_dict` restores JSON snapshots. SQLite uses one connection and one transaction per
nested registration, foreign keys and JSON payloads; it does not load archived pickle blobs.
Cyclic nesting and failed reuse checks roll back the complete write. Returned objects are
restored snapshots; changing one does not silently update a registered definition.

## Query and binding APIs

```python
from leanbench.schema_registry import SchemaRegistry, slot_key

with SchemaRegistry("private-registry.sqlite") as registry:
    schema = registry.get_simplex("schema:example")
    matches = registry.search_roles("group")
    containers = registry.find_by_roles(["role:group"], match_all=True)
    candidates = registry.find_solvable([
        slot_key("schema:example", "left"),
        slot_key("schema:example", "right"),
        slot_key("schema:example", "map"),
        slot_key("schema:example", "bijective"),
    ])
```

`find_by_roles` searches definition references, including descendants of nested schemas.
`find_solvable` retains the archived API name but implements **structural readiness only**:
all input occurrences must be supplied and at least one marked goal/own occurrence must
remain unresolved. It returns `structural_candidate_only: true`, not a proof or a computed value.
Having one `role:group` definition cannot satisfy two distinct group slots. A nested input
must itself be explicitly supplied; the registry does not apply its internal theorem automatically.

`SimplexInstance(schema, facts=..., goals=...)` binds local aliases. Facts and goals must be
distinct declared slots. Omitting `goals` uses roles marked `goal` or `own`; `resolve` checks
a supplied goal value against choices. Completion means that declared goals have values,
not that Lean verified them. Value unification, dependent type checking and proof search
remain outside this implementation.

## Materialization of the 65 P0 items

The builder consumes the frozen current-chat GPT diagnostic's source descriptions and
unchanged Lean strings. It makes no model request, revises no assessment and performs no
Lean compilation. Results:

| Artifact | Count |
|---|---:|
| Source annotation seed schemas | 65 |
| Lean signature schema seeds | 50 |
| Items with fewer than two projected Lean roles | 15 |
| Stored schemas | 115 |
| Scoped role records / slot occurrences | 483 / 483 |

These 115 seeds deliberately do not auto-reuse definitions across statements. Explicit reuse
is supported and tested by the synthetic example; a reviewed shared ontology is future work.
The 15 incomplete Lean sides remain in the index with status `insufficient_projected_roles`.
A closed declaration may mention concrete objects inside its conclusion that the binder-based
projector misses. No object roles were invented to hide this limitation.

Source schemas are marked `unreviewed_annotation_seed`. Existing `given` tags are preserved
with `quantifier_status: unreviewed`; they are not silently converted to universal/existential
quantifiers. References on the source side use explicit symbol candidates; Lean references
are syntactic identifier candidates. Neither is a complete dependency analysis.
For example, P11's source seed lists a named size while Lean uses `Fintype.card G` inline.
The materializer preserves both representations; it does not invent a validated cardinality
binding or repair the old alignment result. Annotation quality and semantic normalization
still require a separate review.

Private outputs under `experiments/P0-pilot/data/simplex-schemas-v1/`:

- `registry.sqlite`: queryable catalog with the 115 schemas and scoped slots.
- `schemas.json`: all 65 source/Lean pairs, retaining incomplete Lean projections.
- `schemas.html`: a local generated copy of the schema-only review tracked below.
- `schema-inputs.json`: input hashes; an existing directory rejects changed inputs.

Tracked outputs:

- `experiments/P0-pilot/results/simplex-schema-index.json`: 65 item IDs, schema keys,
  role counts, coverage status and reference-candidate counts.
- `experiments/P0-pilot/results/simplex-schema-summary.json`: coverage, limitations and hashes.
- [65-item schema review](reviews/simplex-schemas.html): an owner-approved, self-contained
  HTML view of all 65 source/Lean pairs. It includes schema role descriptions and Lean
  signature expressions, but no textbook paragraphs or full assistant judgment explanations.
  Open the file in a browser after cloning, or download it from the repository; the Git web
  interface may display HTML source instead of rendering it. The JSON indexes above remain
  text-free counts/keys. Full source-inclusive inputs and assessment files remain gitignored.

Replay from the repository root with private inputs present:

```sh
PYTHONPATH=. python3 experiments/P0-pilot/build_schemas.py \
  --items experiments/P0-pilot/data/simplex-schemas-v1/items.jsonl \
  --assessments experiments/P0-pilot/data/simplex-schemas-v1/assistant-assessments.json \
  --key experiments/P0-pilot/labels/key.json \
  --private-out experiments/P0-pilot/data/simplex-schemas-v1 \
  --index experiments/P0-pilot/results/simplex-schema-index.json \
  --summary experiments/P0-pilot/results/simplex-schema-summary.json \
  --review-page docs/reviews/simplex-schemas.html
```

The original annotations, judgments, Qwen results and matcher thresholds remain unchanged.
The registry is a usable schema foundation, not evidence of a validated theorem, a working
prover, independently measured faithfulness, or a completed Phase 1 experiment.