orthonym.validation.binding_spine

Note

Internal API. Names and behaviour may change between releases.

a phase: the recursion-safe name<->graph binding spine.

WHY this module exists

pushes best-effort naming breadth far past the general_engine’s

flat, chain-shaped emissions, and that is only safe if an emitted name can be PROVEN to spell exactly the input graph – cheaply, in-process, with no Java. The existing E1 certificate (e1_certificate.py) proves a flat atom->token partition, which is sound only while every token is atomic. It is not: a substituent prefix token like "2-chloroethyl" is a COMPOSITE that spells a sub-name, and under a flat model such a token may legitimately claim a whole subtree – including atoms whose morphemes live in its own inner name. A flat partition therefore cannot distinguish “this token says those atoms” from “this token was handed those atoms”.

The spine closes that hole with one invariant:

EXCLUSIVE CLAIM – a binding’s atom_ids are the atoms that this token itself spells, and never include an atom spelled by one of its children. Nesting in the name is nesting in the spine, so subtree_atoms == atom_ids | union(child.subtree_atoms).

Consequence: a composite token can no longer claim a subgraph it does not say. Every atom in the molecule must be claimed by exactly one binding somewhere in the tree, at the depth whose morpheme actually spells it.

Scope and status (a phase)

AUDIT-ONLY and PURE. This module is wired into no naming path, gates nothing, and changes no emitted name. verify_spine runs proofs P1 (atom partition: exactly-once, no unbound, no phantom), P2 (bond totality: every bond claimed exactly once), P3 (charge totality), P4 (every token anchored to real spans of the FINAL name, with multiplicity), P5 (name morphemes no binding accounts for – the dual of P1’s atom coverage) and P6 (each token’s claimed atom count checked against an INDEPENDENT estimate of what its text spells). Each appends to the SAME findings list, so the proof object grows without changing shape.

P1-P3 all take the producer at its word about WHICH atoms a token covers: they check the claims are mutually consistent and total, never that the token’s TEXT says those atoms. P4 and P6 are the two halves of closing that: P4 proves the token is spelled in the name at all (and the right number of times), P6 proves the number of atoms it claims is the number its morphemes spell. P6 is the falsifier – it is what makes a token unable to claim atoms it does not say.

Atom coverage alone is not structure: a name can spell exactly the right atom set while describing the wrong bonds (propylpropane and cyclohexane claim the same six carbons). P2 is therefore not a refinement of P1 but the other half of it – P1 fixes which atoms the name accounts for, P2 fixes how they are joined.

What P4 cannot decide, and how the residual is surfaced

P4 is a BOUNDARY proof, and no boundary proof can choose between two morpheme partitions of the same string: bu|tane and but|ane cut butane in exactly the same two places, so a rule about what abuts a cut cannot prefer either. The evidence is even mutual – each fabricated half is the other’s “another binding’s token” – and that clause cannot simply be dropped, since it is what anchors the parent in every real methyl|benzene. Tightening P4 here would buy one missed detection at the price of false errors on correct names, which is the wrong trade for a proof that must never be confidently wrong.

The lexicon-level question – “is this string a morpheme at all?” – belongs to P6, whose oracle answers “unconfident” for both halves of bu|tane. So the real residual is not that P4 is wrong but that a spine in which NOTHING is arity-confident has had nothing corroborated by anything independent of the producer, and used to report ok=True while saying so nowhere. PROOF_UNSUBSTANTIATED closes that: stats["arity_confident_atom_frac"] is the share of claimed heavy atoms sitting under an arity-confident token, and the finding is raised when it is 0.0 – not one token independently corroborated. Zero is the defensible line; any threshold above it is a tuning knob no measurement supports yet.

It SUPERSEDES NOTHING yet: e1_certificate.py is untouched and remains the production emission gate for this phase.

Fail-closed discipline

A proof must never be confidently wrong. A finding is an "error" only when the spine and the graph provably disagree; anything the current proofs cannot decide is reported as its own code (*_UNVERIFIED, PROOF_UNSUBSTANTIATED) or not claimed at all – never silently folded into ok. ok means “no error-severity finding was raised by the proofs that actually ran”, so callers that need a stronger guarantee must check which proofs ran (stats["proofs"]) and how much those proofs actually corroborated (stats["arity_confident_atom_frac"]).

verify_spine requires a real RDKit mol; it raises rather than returning a verdict when handed None, because a crash is safe and a fabricated pass is not.

class orthonym.validation.binding_spine.BindingKind(*values)

Bases: str, Enum

What a token contributes to the name.

Values are the lowercase member names so a kind serialises readably into stats and logs. PARENT/SUFFIX/PREFIX are the kinds the legacy flat bindings can express; the rest exist for the later phases (functional replacement, fusion assembly, charge suffixes, added hydrogen) so that spine consumers never need a second vocabulary.

PARENT = 'parent'

SUFFIX = 'suffix'

PREFIX = 'prefix'

REPLACEMENT = 'replacement'

FUSION = 'fusion'

CHARGE = 'charge'

HYDRO = 'hydro'

class orthonym.validation.binding_spine.SpineBinding(token, kind, atom_ids, bond_ids=frozenset({}), charge_atom_ids=frozenset({}), children=(), attachment=None)

Bases: object

One token and the atoms it itself spells.

