veraxis-protocol · inventor1975 · Sep 7, 2026 · Sep 7, 2026
@@ -1,5 +1,49 @@
 # Open Institutional Compiler
 
+> ## OIC↔ZTL boundary — 2026-09-07
+>
+> Gate G promotion is recorded in the Status line below and in `STATUS.md`. This block adds
+> what those do not say: **where the boundary with ZTL is, and why nothing crosses it yet.**
+>
+> The state has **two matured sides and one missing centre**, all three true at once.
+>
+> **Side one — the OIC admission plane is materially implemented.** Present on `main`:
+>
+> - **bounded candidate admission** — a frozen admission runtime with fifteen terminal states
+>   and recomputable receipts;
+> - **provisional interpretation** — model-proposed semantic structure, explicitly marked
+>   provisional and untrusted.
+>
+> **Side two — ZTL reasoning and warrant semantics have materially matured**, well beyond the
+> July dossier in `adapters/ztl/`. See [`adapters/ztl/CURRENT-STATE-001.md`](adapters/ztl/CURRENT-STATE-001.md).
+> This is a statement about the dependency's own maturity, not a claim that OIC uses it.
+>
+> **The missing centre.** Between those two sides, three institutional transitions do not
+> exist:
+>
+>     institutional semantic admission
+>       → stable admitted proposition
+>         → evidence-bearing formalization
+>
+> What remains blocked, and is *not* made less blocked by either side maturing:
+>
+> - **semantic implementation has not started.** The semantic code-start gate is
+>   `READY FOR SEPARATE EXACT-HEAD REVIEW / NOT OPEN` — see
+>   [`docs/gates/OIC-SEMANTIC-CODE-START-GATE-CLOSURE-v0.1.md`](docs/gates/OIC-SEMANTIC-CODE-START-GATE-CLOSURE-v0.1.md).
+> - **ZTL runtime attachment is blocked.** No institutional act converts a reviewed
+>   interpretation proposal into admitted canonical meaning, and no canonical formal object
+>   exists for a logic kernel to receive. The pipeline ends at a provisional proposal.
+>
+> The boundary itself is described in
+> [`docs/architecture/OIC-ZTL-MATURATION-DELTA-001.md`](docs/architecture/OIC-ZTL-MATURATION-DELTA-001.md)
+> and [`docs/architecture/OIC-ZTL-LAYER-OWNERSHIP-001.md`](docs/architecture/OIC-ZTL-LAYER-OWNERSHIP-001.md);
+> the falsifiability hierarchy in
+> [`docs/darpa/OIC-ZTL-DARPA-CROSSWALK-001.md`](docs/darpa/OIC-ZTL-DARPA-CROSSWALK-001.md).
+>
+> Nothing in this block establishes semantic correctness, runtime authorization,
+> institutional validity, or independent reproduction. `tier_1_reproduction` remains
+> **NOT ESTABLISHED**.
+
 - **Status:** BOUNDED_REFERENCE_IMPLEMENTATION — scoped independent Gate G validation passed for candidate `a2b5053771ce510fb35ce09f3e99f545c21ac20e` and merged to `main` as `c4a325c551ce8904dfcc5b9fe81b05109726a334`
 - **Bootstrap date:** 2026-07-29
 - **Governing design:** TDD-OIC-001 v1.1

@@ -1,5 +1,34 @@
 # Project Status
 
