Make every conjunct say whose requests it narrows - #613
Open
xmap wants to merge 1 commit into
Open
Conversation
Kind-blindness pins the door: no gate branches on whether a principal is a machine. It says nothing about the envelope, and the two do not imply each other. A gate that never reads a kind can still bind agents on eight axes and humans on two, because the narrowing arrives through the instrument a principal holds rather than through a branch on what they are. Every step of that drift is legal under the existing test, individually documented, and the endpoint is a system whose symmetry describes a doorway and nothing else. That endpoint is the current trajectory, not a hypothetical: the mandate design carries eight axes and the human envelope binds two. So an axis may be bound only from an instrument the facility actually issues. Where a conjunct binds some principals and not others, the gap is not an oversight to disclose after the fact; it is an entry that must name the gesture the facility does not perform, and the trigger that would retire it. `_REACH_LEDGER` classifies every `Conjunct` member, asserted against the enum in both directions so a new conjunct fails as unclassified and a removed one fails as stale. `_CARVE_OUT_LEDGER` holds the exceptions, and a `_CarveOut` cannot be written without saying which principals the conjunct narrows, why that is acceptable meanwhile, which facility gesture is absent for everyone else, and what would end the entry. A blank field fails. The load-bearing field is `missing_gesture`, because it separates an asymmetry the world imposes from one CORA invented. An asymmetry with no nameable missing gesture is usually a conjunct keyed on the principal that should have been keyed on the request, and that reframing is cheaper before the conjunct ships. Both ledgers are as small as they can be: one classification, no carve-outs, and every test passes trivially. That is the point, and it is the reason `Conjunct` itself shipped with one member: answering "whose requests does this narrow" costs nothing while writing a conjunct and nearly everything once twenty exist. A ledger written afterwards is an audit, and this repo already learned what audits are worth. Unlike the kind-blindness sweep, this records a declaration rather than a discovery, since no syntax reveals which principals a conjunct narrows. So the one live classification is backed structurally instead of by its author's word: Policy can narrow every principal alike only while it holds nothing to tell them apart by, and a kind-shaped field on it now fails rather than silently falsifying the entry. Naming follows the sibling rather than inventing a parallel vocabulary. The record is a carve-out because that is what the sibling calls the same job and what conventions.md already uses; `_Justification` is refused because cora.shared.justification owns that noun for the obligation gate, which calls itself the deontic dual of authorization, so the overload would land where it is most expensive. `_PrincipalReach` is quantified rather than kind-named on purpose: a real carve-out could key on service accounts or on key-backed identity, and naming the axis by actor kind would pre-commit the ledger to a two-kind world while reintroducing `kind` into a module whose sibling makes kind structurally unreachable at the port. Verified: architecture 30,195 passed / 620 skipped; pyright src tests 0 errors; ruff clean. Each of the six tests was mutated into its failure mode and confirmed to go red, since an empty ledger would otherwise pass a test with no teeth. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Why
test_actor_kind_blindness.pypins the door: no gate branches on whether a principal is a machine. It says nothing about the envelope, and the two do not imply each other.A gate that never reads a kind can still bind agents on eight axes and humans on two, because the narrowing arrives through the instrument a principal holds rather than through a branch on what they are. Every step of that drift is legal under the existing test and individually documented, and the endpoint is a system whose symmetry describes a doorway and nothing else.
That endpoint is the current trajectory, not a hypothetical: the mandate design carries eight axes and the human envelope binds two.
The rule
An axis may be bound only from an instrument the facility actually issues. Where a conjunct binds some principals and not others, the gap is not an oversight to disclose after the fact; it is an entry that must name the gesture the facility does not perform, and the trigger that would retire it.
_REACH_LEDGERclassifies everyConjunctmember, asserted against the enum in both directions, so a new conjunct fails as unclassified and a removed one fails as stale._CARVE_OUT_LEDGERholds the exceptions. A_CarveOutcannot be written without saying which principals the conjunct narrows, why that is acceptable meanwhile, which facility gesture is absent for everyone else, and what would end the entry. A blank field fails.The load-bearing field is
missing_gesture, because it separates an asymmetry the world imposes from one CORA invented. An asymmetry with no nameable missing gesture is usually a conjunct keyed on the principal that should have been keyed on the request, and that reframing is cheaper before the conjunct ships.Why ship it empty
Both ledgers are as small as they can be: one classification, no carve-outs, and every test passes trivially. That is the point, and it is the reason
Conjunctitself shipped with one member. Answering "whose requests does this narrow" costs nothing while writing a conjunct and nearly everything once twenty exist. A ledger written afterwards is an audit.One structural backing
Unlike the kind-blindness sweep, this records a declaration rather than a discovery, since no syntax reveals which principals a conjunct narrows. So the one live classification does not rest on its author's word:
Policycan narrow every principal alike only while it holds nothing to tell them apart by, and a kind-shaped field on it now fails rather than silently falsifying the entry.Verification
uv run pyright src tests0 errors, ruff clean🤖 Generated with Claude Code