atom_ids is EXCLUSIVE: atoms spelled by a nested token belong to that child, not here. bond_ids and charge_atom_ids follow the same exclusivity and stay empty until P2/P3 populate them. attachment is an atom OF THIS FRAGMENT – a member of this binding’s own atom_ids – namely the one bonded to the enclosing token. It is NOT the atom on the parent/enclosing side of that bond (None for a parent/root token, which has no enclosing token to attach to).

token: str

kind: BindingKind

atom_ids: frozenset[int]

bond_ids: frozenset[int] = frozenset({})

charge_atom_ids: frozenset[int] = frozenset({})

children: Tuple[SpineBinding, ...] = ()

attachment: int | None = None

subtree_atoms()

Atoms spelled by this token together with its whole subtree.

walk()

Pre-order traversal of this subtree, self first.

class orthonym.validation.binding_spine.BindingSpine(roots, legacy_role_coerced=(), stereo_atom_to_locant=<factory>)

Bases: object

The full name<->graph binding tree for one emission.

legacy_role_coerced carries the raw TokenBinding.role strings that from_token_bindings could not map, so verify_spine can report them in stats instead of the adapter having to log out of band. It defaults to empty for hand-built spines.

stereo_atom_to_locant (a phase Task 3) is the atom->locant map the PARENT-scope stereodescriptor block (if any) was spelled from – the SAME dict general_engine._stereo_prefix was called with, threaded here so P8 can resolve the block to real atom/bond identity. Empty for every result whose producer never called _stereo_prefix (nothing to resolve) and for hand-built spines that do not opt in.

roots: Tuple[SpineBinding, ...]

legacy_role_coerced: Tuple[str, ...] = ()

stereo_atom_to_locant: Dict[int, int]

walk()

Pre-order traversal of every binding in every root.

classmethod from_token_bindings(bindings, stereo_atom_to_locant=None)

Adapt legacy flat ``TokenBinding``s into a (flat) spine.

The legacy producers claim a substituent’s WHOLE branch subtree under a single composed token string, so no nesting can be recovered without re-deriving the sub-name: every adapted binding is therefore a root with children=. That is a faithful widening – the flat spine proves exactly what the flat E1 certificate proved, no more – and it is deliberately NOT an attempt to infer structure the legacy binding never recorded.

a phase Task 2: a role='charge' legacy binding (general_engine.TokenBinding) carries the charged atom indices in its OWN charge_atom_ids field, not in atom_ids – E1 (e1_certificate.verify_certificate) treats every binding’s atom_ids uniformly for its double-bind/phantom checks, so putting the already-parent-owned charged atom there would manufacture a false ATOM_DOUBLE_BOUND. This adapter therefore reads getattr(binding, "charge_atom_ids", ) for every binding (empty for the 12 legacy producers that have no such field/value, so their behaviour is unchanged) and threads it onto SpineBinding, which already has that exact slot.

a phase Task 3: stereo_atom_to_locant is NOT carried per-binding (unlike charge_atom_ids) – general_engine.GeneralEngineResult threads ONE map for the whole result (the map its single _stereo_prefix call used), so the caller passes it here rather than it living on any one TokenBinding. Defaults to empty, which is byte-identical to before this field existed.

class orthonym.validation.binding_spine.Finding(code, detail, severity)

Bases: object

One thing a proof observed. Only "error" blocks ok.

code: str

detail: str

severity: str

class orthonym.validation.binding_spine.SpineProof(ok, findings, stats)

Bases: object

Result of running the proofs that are implemented so far.

stats["proofs"] names them, so a caller can tell “passed every proof there is” from “passed the two that ran”.

ok: bool

findings: Tuple[Finding, ...]

stats: Dict[str, Any]

codes()

Finding codes in the order they were raised.

orthonym.validation.binding_spine.verify_spine(mol, spine, name, *, mode='audit', allow_charged=False, escalate=frozenset({}))

Prove that spine binds name to exactly the graph of mol.

Runs P1 (atom partition), P2 (bond totality), P3 (charge totality), P4 (token spans on name), P5 (name residue) and P6 (token arity). name must be the FINAL post-processed string, since that is what P4 and P5 read. mode selects P2’s linkage policy and the severity of the three unproven-not-disproven codes (CHARGE_UNVERIFIED, UNBOUND_MORPHEME, PROOF_UNSUBSTANTIATED): "audit" infers a unique undeclared cross-subtree bond as an attachment (what today’s producers actually emit) and warns on the unproven, "strict" requires every bond to be declared or internal and leaves nothing unproven.

escalate (a phase Task 4) force-promotes any listed finding CODE from "warn" to "error" after every proof has run, independent of mode – the mechanism the wiring uses to enforce JUST the P8 stereo axis and P3’s CHARGE_UNVERIFIED (STRICT_STEREO_CHARGE_AXES) without also flipping P2’s bond-linkage inference policy or P5/P6’s unrelated unproven-codes, which a blanket mode="strict" would do too. Never touches "info"-severity findings (SUBSTITUENT_STEREO_UNVERIFIED is never in STRICT_STEREO_CHARGE_AXES for exactly this reason).

stats["proofs"] lists the proofs that actually ran, so ok is never mistaken for a stronger guarantee than was computed. A failed P1 drops both P2 (bond ownership becomes undecidable) and P5 (a token set that does not partition the graph makes the span map unreliable, so uncovered text says nothing). P4 and P6 read only the name and the tokens, so they still run – and are often exactly what explains the P1 failure.