+## OIC↔ZTL boundary — 2026-09-07
+
+Gate G promotion is recorded in the section below. This block adds what it does not say:
+**where the boundary with ZTL is, and why nothing crosses it yet.**
+
+On `main` today: **bounded candidate admission** and **provisional interpretation** are
+present. Separately, **ZTL reasoning and warrant semantics have materially matured** well
+beyond the July dossier in `adapters/ztl/` — a statement about the dependency, not a claim
+that OIC uses it.
+
+Between those two matured sides, three institutional transitions **do not exist**:
+
+    institutional semantic admission
+      → stable admitted proposition
+        → evidence-bearing formalization
+
+Therefore: semantic implementation has not started, the broader production semantic gate
+remains **BLOCKED**, and **ZTL runtime attachment remains BLOCKED** — the institutional
+semantic act that would produce an admitted canonical proposition does not exist, so there is
+no lawful input for a logic kernel. Neither side maturing makes that blockage smaller.
+
+The boundary is described in `docs/architecture/OIC-ZTL-MATURATION-DELTA-001.md` and
+`docs/architecture/OIC-ZTL-LAYER-OWNERSHIP-001.md`; the current dependency state in
+`adapters/ztl/CURRENT-STATE-001.md`; the falsifiability hierarchy in
+`docs/darpa/OIC-ZTL-DARPA-CROSSWALK-001.md`.
+
+No semantic correctness, runtime authorization, institutional validity, or independent
+reproduction is established by this block. `tier_1_reproduction` remains **NOT ESTABLISHED**.
+
 ## Current status
 
 **BOUNDED_REFERENCE_IMPLEMENTATION — SCOPED INDEPENDENT GATE G VALIDATION PASSED AND MERGED TO MAIN**

