diff --git a/research/reversible-cnf-independent-audit/PROOF.md b/research/reversible-cnf-independent-audit/PROOF.md
new file mode 100644
index 0000000000..5d4ba20edc
--- /dev/null
+++ b/research/reversible-cnf-independent-audit/PROOF.md
@@ -0,0 +1,349 @@
+# Independent audit of the reversible five-role CNF reduction
+
+Prepared for Hiroki KUMAZAKI (@kumagi), with substantial OpenAI Codex
+assistance in derivation, implementation, and review. New work is
+Apache-2.0.
+
+**Finding:** no defect was found in the reversible reduction or the
+coNP-completeness statement in Section 6 of Ali Romman's
+[PR #5369 proof](https://github.com/aliromman/integer-mult-bounds/blob/18354f41de4dc7bfda4692e814cf1d91a6d619ef/research/native-tensor-cutoff/PROOF.md)
+under its stated unbounded mathematical grammar. This audit spells out
+the dirty-input identity, chronological permutation convention, size
+recurrences, and input-encoding qualifications. In particular, the
+instruction bound is not a bound on the serialized bytes of arbitrarily
+large unused axis tables.
+
+The reviewed source is `reversible_cnf.py` and Section 6 at head
+`18354f41de4dc7bfda4692e814cf1d91a6d619ef`, unchanged in the package base
+`df0137efd35e11b4445734bf612bdd4c7ebc330c`. [SOURCES.json](SOURCES.json)
+pins the actual proof, compiler, arithmetic helper, and context. Mihir
+Srivastava's [PR #5521 audit](../native-cutoff-independent-audit/README.md)
+explicitly excluded this reduction and requested its separate review.
+
+## 1. The precise decision problem
+
+There are five independent, arbitrarily initialized roles. A role holds
+\((\mathbb C^{2^n})^{\otimes f}\), where \(n\ge1\) is unbounded and
+\(f\ge1\). The only native generators in this restricted class are
+
+\[
+ Z_j e_x=(-1)^{x_j}e_x.
+\]
+
+Permitted instructions are rational ADD and QUERY between distinct roles,
+unary APPLY of a \(Z_j\), and role SWAP. A query adds a rational multiple
+of \(Z_j^{\otimes f}\) of the current source to the current destination.
+All rational numerators and denominators and variable indices have
+ordinary finite binary encodings. The decision problem is equality of
+the complete five-role endpoints of two words, for all dirty inputs and
+all positive widths. The hardness construction uses the empty word as
+reference. It has no SCALE, CLEAR, assumed zero role, or discarded return.
+
+The signs on a tensor basis tuple \((x^{(1)},\ldots,x^{(f)})\) are
+
+\[
+ z_j=(-1)^{\sum_t x_j^{(t)}}\in\{1,-1\}.
+ \tag{1}
+\]
+
+No instruction changes its tuple of payload addresses. Restricting the
+complete word to such a tuple therefore gives an ordinary \(5\times5\)
+rational matrix, obtained by substituting these signs. Every assignment
+of the signs is realized at width one, and at any larger positive width
+by adding zero addresses. Hence complete endpoint equality in this
+class is exactly equality of those matrices at every sign assignment.
+This observation concerns commuting sign generators only; it is not an
+extension to arbitrary native or independent operators.
+
+## 2. The controlled swap on two arbitrary inputs
+
+Let \(z\) be an involution, initially either the scalar sign in (1) or
+the operator \(Z_j^{\otimes f}\). Define its complementary projectors
+\(p_+=(1+z)/2\) and \(p_-=(1-z)/2\). Since \(z^2=1\),
+
+\[
+ p_+^2=p_+,\quad p_-^2=p_-,\quad p_+p_-=0,\quad p_++p_-=1.
+\]
+
+The source's five chronological steps on arbitrary \(x,y\) are
+
+\[
+ x\leftarrow x-y,\quad
+ y\leftarrow y+x/2,\quad
+ y\leftarrow y-zx/2,\quad
+ x\leftarrow zx,\quad
+ x\leftarrow x+y.
+ \tag{2}
+\]
+
+After the first step set \(a=x_{\rm old}-y_{\rm old}\). The next
+two steps give \(y_{\rm new}=y_{\rm old}+(1-z)a/2\). The final
+two give \(x_{\rm new}=za+y_{\rm new}\). Thus the full endpoint is
+
+\[
+ \begin{pmatrix}x_{\rm new}\\y_{\rm new}\end{pmatrix}
+ =S(z)\begin{pmatrix}x_{\rm old}\\y_{\rm old}\end{pmatrix},
+ \qquad
+ S(z)=\begin{pmatrix}p_+&p_-\\p_-&p_+\end{pmatrix}.
+ \tag{3}
+\]
+
+In the commutative ring generated by \(z\),
+\(S(z)^2=I\) and \(\det S(z)=p_+^2-p_-^2=z\). At sign \(+1\)
+the endpoint is the identity; at sign \(-1\) it is the swap. Both
+initial values remain independent throughout the derivation: setting
+either input to zero is unnecessary and would not check the claimed
+dirty-input contract. The other three roles are unchanged.
+
+Each ADD or QUERY in (2) is a distinct-role shear, with inverse obtained
+by negating its coefficient. APPLY of \(z\) is its own inverse. Thus
+every individual instruction is invertible, not merely the completed
+two-role map. The only nonintegral coefficients are \(1/2,-1/2\).
+
+The source's serialized generator has identity affine matrix rows,
+zero offset and constant phase, zero quadratic rows, and linear phase
+coefficient two at coordinate \(j\). Its literal input phase is
+\(i^{2x_j}=(-1)^{x_j}\), so it is precisely the required \(Z_j\),
+including at tensor width \(f\) via (1).
+
+## 3. Chronological permutations and lowering a branch
+
+Represent a permutation by its five images, with
+\((pq)(i)=p(q(i))\): the rightmost map acts first. A chronological
+list \(g_1,\ldots,g_L\) therefore has endpoint
+\(g_L\cdots g_1\). This is the convention in the source's
+`compose` and `evaluate`.
+
+A cycle \((i,j_1,\ldots,j_{s-1})\) is implemented by the chronological
+swaps \((i,j_1),(i,j_2),\ldots,(i,j_{s-1})\). Their product sends
+\(i\) to \(j_1\), each \(j_t\) to \(j_{t+1}\), and the last
+element back to \(i\). This proves the order used by `swaps`, not
+only the unordered transposition decomposition. Disjoint cycles need
+at most \(5-\text{number of cycles}\le4\) swaps in total.
+
+For a branch selecting \(a\) at bit zero and \(b\) at bit one,
+`lower_word` first performs \(a\), then performs the swaps for
+\(ba^{-1}\), with each swap replaced by (2). The controlling sign
+is \(z=(-1)^{\text{bit}}\). At bit zero the second part is identity;
+at bit one the endpoint is \((ba^{-1})a=b\). Thus both branches
+act on every dirty column with exactly the specified permutation.
+The cost is at most \(4+5\cdot4=24\) register instructions. A
+constant branch has \(a=b\) and needs only the first permutation;
+the same upper bound remains valid.
+
+`invert_word` reverses the chronological list and replaces both branch
+permutations by their inverses. On each assignment its endpoint is
+therefore the inverse of the original endpoint. Inverting individual
+permutations without reversing the list would not establish this fact.
+
+## 4. Boolean compilation and the commutator convention
+
+Use the source's three permutations
+
+\[
+ A=(1,2,3,4,0),\quad B=(1,3,0,4,2),\quad
+ C=B^{-1}A^{-1}BA=(4,3,1,0,2).
+ \tag{4}
+\]
+
+Each is a five-cycle. For any five-cycle target \(T\), the compiler
+maintains the invariant: its word is identity when the Boolean formula
+is false and \(T\) when the formula is true.
+
+For a positive literal, a single branch selects identity or \(T\)
+at its variable's zero or one value. A negative literal reverses those
+branches. Boolean false is the empty word, and Boolean true is one
+constant \(T\) branch. The implementation distinguishes Boolean
+constants from integer literal indices before testing the integer case.
+
+For NOT, invert the child word and append the constant \(T\) branch.
+If its child endpoint is \(P\), the chronological endpoint is
+\(TP^{-1}\), which is \(T\) for \(P=I\) and \(I\) for \(P=T\).
+
+For AND, construct \(F\) by
+\(F(C^j(0))=T^j(0)\), for \(0\le j<5\). Both cycles visit all five
+points, so this defines a permutation and proves \(FCF^{-1}=T\).
+Compile the children with targets \(FAF^{-1}\) and \(FBF^{-1}\).
+If their endpoints are \(P,Q\), the chronological list
+
+\[
+ \text{word}(P),\ \text{word}(Q),\
+ \text{word}(P)^{-1},\ \text{word}(Q)^{-1}
+\]
+
+has endpoint **\(Q^{-1}P^{-1}QP\)**. If either child is false, the
+nonidentity factors cancel. If both are true, this endpoint is
+\(F(B^{-1}A^{-1}BA)F^{-1}=T\), using exactly (4). This checks the
+chronological order in the source; a different convention for a
+commutator cannot silently be substituted. OR is compiled as
+\(\neg(\neg P\wedge\neg Q)\), so the same invariant proves it.
+
+Induction establishes the invariant for every formula constructed by
+the compiler, including repeated and negated literals, tautological
+clauses, and the Boolean constants. In particular an empty clause is
+false, while an empty conjunction of clauses is true. With root target
+\(A\), the CNF endpoint is exactly \(A\) on satisfying assignments
+and identity on all others.
+
+## 5. The three size bounds and what they count
+
+Let \(w(F)\) count group-program branch instructions. A literal has
+length one, NOT changes length \(s\) to \(s+1\), AND of lengths
+\(s,t\) has length \(2s+2t\), and the displayed OR construction
+has length \(2s+2t+5\). A clause with one, two, or three literals
+therefore has length at most \(1,9,25\), respectively. An empty
+clause has length zero. These are bounds for the actual syntactic
+construction; they do not depend on simplification of the formula.
+
+For \(m\ge1\) clauses, `balanced` pairs adjacent nodes and carries
+an unmatched last node to the next level. It takes at most
+\(\lceil\log_2m\rceil\) rounds. Each AND ancestor duplicates a
+clause word twice, so its total multiplicity is at most
+\(2^{\lceil\log_2m\rceil}\). Consequently
+
+\[
+ w(\text{CNF})\le25m\,2^{\lceil\log_2m\rceil}\le50m^2.
+ \tag{5}
+\]
+
+For \(m=0\), the empty conjunction compiles to one constant branch,
+which also satisfies \(50\max(1,m)^2\). Applying the 24-instruction
+branch lowering gives
+
+\[
+ \text{register instructions}\le1200\max(1,m)^2.
+ \tag{6}
+\]
+
+This is an instruction-count bound. To obtain a polynomial-time
+many-one reduction with ordinary input encodings, first relabel the
+distinct variables actually appearing in the 3-CNF as \(1,\ldots,q\).
+There are at most \(3m\); choose \(n=\max(1,q)\). This renaming
+preserves satisfiability and is polynomial in the original binary
+input length, including when the old variable names are very large.
+
+The source `lower_word` emits all \(n\) generators, each with dense
+length-\(n\) recipe tables. There are \(O(n^2)\) integer entries,
+but each identity matrix row `1 << j` has \(j+1\) bits. Repeating
+those rows in all generators gives \(O(n^3)\) bits in the explicit
+tables, rather than \(O(n^2)\) bits. The word serialization adds
+\(O(\max(1,m)^2\log(n+1))\) bits, since roles and coefficients
+have constant size and generator indices have logarithmic size.
+With the renaming above, both output length and construction time are
+polynomial. Equations (5)–(6) do not claim a quadratic byte bound for
+an arbitrary binary-declared \(n\) with many unused axes.
+
+## 6. coNP membership with an explicit bit bound
+
+For two input words, let \(S\) be the set of generator indices
+actually referenced in either word. Assign one bit to each element
+of \(S\), and identify a differing row/column of their five-role
+endpoints. This is a polynomial-size certificate of inequality.
+Only referenced generators require signs: with \(L\) total
+instructions, \(|S|\le L\). If \(n\) is given compactly in binary,
+there is no need to write a full \(n\)-bit assignment to unused axes.
+Conceptually, put zeros on those axes to realize the supplied signs
+as a payload address. The certificate verifier works with signs and
+does not construct that potentially huge dense address.
+
+Exact endpoint evaluation also has polynomial bit complexity. Normalize
+each rational shear coefficient as \(p_t/q_t\), where \(q_t>0\).
+At a fixed sign assignment its elementary matrix \(M_t\) has
+\(N_t=q_tM_t\) integral and
+
+\[
+ \|N_t\|_\infty\le q_t+|p_t|,
+\]
+
+where the norm is the maximum absolute row sum. For an APPLY or SWAP
+take \(q_t=1\) and bound \(\|N_t\|_\infty\le1\). At every
+prefix, the endpoint has the unreduced representation
+
+\[
+ M_s\cdots M_1
+  =\frac{N_s\cdots N_1}{\prod_{t=1}^s q_t},\qquad
+ \|N_s\cdots N_1\|_\infty
+  \le\prod_{t=1}^s\|N_t\|_\infty.                  \tag{7}
+\]
+
+Thus denominator bit length is at most the sum of denominator bit
+lengths, and numerator bit length is at most
+\(1+\sum_t\lceil\log_2\max(1,q_t+|p_t|)\rceil\), taking zero
+contribution for the unit-norm steps. This is bounded by the total
+coefficient encoding length plus \(O(L)\). Reduction of fractions
+can only shorten the resulting numerator and denominator. The same
+bound holds for every prefix; comparing the two final rational
+matrices by cross multiplication adds their bit bounds. Constant-size
+matrix arithmetic on these integers takes polynomial time.
+
+By Section 1, a true endpoint discrepancy occurs at some assignment
+of the referenced signs, and conversely any certified matrix
+discrepancy is a genuine dirty-input discrepancy at width one. This
+proves that the complement of the equality problem is in NP, hence
+the equality problem is in coNP. The source's stated bit bound is
+valid; (7) makes the denominator and magnitude accounting explicit.
+
+## 7. Hardness and the implementation boundary
+
+Start with the classical coNP-complete problem of 3-CNF
+unsatisfiability, perform the variable renaming in Section 5, and
+emit the source compiler's five-role word with empty reference.
+Sections 2–4 show that on each sign assignment its full endpoint is
+identity or the nonidentity five-cycle \(A\), according as the
+formula is false or true. Every assignment is realized by a tensor
+basis address. Therefore
+
+\[
+ \text{CNF is unsatisfiable}
+ \quad\Longleftrightarrow\quad
+ \text{compiled word equals the empty reference on all dirty inputs
+ and all positive widths}.                           \tag{8}
+\]
+
+A satisfying assignment produces a differing role endpoint; it is
+not merely a difference on an auxiliary register that the contract
+allows one to ignore. The construction has exactly five arbitrary
+input roles, returns all five, and every emitted step is invertible.
+The size and encoding discussion proves that (8) is a polynomial-time
+many-one reduction. Together with Section 6, this establishes the
+source's coNP-completeness assertion for its stated unbounded class.
+
+The predecessor's command-line implementation limits axes to 256 and
+has separate role and stored-term limits. Those are explicitly
+distinct from the unbounded theorem. We do not ascribe the unbounded
+complexity classification to a fixed-axis finite implementation, and
+we do not treat a stored-term resource failure as an equality decision.
+No physical native cost, multiplication bound, or fast general solver
+follows from the reduction.
+
+## 8. Scope of acceptance and credit
+
+| Source obligation | Result of this review | Important premise |
+|---|---|---|
+| Five-step controlled swap | Exact complete endpoint (3), determinant \(z\), and invertibility of each step | Distinct roles and involution \(z^2=1\); neither input is clean |
+| `swaps`, branch lowering, and `invert_word` | Chronological permutation semantics established | A permutation is stored by its images; later instructions multiply on the left |
+| Conjugator, AND, NOT, OR, and constants | Boolean invariant proved by induction | Recursive targets are five-cycles; empty clause and empty conjunction differ |
+| 25, \(50\max(1,m)^2\), and \(1200\max(1,m)^2\) bounds | Analytically established for the actual construction | These count instructions, not all serialized bytes |
+| Polynomial hardness reduction | Established by (8) and the explicit output-size bound | Renumber used variables before emitting dense generator tables |
+| coNP membership | Referenced-sign certificate and exact bit bound (7) | Restricted commuting-sign alphabet and complete five-role endpoints |
+| General native compiler, four-width theorem, source event8814, physical supplier, or multiplication theorem | Outside this audit | No acceptance of these separate obligations is inferred |
+
+The executable evidence binds the actual source-emitted words to a
+separate literal endpoint implementation and targeted rejection
+controls. Its precise executed cases and counts belong to the
+verification receipt. Finite tests corroborate the induction and
+arithmetic claims; they do not prove coNP-hardness by enumeration.
+This is a separate agent-assisted audit, not independent human
+acceptance or proof-assistant verification.
+
+Ali Romman retains credit for PR #5369's stated reduction, source
+compiler, and native dirty-register formulation. Barrington's
+width-five permutation-program construction and classical 3-CNF
+complexity theory retain their original credit; this audit claims
+neither a new coNP theorem nor a new branching-program method.
+Mihir Srivastava retains credit for PR #5521's earlier scoped audit
+and this explicit remaining review request. Jose Manuel and the
+native/phase/compiler lineage credited by the predecessor remain
+credited; all retained source files are unchanged. The selected
+frontier, physical suppliers, and complete multiplication exponent
+are unaffected.
diff --git a/research/reversible-cnf-independent-audit/README.md b/research/reversible-cnf-independent-audit/README.md
new file mode 100644
index 0000000000..5ae1ef6558
--- /dev/null
+++ b/research/reversible-cnf-independent-audit/README.md
@@ -0,0 +1,132 @@
+# Independent audit of the reversible dirty-CNF reduction
+
+PR #5369's Section 6 reduction and stated coNP-completeness result hold for
+the declared unbounded five-role commuting-sign grammar. **No defect was
+found in this scope.** [PROOF.md](PROOF.md) supplies an independent derivation
+of the dirty controlled swap, chronological Boolean compiler, instruction
+bounds, exact arithmetic bit bound and the required input-encoding choices.
+This answers the separate review question explicitly left open by
+[PR #5521](../native-cutoff-independent-audit/README.md).
+
+The audit makes a distinction explicit: **at most 1200·max(1,m)² instructions
+is not a quadratic serialized-byte bound**. The source emits dense generator
+tables containing O(n³) bits. Renumbering used variables first gives
+n≤max(1,3m), so the complete reduction remains polynomial. This preprocessing
+is part of the audited reduction argument; the source compiler does not
+automatically perform it. A certificate of inequality only needs signs for
+referenced generators, avoiding a huge unused-axis assignment.
+
+No new hardness theorem, tensor cutoff, physical supplier or κ is claimed.
+Barrington's width-five construction and Ali Romman's native reduction retain
+their credit. The current selected P104 κ=62009/20000000 and its five premises
+remain unchanged.
+
+## Independent evidence
+
+The actual pinned `reversible_cnf.py` compiler generates the words under test.
+A separately written [literal.py](literal.py) evaluates their full 5×5 rational
+endpoints. It reads the serialized phase recipes and all tensor columns;
+generator names are opaque. The source's evaluator, general verifier,
+composition helpers and arithmetic are not used as the expected-result oracle.
+The compiler imports its unchanged `exact.py` dependency for validation.
+
+[RESULT.json](RESULT.json) records:
+
+- All **14,400 pairs of five-role permutations**, with **28,800 complete dirty
+  branch endpoints**, plus 120 constant endpoints. The maximum emitted branch
+  length is 24 instructions. All 24 five-cycle targets also pass the conjugated
+  AND check on all four assignments.
+- **1,807 CNFs / 14,456 assignments** built from all 42 canonical clauses of
+  up to three distinct signed literals on three variables. This checks the
+  source group program against direct Boolean truth, including empty clauses,
+  tautologies and contradictions.
+- **820 literal tensor blocks** at widths 1,2,3 for seven complete emitted-CNF
+  fixtures, with all five independent dirty input columns. This includes the
+  complete three-axis tuple domain through width 3 and a sparse-label case.
+  Separately, 120 local controlled-swap endpoints cover all 20 ordered role pairs.
+- Actual clause lengths 0,1,9,25, plus 24 balanced-size fixtures through 65 clauses.
+  A 201-bit variable-name fixture is compressed to three axes and checked on
+  all eight assignments without constructing a huge dense axis table.
+- **Eight semantic mutations**, each producing a recorded wrong matrix entry:
+  missing inverse reversal, wrong relative-product order, reversed cycle swaps,
+  wrong empty-conjunction semantics, query-sign error, missing final ADD,
+  erased variable sign, and an extra constant phase. The last mutation passes
+  the specified even-width control and fails at odd width. Seven invalid
+  compiler inputs are also rejected.
+
+The eight semantic failures are endpoint discrepancies, not hash failures.
+Source-code mutations execute separate in-memory compiler copies; serialized
+program/recipe mutations operate on deep copies. All original source bytes
+remain unchanged. Finite controls corroborate the written proof; they do not
+establish a complexity theorem by enumeration.
+
+## Source and scope
+
+Source: [PR #5369](https://github.com/CrocSwap/integer-mult-bounds/pull/5369),
+head `18354f41de4dc7bfda4692e814cf1d91a6d619ef`. Its proof, README, compiler and
+arithmetic helper are unchanged at canonical main
+`df0137efd35e11b4445734bf612bdd4c7ebc330c` and pinned in
+[SOURCES.json](SOURCES.json). The PR #5521 review README and repository license
+complete the six declared live inputs.
+
+The scope is the five-role reversible reduction in Section 6. General native
+composition, self-query semantics, the four-width cutoff theorem, source
+event8814, physical cost/storage/precision and the full multiplication theorem
+are outside this review. The predecessor's CLI has separate finite axis and
+stored-term limits; the unbounded coNP statement is not attributed to a
+fixed-axis implementation. No general-source or selected cold replay was run.
+
+The picker ran once with seed `aa32479c3ec3e4781cbe692d0b861686`, selecting the
+bit-mechanisms track. [TASK.json](TASK.json) explicitly records the handoff-first
+override to the `formal-interface-lemma` card for this uncovered proof/source
+implication. No formal proof-assistant build is claimed.
+
+The initial overlap snapshot covered 7,676 local notes, 395 open PRs and 5,055
+Discussion records with complete reported pagination and no warnings. Exact
+Discussion #5354 and targeted all-status Barrington/coNP/CNF searches found the
+source and complementary cutoff successors, with no competing Section 6 audit.
+These searches do not cover unpublished work or every historical code diff.
+[Canonical claim and handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/5354#discussioncomment-19192650).
+
+## Reproduce
+
+Python 3.12 and its standard library; one registered command with a 120 s timeout.
+The local scientific replay takes about four seconds.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/reversible-cnf-independent-audit --check-only
+python3.12 -B scripts/research_package.py --package research/reversible-cnf-independent-audit
+python3.12 -I -O -B research/reversible-cnf-independent-audit/verify.py
+```
+
+The direct verifier checks all six pinned inputs before loading the source
+compiler, executes the independent checks and compares the deterministic
+receipt. It does not rewrite evidence or require Git/network access. An export
+must retain the declared repository-relative source paths.
+[VERIFICATION.md](VERIFICATION.md) records executed checks and their limits.
+
+## Open next questions
+
+A separate source-bound audit is still needed for the general native endpoint
+compiler at a concrete physical caller, including generator composition,
+inversion, self-query conventions, and every dirty input/return. This sign-only
+reduction cannot supply that coverage. Another justified direction would name
+a useful caller restriction and prove a tractable identity-test bound while
+preserving the complete endpoint contract. No such restriction is supplied
+here; the general hardness result is not a barrier for every subclass.
+[TASK.json](TASK.json) gives the relevance, first steps and blockers.
+
+## Credit
+
+Ali Romman retains the source compiler and native dirty-register reduction.
+Barrington retains the classical width-five branching-program construction;
+classical CNF complexity theory is not new here. Mihir Srivastava retains
+PR #5521's earlier cutoff audit and this review request. Jose Manuel and all
+native/phase/compiler predecessors named in the source retain their attribution.
+No predecessor file is changed and no predecessor executable is copied.
+
+New proof, checks and prose prepared for Hiroki KUMAZAKI, with substantial
+OpenAI Codex assistance. Delegated agents scoped overlap, independently derived
+and reviewed the proof/encoding, implemented the literal interpreter and
+reviewed the semantic controls. This is agent-assisted independent review,
+not human acceptance or proof-kernel verification. Apache-2.0.
diff --git a/research/reversible-cnf-independent-audit/RESULT.json b/research/reversible-cnf-independent-audit/RESULT.json
new file mode 100644
index 0000000000..26a7055751
--- /dev/null
+++ b/research/reversible-cnf-independent-audit/RESULT.json
@@ -0,0 +1,303 @@
+{
+  "authenticated_inputs": 6,
+  "checks": {
+    "branches": {
+      "all_permutations": 120,
+      "branch_pairs": 14400,
+      "constant_endpoints": 120,
+      "literal_branch_endpoints": 28800,
+      "maximum_emitted_instructions": 24
+    },
+    "conjugation": {
+      "complete_dirty_endpoints": 96,
+      "target_five_cycles": 24
+    },
+    "formula_truth": {
+      "assignment_checks": 14456,
+      "canonical_clauses": 42,
+      "clause_lengths_0_to_3": [
+        0,
+        1,
+        9,
+        25
+      ],
+      "formulas": 1807
+    },
+    "invalid_inputs": {
+      "rejected_inputs": 7
+    },
+    "local_controls": {
+      "Boolean_boundary_controls": 4,
+      "complete_five_column_endpoints": 120,
+      "opaque_generator_name_control": true,
+      "ordered_role_pairs": 20,
+      "tensor_tuples_per_pair": 6,
+      "tensor_widths": [
+        1,
+        2,
+        3
+      ]
+    },
+    "mutations": {
+      "constant_phase_even_width_control_passes": true,
+      "semantic_rejections": 8,
+      "witnesses": [
+        {
+          "differing_entry": {
+            "actual": "0",
+            "dirty_input_role": 0,
+            "output_role": 0,
+            "required": "1"
+          },
+          "mutation": "omit inverse-word reversal",
+          "tensor_addresses": [
+            0
+          ]
+        },
+        {
+          "differing_entry": {
+            "actual": "0",
+            "dirty_input_role": 2,
+            "output_role": 0,
+            "required": "1"
+          },
+          "mutation": "reverse relative permutation product",
+          "tensor_addresses": [
+            1
+          ]
+        },
+        {
+          "differing_entry": {
+            "actual": "1",
+            "dirty_input_role": 1,
+            "output_role": 0,
+            "required": "0"
+          },
+          "mutation": "reverse cycle swap chronology",
+          "tensor_addresses": [
+            0
+          ]
+        },
+        {
+          "differing_entry": {
+            "actual": "1",
+            "dirty_input_role": 0,
+            "output_role": 0,
+            "required": "0"
+          },
+          "mutation": "empty conjunction made false",
+          "tensor_addresses": [
+            0
+          ]
+        },
+        {
+          "differing_entry": {
+            "actual": "2",
+            "dirty_input_role": 0,
+            "output_role": 0,
+            "required": "1"
+          },
+          "mutation": "flip controlled-query sign",
+          "tensor_addresses": [
+            0
+          ]
+        },
+        {
+          "differing_entry": {
+            "actual": "-1",
+            "dirty_input_role": 1,
+            "output_role": 0,
+            "required": "0"
+          },
+          "mutation": "omit final controlled-swap ADD",
+          "tensor_addresses": [
+            0
+          ]
+        },
+        {
+          "differing_entry": {
+            "actual": "1",
+            "dirty_input_role": 0,
+            "output_role": 0,
+            "required": "0"
+          },
+          "mutation": "erase variable sign",
+          "tensor_addresses": [
+            1
+          ]
+        },
+        {
+          "differing_entry": {
+            "actual": "1",
+            "dirty_input_role": 0,
+            "output_role": 0,
+            "required": "0"
+          },
+          "mutation": "extra constant phase hidden at even widths",
+          "tensor_addresses": [
+            1
+          ]
+        }
+      ]
+    },
+    "native_cnf": {
+      "dirty_input_columns_per_block": 5,
+      "fixtures": {
+        "contradiction": 14,
+        "empty-clause": 14,
+        "empty-conjunction": 14,
+        "mixed-three-axis": 584,
+        "mixed-two-axis": 84,
+        "sparse-label": 96,
+        "tautology": 14
+      },
+      "literal_tensor_blocks": 820,
+      "max_program_instructions": 768,
+      "oracle_assignment": "XOR of every tensor column address",
+      "tensor_widths": [
+        1,
+        2,
+        3
+      ]
+    },
+    "sizes": {
+      "bit_encoding_qualification": "generator-table O(n^3) bits; renumber used variables before reduction",
+      "cases": 24,
+      "native_bound": "24 per branch; at most 1200*max(1,m)^2 instructions",
+      "rows": [
+        {
+          "branch_instructions": 1,
+          "clauses": 0,
+          "proved_upper": 1
+        },
+        {
+          "branch_instructions": 25,
+          "clauses": 1,
+          "proved_upper": 25
+        },
+        {
+          "branch_instructions": 100,
+          "clauses": 2,
+          "proved_upper": 100
+        },
+        {
+          "branch_instructions": 250,
+          "clauses": 3,
+          "proved_upper": 300
+        },
+        {
+          "branch_instructions": 400,
+          "clauses": 4,
+          "proved_upper": 400
+        },
+        {
+          "branch_instructions": 850,
+          "clauses": 5,
+          "proved_upper": 1000
+        },
+        {
+          "branch_instructions": 1000,
+          "clauses": 6,
+          "proved_upper": 1200
+        },
+        {
+          "branch_instructions": 1300,
+          "clauses": 7,
+          "proved_upper": 1400
+        },
+        {
+          "branch_instructions": 1600,
+          "clauses": 8,
+          "proved_upper": 1600
+        },
+        {
+          "branch_instructions": 3250,
+          "clauses": 9,
+          "proved_upper": 3600
+        },
+        {
+          "branch_instructions": 3400,
+          "clauses": 10,
+          "proved_upper": 4000
+        },
+        {
+          "branch_instructions": 3700,
+          "clauses": 11,
+          "proved_upper": 4400
+        },
+        {
+          "branch_instructions": 4000,
+          "clauses": 12,
+          "proved_upper": 4800
+        },
+        {
+          "branch_instructions": 4900,
+          "clauses": 13,
+          "proved_upper": 5200
+        },
+        {
+          "branch_instructions": 5200,
+          "clauses": 14,
+          "proved_upper": 5600
+        },
+        {
+          "branch_instructions": 5800,
+          "clauses": 15,
+          "proved_upper": 6000
+        },
+        {
+          "branch_instructions": 6400,
+          "clauses": 16,
+          "proved_upper": 6400
+        },
+        {
+          "branch_instructions": 12850,
+          "clauses": 17,
+          "proved_upper": 13600
+        },
+        {
+          "branch_instructions": 24400,
+          "clauses": 31,
+          "proved_upper": 24800
+        },
+        {
+          "branch_instructions": 25600,
+          "clauses": 32,
+          "proved_upper": 25600
+        },
+        {
+          "branch_instructions": 51250,
+          "clauses": 33,
+          "proved_upper": 52800
+        },
+        {
+          "branch_instructions": 100000,
+          "clauses": 63,
+          "proved_upper": 100800
+        },
+        {
+          "branch_instructions": 102400,
+          "clauses": 64,
+          "proved_upper": 102400
+        },
+        {
+          "branch_instructions": 204850,
+          "clauses": 65,
+          "proved_upper": 208000
+        }
+      ]
+    },
+    "variable_renaming": {
+      "clauses": 3,
+      "compact_axes": 3,
+      "complete_dirty_endpoints": 8,
+      "largest_original_variable_bits": 201,
+      "source_compiler_auto_renaming_claimed": false
+    }
+  },
+  "new_hardness_theorem_or_kappa": false,
+  "reviewed_source_head": "18354f41de4dc7bfda4692e814cf1d91a6d619ef",
+  "source_compiler_executed": true,
+  "source_evaluator_or_verifier_used": false,
+  "status": "PASS_REVERSIBLE_CNF_INDEPENDENT_AUDIT"
+}
diff --git a/research/reversible-cnf-independent-audit/SOURCES.json b/research/reversible-cnf-independent-audit/SOURCES.json
new file mode 100644
index 0000000000..267505b2f1
--- /dev/null
+++ b/research/reversible-cnf-independent-audit/SOURCES.json
@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c",
+  "files": [
+    {
+      "path": "LICENSE",
+      "usage": "input",
+      "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64",
+      "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/native-cutoff-independent-audit/README.md",
+      "usage": "input",
+      "git_blob": "0269df4ad725d5c8ec982556f6d3c620db8cc516",
+      "sha256": "4f3c3c92059c51760990c7635f43c6d0a2b26b59214f6d9e7d37b2d8ad7a60b8"
+    },
+    {
+      "path": "research/native-tensor-cutoff/PROOF.md",
+      "usage": "input",
+      "git_blob": "2d92f17cd8e1064028656cd4ff06c1d38f14ebc0",
+      "sha256": "b2d31ea52b652f43cc8576affde6092a884d2832820221a43933e7e27dc07041"
+    },
+    {
+      "path": "research/native-tensor-cutoff/README.md",
+      "usage": "input",
+      "git_blob": "91ae9eadd8a8679de7cf488fc2e3f350214feeff",
+      "sha256": "98a3166b7d0db513e8918f17f73359bebde1f802af251f6c55305fb99b869f87"
+    },
+    {
+      "path": "research/native-tensor-cutoff/exact.py",
+      "usage": "input",
+      "git_blob": "4f8514d1a2ab211b46e820e030e2feda36a4882c",
+      "sha256": "6d918d23200b7603b620fbe0a3efefd5d05a20d0b99ad8bb9a43b8fcb9e39130"
+    },
+    {
+      "path": "research/native-tensor-cutoff/reversible_cnf.py",
+      "usage": "input",
+      "git_blob": "6878b4c33e6e0fa1ed8d51b7dfe029d54cd46f3d",
+      "sha256": "428df1de10c9d724dcdb03aa789980c06b8fc3d63d6722f23fdb36e9b6934e1d"
+    }
+  ]
+}
diff --git a/research/reversible-cnf-independent-audit/TASK.json b/research/reversible-cnf-independent-audit/TASK.json
new file mode 100644
index 0000000000..f66f6be3b5
--- /dev/null
+++ b/research/reversible-cnf-independent-audit/TASK.json
@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Independently audit PR5369 PROOF.md \u00a76 and reversible_cnf.py: complete dirty controlled swap, chronological Boolean compiler, actual source-emitted five-role endpoints, instruction and exact-bit bounds.",
+  "scope_change_reason": "Handoff-first override of one picker run (bit-mechanisms; seed aa32479c3ec3e4781cbe692d0b861686). PR5521 explicitly leaves this proof/source implication open. Use formal-interface-lemma for a scoped mathematical audit before any formalization; no reroll or new cutoff campaign.",
+  "bottleneck_link": "The native identity checker has a claimed complexity boundary even for reversible dirty programs. A source-bound independent reduction audit checks whether that boundary is valid and clarifies why finite solver limits or small-width samples cannot imply a general efficient checker; no physical supplier cost follows.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the explicit \u00a76 compiler/equivalence/size audit and bounded independent rational controls. Do not rerun the general source verifier, extend tensor cutoffs, claim a new hardness theorem, or start physical supplier/Lean/cold-admission work.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the quantified audit and encoding qualification. RESULT.json binds actual source compilation to a separate five-role rational interpreter: all14400 branch pairs,28800 branch endpoints,820 full-CNF tensor blocks at widths1\u20133, all24 five-cycle targets,14456 truth-table checks, eight semantic mutant witnesses and seven input rejections.",
+  "author": "Hiroki KUMAZAKI",
+  "ai_assistance": "Substantial OpenAI Codex assistance in mathematical derivation, code, verification and prose. Delegated agents independently scoped live handoffs, reviewed the proof/encoding, implemented the literal endpoint interpreter and checked semantic boundaries. This is not independent human or proof-kernel acceptance.",
+  "open_questions": [
+    {
+      "question": "Does the general native endpoint compiler preserve its declared grammar and complete dirty state at an actual source-bound caller?",
+      "why_it_matters": "This audit covers only the commuting-sign CNF reduction, not arbitrary affine/quadratic native maps or the source solver implementation.",
+      "first_step": "Choose one unclaimed concrete caller and pin the generator composition/inversion, self-query conventions, independent inputs and required returns; compare emitted endpoints with a separate literal interpreter.",
+      "blocked_by": "A named caller and its full source closure; the present sign reduction supplies neither physical execution nor general compiler acceptance."
+    },
+    {
+      "question": "Can a practically useful tractable subclass of the native identity problem be isolated without changing the dirty-input contract?",
+      "why_it_matters": "The general coNP classification does not rule out efficient algorithms for a bounded or structurally restricted caller family.",
+      "first_step": "Name a concrete caller restriction, such as a fixed generator-support or role-interaction structure, and prove the resulting exact decision cost while preserving all returns.",
+      "blocked_by": "A useful actual caller restriction and full encoding/budget; finite solver samples alone do not provide such a theorem."
+    }
+  ]
+}
diff --git a/research/reversible-cnf-independent-audit/VERIFICATION.md b/research/reversible-cnf-independent-audit/VERIFICATION.md
new file mode 100644
index 0000000000..ba4f0289de
--- /dev/null
+++ b/research/reversible-cnf-independent-audit/VERIFICATION.md
@@ -0,0 +1,72 @@
+# Verification record
+
+Linux x86_64, Python 3.12.13, standard library only. Base:
+`df0137efd35e11b4445734bf612bdd4c7ebc330c`. The four reviewed source files
+are byte-identical to PR #5369 head
+`18354f41de4dc7bfda4692e814cf1d91a6d619ef`; exact Git blobs and SHA256 pins
+are in SOURCES.json.
+
+The initial source-bound scientific run completed in 3.47 seconds before the
+additional compact-label fixture. Every check uses explicit exceptions and
+remains enabled under optimization. The source compiler and its unchanged
+exact helper are executed; the source evaluator/verifier is not used as an
+oracle. Independent endpoint arithmetic uses Fraction throughout.
+
+The following completed successfully on 2026-10-26:
+
+```sh
+python3.12 -B scripts/research_selected_baseline.py
+python3.12 -B scripts/research_package.py --package research/reversible-cnf-independent-audit --check-only
+python3.12 -B scripts/research_package.py --package research/reversible-cnf-independent-audit
+python3.12 -I -O -B research/reversible-cnf-independent-audit/verify.py
+```
+
+The baseline checks selected source bindings/metadata, not scientific supplier
+admission. The complete scientific receipt from normal and optimized execution
+matches RESULT.json. The registered run checks source pins and all declared
+finite controls; the general-source and selected cold replays were not run.
+
+The pre-submission main refresh retained the same base. The fresh overlap
+snapshot at 09:55:16 UTC covered 7,676 HEAD notes plus the two new package notes,
+395 open PRs and 5,058 Discussion records with complete reported pagination
+and no warnings. No new competing §6 audit was found. This is reported search
+coverage, not a claim of novelty or coverage of unpublished work.
+
+The focused shared navigation test was also run to distinguish a known base
+failure from this package:
+
+```sh
+python3.12 -B -m unittest discover -s tests -p test_research_current_status.py
+```
+
+It ran six tests and failed the two subcases of
+`test_current_ci_section_matches_selected_record` for `review` and
+`source_manifest`. The current section of docs/ci-verification.md lacks links
+to the selected PR5599 review and certificates/frontier5599-source.json.
+Those tests, the document, selected files and workflows are unchanged by this
+contribution. Existing [PR #5703](https://github.com/CrocSwap/integer-mult-bounds/pull/5703)
+supplies the shared document repair; no duplicate fix is included here.
+This known planning failure is separate from the passing package replay.
+Hosted status will be reported on the published PR.
+
+Committed-byte/source-history and export checks also passed:
+
+```sh
+python3.12 -B scripts/check_research_commit.py --package research/reversible-cnf-independent-audit --check-source-history
+python3.12 -B scripts/export_research_package.py export --package research/reversible-cnf-independent-audit --output /tmp/imb-20261026-next-cnf.tar
+python3.12 -B scripts/export_research_package.py check /tmp/imb-20261026-next-cnf.tar
+```
+
+The deterministic export contains 16 package/input files. It was extracted
+with the tar data filter into a fresh directory outside the checkout. An
+absolute Python executable ran the direct verifier from `/tmp` with `-I -O -B`,
+`PATH=/nonexistent` and empty `PYTHONPATH`. Its complete scientific receipt
+matched the committed one without Git. In that disposable copy, changing
+RESULT.json caused the expected receipt mismatch, and changing the pinned
+compiler caused source-hash rejection before execution. Both transport
+controls were separate from the eight semantic endpoint mutations.
+
+After recording these results, final committed bytes were rechecked/exported
+and the full isolated optimized replay repeated in a second fresh tree.
+The canonical base and predecessor head were also reconfirmed immediately
+before publication. No frozen predecessor file was changed.
diff --git a/research/reversible-cnf-independent-audit/VERIFY.json b/research/reversible-cnf-independent-audit/VERIFY.json
new file mode 100644
index 0000000000..7d6abaccd4
--- /dev/null
+++ b/research/reversible-cnf-independent-audit/VERIFY.json
@@ -0,0 +1,25 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "LICENSE",
+    "research/native-cutoff-independent-audit/README.md",
+    "research/native-tensor-cutoff/PROOF.md",
+    "research/native-tensor-cutoff/README.md",
+    "research/native-tensor-cutoff/exact.py",
+    "research/native-tensor-cutoff/reversible_cnf.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Authenticate the exact compiler/proof closure; independently evaluate every emitted dirty matrix in the declared finite domain, Boolean truth and all permutation branches, tensor signs, size/encoding controls, eight semantic mutation witnesses and seven input rejections; compare deterministic receipt."
+    }
+  ]
+}
diff --git a/research/reversible-cnf-independent-audit/audit.py b/research/reversible-cnf-independent-audit/audit.py
new file mode 100644
index 0000000000..f84fa09b4a
--- /dev/null
+++ b/research/reversible-cnf-independent-audit/audit.py
@@ -0,0 +1,235 @@
+"""Independent source-compiler checks. Hiroki KUMAZAKI / OpenAI Codex.
+
+Apache-2.0. Source compilation is the system under review, never the oracle.
+"""
+from copy import deepcopy
+from itertools import combinations, permutations, product
+from functools import reduce
+from operator import xor
+
+IDENTITY = (0, 1, 2, 3, 4)
+TARGET = (1, 2, 3, 4, 0)
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def group_endpoint(word, assignment):
+    # Follow each source role through the chronological instruction list.
+    # No source compose, evaluate, inverse or swaps helper is used.
+    paths = list(range(5))
+    for variable, zero, one in word:
+        branch = one if variable is not None and ((assignment >> variable) & 1) else zero
+        paths = [branch[position] for position in paths]
+    return tuple(paths)
+
+
+def branch_census(source, literal):
+    perms = list(permutations(range(5)))
+    endpoints = 0
+    maximum = 0
+    for zero in perms:
+        constant = source.lower_word(1, [(None, zero, zero)])
+        need(len(constant['program']) <= 4, 'constant permutation swap bound')
+        need(literal.endpoint(constant, (0,)) == literal.permutation_matrix(zero),
+             'literal constant-permutation endpoint')
+        for one in perms:
+            problem = source.lower_word(1, [(0, zero, one)])
+            literal.strict_standard_generators(problem)
+            maximum = max(maximum, len(problem['program']))
+            need(len(problem['program']) <= 24, 'single-branch instruction bound')
+            for bit, wanted in enumerate((zero, one)):
+                need(literal.endpoint(problem, (bit,)) == literal.permutation_matrix(wanted),
+                     'literal two-branch complete dirty endpoint')
+                endpoints += 1
+    return {'all_permutations': len(perms), 'branch_pairs': len(perms)**2,
+            'literal_branch_endpoints': endpoints, 'constant_endpoints': len(perms),
+            'maximum_emitted_instructions': maximum}
+
+
+def five_cycle_conjugation(source, literal):
+    cycles = []
+    for tail in permutations(range(1, 5)):
+        sequence = (0,) + tail
+        images = [0]*5
+        for a, b in zip(sequence, sequence[1:] + sequence[:1]):
+            images[a] = b
+        cycles.append(tuple(images))
+    cases = 0
+    for target in cycles:
+        word = source.formula_word(('and', 1, 2), target)
+        problem = source.lower_word(2, word)
+        literal.strict_standard_generators(problem)
+        for assignment in range(4):
+            expected = target if assignment == 3 else IDENTITY
+            need(group_endpoint(word, assignment) == expected, 'conjugated AND group endpoint')
+            need(literal.endpoint(problem, (assignment,)) == literal.permutation_matrix(expected),
+                 'conjugated AND literal endpoint')
+            cases += 1
+    return {'target_five_cycles': len(cycles), 'complete_dirty_endpoints': cases}
+
+
+def formula_census(source, literal):
+    # Canonical clauses of up to three distinct signed literals, including
+    # tautologies and the empty clause. All ordered pairs are included.
+    literals = (-3, -2, -1, 1, 2, 3)
+    clauses = [list(c) for size in range(4) for c in combinations(literals, size)]
+    formulas = [[]] + [[c] for c in clauses] + [[a,b] for a in clauses for b in clauses]
+    checks = 0
+    for cnf in formulas:
+        word = source.cnf_word(3, cnf)
+        for assignment in range(8):
+            target = TARGET if literal.direct_clauses(cnf, assignment) else IDENTITY
+            need(group_endpoint(word, assignment) == target, 'CNF truth versus branch program')
+            checks += 1
+    lengths = [len(source.cnf_word(3, [list(range(1,size+1))])) for size in range(4)]
+    need(lengths == [0,1,9,25], 'clause-length base cases')
+    return {'canonical_clauses': len(clauses), 'formulas': len(formulas),
+            'assignment_checks': checks, 'clause_lengths_0_to_3': lengths}
+
+
+def native_cnf(source, literal):
+    fixtures = [
+        ('empty-conjunction',1,[]), ('empty-clause',1,[[]]),
+        ('tautology',1,[[1,-1]]), ('contradiction',1,[[1],[-1]]),
+        ('mixed-two-axis',2,[[1,-2],[2]]),
+        ('mixed-three-axis',3,[[1,-2,3],[-1,2]]),
+        ('sparse-label',5,[[5]]),
+    ]
+    counts = {}
+    maximum_instructions = 0
+    for name, n, cnf in fixtures:
+        problem = source.cnf_problem(n, cnf)
+        literal.strict_standard_generators(problem)
+        need(problem['reference'] == [], 'identity reference')
+        maximum_instructions = max(maximum_instructions, len(problem['program']))
+        domain = range(2**n)
+        tuples = [(a,) for a in domain]
+        if n <= 3:
+            tuples += list(product(domain, repeat=2)) + list(product(domain, repeat=3))
+        else:
+            tuples += [(a,a) for a in domain] + [(a,a,a) for a in domain]
+        for addresses in tuples:
+            assignment = reduce(xor, addresses, 0)
+            target = TARGET if literal.direct_clauses(cnf, assignment) else IDENTITY
+            need(literal.endpoint(problem, addresses) == literal.permutation_matrix(target),
+                 'literal CNF endpoint at full tensor address: ' + name)
+        counts[name] = len(tuples)
+    return {'fixtures': counts, 'literal_tensor_blocks': sum(counts.values()),
+            'dirty_input_columns_per_block': 5, 'tensor_widths': [1,2,3],
+            'max_program_instructions': maximum_instructions,
+            'oracle_assignment': 'XOR of every tensor column address'}
+
+
+def size_checks(source):
+    sizes = list(range(18)) + [31,32,33,63,64,65]
+    rows = []
+    for m in sizes:
+        cnf = [[1,2,3] for _ in range(m)]
+        word = source.cnf_word(3, cnf)
+        tighter = 1 if m == 0 else 25*m*2**((m-1).bit_length())
+        need(len(word) <= tighter <= 50*max(1,m)**2, 'balanced-tree size bound')
+        rows.append({'clauses':m, 'branch_instructions':len(word), 'proved_upper':tighter})
+    return {'cases':len(rows), 'rows':rows,
+            'native_bound': '24 per branch; at most 1200*max(1,m)^2 instructions',
+            'bit_encoding_qualification': 'generator-table O(n^3) bits; renumber used variables before reduction'}
+
+
+def renaming_control(source, literal):
+    # This audit's explicit preprocessing step, not a claim that the source
+    # compiler itself already compacts its caller's declared axis domain.
+    u, v, w = 2**200+3, 2**128+1, 2**65+7
+    original = [[u, -v, w], [-u, v], [-w, u]]
+    names = sorted({abs(x) for clause in original for x in clause})
+    positions = {name:i for i,name in enumerate(names)}
+    compact = [[(1 if x > 0 else -1)*(positions[abs(x)]+1) for x in clause]
+               for clause in original]
+    need(len(names) <= 3*len(original), 'used-variable bound')
+    problem = source.cnf_problem(len(names), compact)
+    literal.strict_standard_generators(problem)
+    for assignment in range(2**len(names)):
+        values = {name:bool((assignment >> positions[name]) & 1) for name in names}
+        expected_truth = all(any(values[abs(x)] if x > 0 else not values[abs(x)]
+                                 for x in clause) for clause in original)
+        need(literal.direct_clauses(compact, assignment) == expected_truth, 'renaming preserves truth')
+        target = TARGET if expected_truth else IDENTITY
+        need(literal.endpoint(problem, (assignment,)) == literal.permutation_matrix(target),
+             'compact encoding has the required complete dirty endpoint')
+    return {'largest_original_variable_bits':max(names).bit_length(),
+            'compact_axes':len(names), 'clauses':len(original),
+            'complete_dirty_endpoints':2**len(names),
+            'source_compiler_auto_renaming_claimed':False}
+
+
+def first_difference(left, right):
+    for i in range(5):
+        for j in range(5):
+            if left[i][j] != right[i][j]:
+                return {'output_role':i, 'dirty_input_role':j,
+                        'actual':str(left[i][j]), 'required':str(right[i][j])}
+    return None
+
+
+def mutation_checks(source, literal, mutated_source):
+    outcomes = []
+    def reject(name, problem, addresses, target):
+        wrong = literal.endpoint(problem, addresses)
+        delta = first_difference(wrong, literal.permutation_matrix(target))
+        need(delta is not None, 'semantic mutation survived: ' + name)
+        outcomes.append({'mutation':name, 'tensor_addresses':list(addresses), 'differing_entry':delta})
+    inverse_bad = mutated_source('for variable, zero, one in reversed(word)',
+                                'for variable, zero, one in word')
+    reject('omit inverse-word reversal', inverse_bad.cnf_problem(2, [[1,2]]), (0,), IDENTITY)
+    quotient_bad = mutated_source('swaps(compose(one, inverse(zero)))',
+                                 'swaps(compose(inverse(zero), one))')
+    zero, one = (1,2,3,4,0), (1,3,0,4,2)
+    reject('reverse relative permutation product', quotient_bad.lower_word(1, [(0,zero,one)]), (1,), one)
+    swap_bad = mutated_source('for i, j in swaps(zero)', 'for i, j in reversed(swaps(zero))')
+    reject('reverse cycle swap chronology', swap_bad.lower_word(1, [(None,TARGET,TARGET)]), (0,), TARGET)
+    empty_bad = mutated_source("for clause in clauses], True)", "for clause in clauses], False)")
+    reject('empty conjunction made false', empty_bad.cnf_problem(1, []), (0,), TARGET)
+    original = source.cnf_problem(1, [[1]])
+    bad = deepcopy(original)
+    query = next(gate for gate in bad['program'] if gate['op'] == 'query')
+    query['coefficient'] = '1/2'
+    reject('flip controlled-query sign', bad, (0,), IDENTITY)
+    bad = deepcopy(original)
+    need(bad['program'][4] == {'op':'add','src':1,'dst':0}, 'expected first controlled swap end')
+    del bad['program'][4]
+    reject('omit final controlled-swap ADD', bad, (0,), IDENTITY)
+    bad = deepcopy(original)
+    next(iter(bad['generators'].values()))['linear_Z4'] = [0]
+    reject('erase variable sign', bad, (1,), TARGET)
+    bad = deepcopy(original)
+    next(iter(bad['generators'].values()))['phase'] = 2
+    need(literal.endpoint(bad, (1,0)) == literal.endpoint(original, (1,0)),
+         'constant-phase mutation must pass this even-width control')
+    reject('extra constant phase hidden at even widths', bad, (1,), TARGET)
+    return {'semantic_rejections':len(outcomes), 'witnesses':outcomes,
+            'constant_phase_even_width_control_passes':True}
+
+
+def invalid_inputs(source):
+    cases = [(0, []), (True, []), (1.0, []), (1, [[0]]), (1, [[True]]),
+             (1, [[2]]), (1, [[1,1,1,1]])]
+    for n, clauses in cases:
+        try:
+            source.cnf_problem(n, clauses)
+        except ValueError:
+            continue
+        raise ValueError('invalid compiler input was accepted')
+    return {'rejected_inputs':len(cases)}
+
+
+def run(source, literal, mutated_source):
+    return {'local_controls':literal.run_local_controls(),
+            'branches':branch_census(source,literal),
+            'conjugation':five_cycle_conjugation(source,literal),
+            'formula_truth':formula_census(source,literal),
+            'native_cnf':native_cnf(source,literal),
+            'sizes':size_checks(source),
+            'variable_renaming':renaming_control(source,literal),
+            'mutations':mutation_checks(source,literal,mutated_source),
+            'invalid_inputs':invalid_inputs(source)}
diff --git a/research/reversible-cnf-independent-audit/literal.py b/research/reversible-cnf-independent-audit/literal.py
new file mode 100644
index 0000000000..4b66c3b0cc
--- /dev/null
+++ b/research/reversible-cnf-independent-audit/literal.py
@@ -0,0 +1,221 @@
+"""Literal rational endpoint checks for the restricted five-role CNF reduction.
+
+Hiroki KUMAZAKI with substantial OpenAI Codex assistance. Apache-2.0.
+
+Independent implementation: no predecessor compiler, evaluator, phase helper,
+or arithmetic implementation is imported.  This interpreter accepts real
+identity-affine diagonal signs, not the general native affine/quadratic
+language.  A separate strict check verifies the compiler's coordinate Z
+alphabet.  Every matrix column is an independent dirty input.
+"""
+
+from fractions import Fraction
+import re
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def rational(value):
+    """Parse exact real coefficients; never silently round a JSON float."""
+    if type(value) is int or isinstance(value, Fraction):
+        return Fraction(value)
+    if isinstance(value, str) and re.fullmatch(r"[+-]?[0-9]+(?:/[+-]?[0-9]+)?", value):
+        try:
+            return Fraction(value)
+        except (ValueError, ZeroDivisionError) as error:
+            raise ValueError("invalid rational coefficient") from error
+    raise ValueError("explicit rational coefficient required")
+
+
+def permutation_matrix(images):
+    """Images encode destination(image[source]); columns are source inputs."""
+    need(isinstance(images, (list, tuple)) and len(images) == 5,
+         "five permutation images required")
+    need(all(type(value) is int for value in images) and sorted(images) == list(range(5)),
+         "permutation images must be exactly 0..4")
+    result = [[Fraction(0) for _ in range(5)] for _ in range(5)]
+    for source, destination in enumerate(images):
+        result[destination][source] = Fraction(1)
+    return result
+
+
+def _signs(problem, addresses):
+    n = problem["axes"]
+    need(type(n) is int and n >= 1, "positive integral axis count")
+    need(isinstance(addresses, (tuple, list)) and len(addresses) >= 1,
+         "positive-width tensor address tuple required")
+    need(all(type(address) is int and 0 <= address < 2**n for address in addresses),
+         "tensor address outside the declared axes")
+    generators = problem["generators"]
+    need(isinstance(generators, dict), "native generator dictionary required")
+    recipe_fields = {"matrix_rows", "offset", "phase", "linear_Z4", "quadratic_rows"}
+    result = {}
+    for name, recipe in generators.items():
+        need(isinstance(name, str) and bool(name), "opaque generator name")
+        need(isinstance(recipe, dict) and set(recipe) == recipe_fields,
+             "exact native recipe fields required")
+        for field in ("matrix_rows", "linear_Z4", "quadratic_rows"):
+            need(isinstance(recipe[field], list) and len(recipe[field]) == n
+                 and all(type(value) is int for value in recipe[field]),
+                 "integral native recipe dimension")
+        need(recipe["matrix_rows"] == [2**i for i in range(n)]
+             and type(recipe["offset"]) is int and recipe["offset"] == 0,
+             "diagonal sign generator must have the identity affine map")
+        need(type(recipe["phase"]) is int and recipe["phase"] in (0, 2),
+             "real diagonal sign requires an even constant phase")
+        need(recipe["quadratic_rows"] == [0] * n,
+             "CNF generator must have zero quadratic phase")
+        linear = recipe["linear_Z4"]
+        need(all(value in (0, 2) for value in linear),
+             "real diagonal sign requires even linear phases")
+
+        # Evaluate the recipe on each literal address.  Neither the generator
+        # name nor a claimed Boolean variable index is used to choose the sign.
+        exponent = 0
+        for address in addresses:
+            bits = [(address // (2**i)) % 2 for i in range(n)]
+            phase = recipe["phase"] + sum(linear[i] * bits[i] for i in range(n))
+            for i in range(n):
+                for j in range(i + 1, n):
+                    phase += 2 * bits[i] * bits[j] * ((recipe["quadratic_rows"][i] // (2**j)) % 2)
+            exponent += phase
+        exponent %= 4
+        need(exponent in (0, 2), "non-real native sign outside this interpreter")
+        result[name] = Fraction(1 if exponent == 0 else -1)
+    return result
+
+
+def strict_standard_generators(problem):
+    """Verify the unmutated compiler emits every primitive coordinate Z once.
+
+    Generator names remain opaque.  This is deliberately separate from the
+    endpoint interpreter, which also evaluates constant or multiplied signs
+    so a changed recipe can produce a literal incorrect endpoint.
+    """
+    need(isinstance(problem, dict) and {"axes", "generators"} <= set(problem),
+         "standard-generator problem fields")
+    _signs(problem, (0,))
+    n = problem["axes"]
+    need(len(problem["generators"]) == n, "one standard generator per axis")
+    represented_axes = []
+    for recipe in problem["generators"].values():
+        need(recipe["phase"] == 0, "standard Z has zero constant phase")
+        linear = recipe["linear_Z4"]
+        need(linear.count(2) == 1, "standard Z has exactly one nonzero linear phase")
+        represented_axes.append(linear.index(2))
+    need(sorted(represented_axes) == list(range(n)), "standard Z recipes cover every axis once")
+    return True
+
+
+def endpoint(problem, tuple_of_addresses):
+    """Return the complete five-by-five dirty endpoint on one tensor address.
+
+    Reference instructions are not subtracted: callers can evaluate them by
+    copying the problem and placing its reference list in the program field.
+    Accepted diagonal generators preserve every address, so distinct tensor
+    addresses form independent invariant blocks of the complete operator.
+    """
+    need(isinstance(problem, dict)
+         and set(problem) == {"axes", "roles", "generators", "program", "reference"},
+         "exact reduction problem fields required")
+    need(type(problem["roles"]) is int and problem["roles"] == 5, "exactly five dirty roles")
+    need(isinstance(problem["program"], list) and isinstance(problem["reference"], list),
+         "program and reference instruction lists required")
+    signs = _signs(problem, tuple_of_addresses)
+    matrix = permutation_matrix((0, 1, 2, 3, 4))
+    for instruction in problem["program"]:
+        need(isinstance(instruction, dict), "instruction object required")
+        op = instruction.get("op")
+        if op == "apply":
+            need(set(instruction) == {"op", "dst", "generator"}, "unary apply fields")
+        elif op == "swap":
+            need(set(instruction) == {"op", "src", "dst"}, "swap fields")
+        elif op in ("add", "query"):
+            required = {"op", "src", "dst"} | ({"generator"} if op == "query" else set())
+            need(required <= set(instruction) <= required | {"coefficient"},
+                 "additive instruction fields")
+        else:
+            raise ValueError("operation outside the reversible CNF alphabet")
+        dst = instruction["dst"]
+        need(type(dst) is int and 0 <= dst < 5, "destination role extent")
+        if op != "apply":
+            src = instruction["src"]
+            need(type(src) is int and 0 <= src < 5 and src != dst,
+                 "binary instruction requires distinct roles")
+        if op in ("query", "apply"):
+            name = instruction["generator"]
+            need(isinstance(name, str) and name in signs, "unknown native generator")
+            sign = signs[name]
+        if op == "swap":
+            matrix[src], matrix[dst] = matrix[dst], matrix[src]
+        elif op == "apply":
+            matrix[dst] = [sign * value for value in matrix[dst]]
+        else:
+            coefficient = rational(instruction.get("coefficient", 1))
+            if op == "query":
+                coefficient *= sign
+            matrix[dst] = [destination + coefficient * source
+                           for destination, source in zip(matrix[dst], matrix[src])]
+    return matrix
+
+
+def direct_clauses(clauses, assignment):
+    """Ordinary CNF truth evaluation on the bits of a nonnegative integer."""
+    need(type(assignment) is int and assignment >= 0, "nonnegative Boolean assignment")
+    need(isinstance(clauses, (list, tuple)), "clause sequence required")
+    answer = True
+    for clause in clauses:
+        need(isinstance(clause, (list, tuple)) and len(clause) <= 3,
+             "at most three literals per clause")
+        satisfied = False
+        for literal in clause:
+            need(type(literal) is int and literal != 0, "nonzero integral literal")
+            bit = bool((assignment // (2 ** (abs(literal) - 1))) % 2)
+            satisfied = satisfied or (bit if literal > 0 else not bit)
+        answer = answer and satisfied
+    return answer
+
+
+def run_local_controls():
+    """Finite complete-input controlled-swap checks, separate from CNF tests."""
+    recipe = {"matrix_rows": [1], "offset": 0, "phase": 0,
+              "linear_Z4": [2], "quadratic_rows": [0]}
+    # Opaque name deliberately disagrees with the source's Z1 spelling.
+    generator = "literal-phase-recipe"
+    tuples = ((0,), (1,), (1, 1), (0, 1), (1, 1, 1), (1, 0, 1))
+    cases = 0
+    for i in range(5):
+        for j in range(5):
+            if i == j:
+                continue
+            program = [{"op": "add", "src": j, "dst": i, "coefficient": -1},
+                       {"op": "add", "src": i, "dst": j, "coefficient": "1/2"},
+                       {"op": "query", "src": i, "dst": j, "generator": generator,
+                        "coefficient": "-1/2"},
+                       {"op": "apply", "dst": i, "generator": generator},
+                       {"op": "add", "src": j, "dst": i}]
+            problem = {"axes": 1, "roles": 5, "generators": {generator: recipe},
+                       "program": program, "reference": []}
+            strict_standard_generators(problem)
+            for addresses in tuples:
+                images = list(range(5))
+                if sum(addresses) % 2:
+                    images[i], images[j] = images[j], images[i]
+                need(endpoint(problem, addresses) == permutation_matrix(images),
+                     "complete dirty controlled swap endpoint")
+                cases += 1
+    need(direct_clauses([], 0), "empty conjunction must be true")
+    need(not direct_clauses([[]], 0), "empty clause must be false")
+    need(all(direct_clauses([[1, -1]], x) for x in range(2)), "tautological clause")
+    need(not any(direct_clauses([[1], [-1]], x) for x in range(2)), "contradictory clauses")
+    return {"ordered_role_pairs": 20, "tensor_tuples_per_pair": len(tuples),
+            "complete_five_column_endpoints": cases, "tensor_widths": [1, 2, 3],
+            "opaque_generator_name_control": True, "Boolean_boundary_controls": 4}
+
+
+if __name__ == "__main__":
+    import json
+    print(json.dumps(run_local_controls(), sort_keys=True))
diff --git a/research/reversible-cnf-independent-audit/verify.py b/research/reversible-cnf-independent-audit/verify.py
new file mode 100644
index 0000000000..2e6759d755
--- /dev/null
+++ b/research/reversible-cnf-independent-audit/verify.py
@@ -0,0 +1,74 @@
+#!/usr/bin/env python3
+"""Source-bound independent reversible CNF audit. Apache-2.0.
+
+Hiroki KUMAZAKI with substantial OpenAI Codex assistance.
+"""
+import hashlib
+import importlib.util
+import json
+from pathlib import Path
+import sys
+
+PACKAGE = Path(__file__).resolve().parent
+ROOT = PACKAGE.parent.parent
+SOURCE = ROOT / 'research/native-tensor-cutoff'
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def module_from_source(name, path, text=None):
+    spec = importlib.util.spec_from_file_location(name, path)
+    module = importlib.util.module_from_spec(spec)
+    exec(compile(path.read_bytes() if text is None else text, str(path), 'exec'), module.__dict__)
+    return module
+
+
+def compiler(text=None):
+    # Execute the actual compiler with its actual exact.py dependency, without
+    # changing either source. Restore the import namespace immediately after.
+    old = sys.modules.get('exact')
+    try:
+        sys.modules['exact'] = module_from_source('exact', SOURCE / 'exact.py')
+        return module_from_source('reviewed_cnf', SOURCE / 'reversible_cnf.py', text)
+    finally:
+        if old is None:
+            sys.modules.pop('exact', None)
+        else:
+            sys.modules['exact'] = old
+
+
+def mutated_source(old, new):
+    text = (SOURCE / 'reversible_cnf.py').read_text()
+    need(text.count(old) == 1, 'unique mutation anchor required')
+    return compiler(text.replace(old, new))
+
+
+def calculate():
+    pins = json.loads((PACKAGE / 'SOURCES.json').read_text())
+    inputs = [row for row in pins['files'] if row['usage'] == 'input']
+    need(len(inputs) == 6, 'exact source-input closure')
+    for row in inputs:
+        need(hashlib.sha256((ROOT / row['path']).read_bytes()).hexdigest() == row['sha256'],
+             'source digest mismatch: ' + row['path'])
+    literal = module_from_source('independent_literal', PACKAGE / 'literal.py')
+    audit = module_from_source('independent_audit', PACKAGE / 'audit.py')
+    return {'status':'PASS_REVERSIBLE_CNF_INDEPENDENT_AUDIT',
+            'reviewed_source_head':'18354f41de4dc7bfda4692e814cf1d91a6d619ef',
+            'authenticated_inputs':len(inputs),
+            'checks':audit.run(compiler(), literal, mutated_source),
+            'source_compiler_executed':True, 'source_evaluator_or_verifier_used':False,
+            'new_hardness_theorem_or_kappa':False}
+
+
+def main():
+    result = calculate()
+    expected = json.loads((PACKAGE / 'RESULT.json').read_text())
+    need(result == expected, 'computed receipt differs from committed RESULT.json')
+    print(json.dumps(result, indent=2, sort_keys=True))
+
+
+if __name__ == '__main__':
+    main()