@@ -0,0 +1,100 @@
+# ZTL current state — 001
+
+**Date:** 2026-09-07. This file records what ZTL is **now**, beside the v0.1/v0.2 dossier and
+conformance material in this directory, which describe a July state and are retained unchanged.
+
+**Reading discipline.** A module's existence and theorem count is **not** a reading of its
+statements. Below, *read* means the source was opened in the pass that produced this file;
+*counted* means only the census figure is asserted. Nothing here upgrades a claim on the
+strength of a file name.
+
+## Pin
+
+| | |
+|---|---|
+| repository | `https://github.com/inventor1975/ZTL` |
+| branch | `master` |
+| HEAD | `8ab40b23546eb9fd5a4fd8cc22e94282ce2a7a44` |
+| tree | `0efbd9cb6852a214bc653477454639a5f378a1ce` |
+
+The **frozen kernel profile pins a different, older commit** — `56e1ff05`, July — and that is
+correct and deliberate: this file is not a re-pin. See
+`docs/architecture/OIC-ZTL-MATURATION-DELTA-001.md` §5.
+
+## Census — measured 2026-09-07
+
+ZTL's own inventory tooling reports, verbatim:
+
+    ALL CLEAN: 1112 theorems across 66 modules, every one on the empty axiom list.
+
+**Anticipating the arithmetic.** A plain count over the sources disagrees — 67 `.lean` files and
+1118 `theorem`/`lemma` line-starts. Both differences are explained and neither is an exclusion:
+
+- **67 vs 66 modules:** one file contains zero theorem or lemma declarations; it is an
+  evaluation script, contributing a file and no theorem.
+- **1118 vs 1112 declarations:** the six extras are English prose **inside block comments**
+  that happen to begin with the word *theorem* or *lemma*. The inventory tool skips block
+  comments deliberately; its own source records that exact bug being caught earlier, with one
+  of these six lines as the example.
+
+Separately and unrelatedly, classical proofs of the `F:∀` rule **are** held outside the
+theorem corpus, in a probes directory that is not part of the module set. That is a real
+exclusion — but those files were never inside the counted scope, so they explain none of the
+six. The two facts are both true and neither explains the other.
+
+**The figure to use is 1112 / 66.**
+
+## Modules the current interface work depends on
+
+| module | theorems | this pass |
+|---|---|---|
+| `ZCutElim` | 103 | counted |
+| `ZProv` | 35 | counted |
+| `ZNaN` | 25 | counted |
+| `Linear` | 22 | counted |
+| `RelianceBridge` | 19 | counted |
+| `LabelExactDefinite` | 19 | counted |
+| `LabelExact` | 17 | counted |
+| `ZHeredTaut` | 17 | counted |
+| `ContextClosure` | 12 | counted |
+| `ZReceiptHard` | 12 | counted |
+| `ZReconverge` | 11 | **read** |
+| `ZWidthHard` | 10 | counted |
+| `NoGift` | 10 | counted |
+| `Receipt` | 4 | counted |
+
+Every module in the census is on the empty axiom list; that part is measured for all of them.
+
+## The one result read in full, because this repository's architecture depends on it
+
+`ZReconverge` — 11 theorems, empty axiom list:
+
+    eligible m (Γ₁ ++ Γ₂) = true  ↔  eligible m Γ₁ = true ∧ eligible m Γ₂ = true
+
+An **equivalence**, holding **without** non-emptiness hypotheses, *whatever the two branches
+share and however many times they share it*. The question is settled by a theorem over every
+marking and every pair of bundles — not by a failed search.
+
+Where sharing does bite: **below eligibility, in the verdict.** One unresolved ground read once
+yields `Z`; read twice it yields `F`. In that witness eligibility is `false` in **both** cases,
+and more generally an unresolved ground makes every branch reading it ineligible **before** any
+recombination. The one way such a ground enters an eligible branch is the over-grant `¬¬p`, and
+there recombination is neutral.
+
+Supporting measurement, 2026-09-07: 135 225 enumerated cells — verdict ≠ meet with both bundles
+non-empty **0**, on the empty-bundle edge **12**, eligibility ≠ conjunction **0**, cells where
+both branches are eligible **14 387** (the denominator; the check is not vacuous). A second
+sweep of 3000 random pairs: 27 000 cells, edge 45, eligibility mismatches **0**.
+
+**Consequences for this repository.** Do not write *"shared ancestor = unsafe"* or *"shared
+ancestor = loss of standing"*; both are refuted. Keep **eligibility**, **verdict**, **ground
+identity**, **use multiplicity** and **path multiplicity** as separate questions — ground
+identity in particular is *not* settled by this module. And note that the meet identity on the
+verdict does carry non-emptiness hypotheses: an empty bundle is not the identity element of
+that operation. No dependency-graph representation is proposed here.
+
+## What this file does not do
+
+It does not re-pin the kernel profile, does not update the dossier, does not claim
+conformance against the current head, and does not establish Tier-1 reproduction — which
+remains **NOT ESTABLISHED**.
diff --git a/docs/architecture/OIC-ZTL-LAYER-OWNERSHIP-001.md b/docs/architecture/OIC-ZTL-LAYER-OWNERSHIP-001.md
@@ -0,0 +1,74 @@
+# OIC↔ZTL Layer Ownership 001
+
+**Date:** 2026-09-07 · **Base:** `main` at `c4a325c5`, tree `b8e31ec4` · **Status:** architecture
+description, not a decision record. It describes ownership as it stands; it creates no
+authority and admits nothing.
+
+This document answers one question for each semantic act in the pipeline: **which layer owns
+it, and what artifact in this repository shows that.** Two rows have no owner. Naming them is
+the point of the document.
+
+## 1. Ownership of each semantic act
+
+| Question | Owning layer | Where it lives here |
+|---|---|---|
+| What source bytes existed? | OIC | `source_id` / `source_version` / `source_digest` on every admission receipt; `schemas/draft/source-document.schema.json`, `source-node`, `source-anchor` |
+| What candidate spans were proposed? | OIC extraction | `src/oic/candidate_extraction.py`; `schemas/draft/candidate-normative-unit.schema.json` |
+| Are **candidate** proposals divergent? | OIC review docket | `src/oic/review_docket.py` — `AgreementState` ∈ {`NO_CANDIDATES`, `IDENTICAL`, `DIVERGENT`} |
+| Is institutional authority evidence sufficient? | OIC admission | `src/oic/admission.py`; `design/admission-boundary-001/ADMISSION-CONTRACT-v0.1.md` |
+| **What meaning was institutionally admitted?** | — **no owner** | assigned in prose to a *"Future Institutional IR construction stage"*; no code, no receipt, no state |
+| **What formal proposition represents that admitted meaning?** | — **no owner** | ADR-002 names Institutional IR as the canonical admitted representation; `schemas/draft/institutional-ir.schema.json` types `nodes` as `{"type":"object"}` and carries no formula |
+| What grounds are verified / unverified? | supplied evidence state | `docs/contracts/kernel-profiles/ztl-v0.1.json` → `unverified_ground_semantics`; ADR-013 W-5, W-12 |
+| What follows without granting truth on credit? | ZTL | ADR-009; profile `entrypoint: ztljudge.judge` |
+| Is the conclusion earned, refuted, on-credit, or open? | ZTL | profile `disposition_values`; ADR-013 §3.1 |
+| Is the result institutionally authorized for this purpose and epoch? | OIC | ADR-013 §2.2 `decision_basis`; `docs/contracts/WARRANT-CONTRACT-v0.1.md` |
+| May software execute an action? | downstream authority / runtime — **not ZTL** | ADR-013 §2.2 `execution_disposition`; ADR-009 forbids ZTL deciding ALLOW/BLOCK/ESCALATE |
+| Is execution integrity established? | VEIP | ADR-010; `docs/contracts/VEIP-CODE-START-BOUNDARY-v0.1.json` (non-executable); ADR-013 §4 |
+| Does historical consequence retain current standing? | OAM / Authority-VM boundary | **not found in this repository.** Reported as *not found*, which is not *absent* |
+
+## 2. A scope distinction that is easy to miss
+
+`review_docket.py` looks like the organ that reviews interpretations. It is not. It consumes
+`CandidateExtractionResult` — candidate **spans** — and never sees an
+`InterpretationProposalResult`. Its own docstring states it *"never votes, selects an
+authoritative interpretation, records admission, or advances candidate state."*
+
+The word *proposal* denotes two different objects in this tree: a proposed span and a proposed
+interpretation. The docket is upstream of interpretation, not downstream of it. **Divergence
+among interpretation proposals has no owner**, which is a third consequence of the two unowned
+rows above: nobody is appointed to accept an interpretation, and nobody is appointed to notice
+that two interpretations disagree.
+
+## 3. Currentness ownership — the rule
+
+> **ZTL may reason over supplied epoch, expiry, revocation and currentness facts. ZTL does not
+> create institutional currentness, validity, expiry authority or revocation authority.**
+
+This is an **ownership rule**, not a claim about the logic. It asserts no theorem, and no ZTL
+result is offered in support of it. It follows the boundary already drawn in ADR-009 —
+which prohibits ZTL from determining authority — and makes explicit what that boundary implies
+for currentness specifically, where the implication had not been written down.
+
+Consistent with it, and already stated in ADR-013 §3.3:
+
+- expiry is **scoped, never global**: `valid_until` is per artifact and `revocation_references`
+  are per ground; unrestricted expiry would make every warranty invariant trivially true;
+- `hereditary` is absorbing **only** under monotone refinement. It waives re-checking on
+  nothing else — not expiry, revocation, correction, source invalidation, schema change,
+  formula change, semantic-version change, or institutional admissibility.
+
+**No ADR text was rewritten to add this rule.** It is stated here because it is an ownership
+statement, and this is the ownership document. If normative consistency later requires it to
+appear in an ADR, that is a separate change with its own justification.
+
+## 4. Complexity as a ceiling, not a citation
+
+Minimality of a repair or recheck set is **not claimed** in this repository, deliberately and
+in three places: `docs/contracts/WARRANT-CONTRACT-v0.1.md` (*"Minimality is not claimed,
+deliberately"*, measured in 38 of 180 census cases), the kernel profile (*"NOT claimed. This is
+a deliberate over-approximation"*), and `docs/contracts/ZTL-OCE-MAPPING-v0.1.json` (*"Neither
+array claims minimality"*).
+
+`SUFFICIENT` and `MINIMAL_IF_ESTABLISHED` must remain distinct wherever a repair certificate is
+eventually emitted. **NP-completeness is not claimed anywhere**: hardness is not membership,
+and no claim here rests on one standing for the other.