Tidy research workspace and separate current source proofs

docs/reference/VERIFICATION_CATALOGUE.md

@@ -255,10 +255,10 @@ without an extra native fixture.
 | Common-probe source and static diagonal repairs | [Proof home](../../research/depth/COUPLED_FINAL_ENCODER.md#common-probe-wide-source), [exact native fixtures](../../tests/test_common_probe_source.py) | All one-address native source columns, actual inverse and relative-fiber columns check phase and orientation. Two- and three-address singlet inputs check literal pulse phases, the complete echo and squared error two. All 2,048 three-address diagonal square entries and both single-wire spectral factors challenge the static-dressing proof; distinct T targets and ledgers are checked through six address bits. The covariance, paired-state and spectral statements are analytic with distinct hypotheses. These internal audits and finite checks supply no unrestricted depth bound or external review |
 | Relative-probe involution and changed lookup trials | [Proof home](../../research/depth/COUPLED_FINAL_ENCODER.md#relative-probe-involution-repair), [native repair fixtures](../../tests/test_relative_probe_repair.py), [asymmetric-fiber fixtures](../../tests/test_probe_asymmetric_trials.py) | Exact native phases, actual inverses, relative blocks, normalized witnesses and ledgers check the corrected source. Rational displacement tails challenge the diagonal-dressing theorem; the nonempty-Hadamard and specified cubic-phase witnesses test complete lookup. Three exact p=3 nonreal relative entries reject the stated asymmetric trials; small binary bases and degree restrictions challenge their analytic components. All-size theorems, finite failures and internal audits retain separate scopes; no external review or frontier improvement is asserted |
 | Broad four-path Bell acceptance | [Complete operator and ledger](../../research/depth/CORANK_FOURIER_BELL_SOURCE.md#four-path-bell-relative-phase), [exact multipath fixtures](../../tests/test_multipath_bell_source.py) | Literal controlled swaps and phases, actual inverses and signal acceptance check all one-cell logical columns at two arbitrary-helper assignments. Complete two-cell Grams and native Bell Pauli propagation challenge coherent normalization and orientation. The exact half Gram gap and shared-control native schedule are analytic; finite fixtures are internal evidence, not an asymptotic emitter or external review |
-| Affine/Fourier repair and exact monomial boundary | [Proof home](../../research/depth/COUPLED_FINAL_ENCODER.md#affine-fourier-complete-transition-gap), [exact fixtures](../../tests/test_affine_fourier_repair.py) | Both affine/Hadamard orders, arbitrary bank columns, a complete native coherent echo and its actual inverse, and distinct-target ledgers challenge the robust transition gap. A correlated X-basis cubic phase checks the broader pulse scope. Walsh/noise and rectangle identities test the exact-only monomial screen, including a nonlinear permutation that transports the target to parity but fails the remaining transition condition. The all-angle and exact-only statements have separate hypotheses; no unrestricted native-depth or fixed-accuracy monomial obstruction is asserted |
-| Two-Clifford mixer screen and rank-one exception | [Proof home](../../research/depth/COUPLED_FINAL_ENCODER.md#two-clifford-mixer-screen), [exact fixtures](../../tests/test_two_mixer_lookup_screen.py) | Every p=3 bank translation and Walsh coefficient, an actual Clifford-coset source, and common-affine parity slopes check the scoped diagonal-support theorem. All 256 bank columns and actual inverses check the genuine rank-one completion, whose middle is supplied only as a truth-table diagonal; degree checks expose its unpaid lookup phase. The bank-only, fixed-address theorem does not cover active extra work or arbitrary native mixing |
-| Rank-one phase / indicator equivalence | [Proof home](../../research/depth/COUPLED_FINAL_ENCODER.md#rank-one-indicator-equivalence), [exact fixtures](../../tests/test_rank_one_indicator_equivalence.py) | The literal four-T-band control core and its actual inverse are checked on every finite basis column. Complete forward reduction, arbitrary auxiliary row zero, address/work-moving gauge cancellation and native gate ledgers test both resource reductions. Oracle calls remain explicitly charged; these tests do not supply a shallow indicator compiler |
-| Interleaved Clifford projector Grams | [Proof home](../../research/depth/CORANK_FOURIER_BELL_SOURCE.md#interleaved-clifford-gram-rigidity), [exact fixtures](../../tests/test_clifford_projector_gram.py) | Exact accepted Grams and clean-X stabilizer elimination test quantized amplitudes, the one-clean boundary and the two-clean target. Binary elimination checks the degree-sensitive label formula. This supports a held-address affine-query limitation, not unrestricted native depth |
+| Affine/Fourier repair and exact monomial boundary | [Proof home](../../research/depth/BANK_MIXING_AND_LOOKUP_PHASE.md#affine-fourier-complete-transition-gap), [exact fixtures](../../tests/test_affine_fourier_repair.py) | Both affine/Hadamard orders, arbitrary bank columns, a complete native coherent echo and its actual inverse, and distinct-target ledgers challenge the robust transition gap. A correlated X-basis cubic phase checks the broader pulse scope. Walsh/noise and rectangle identities test the exact-only monomial screen, including a nonlinear permutation that transports the target to parity but fails the remaining transition condition. The all-angle and exact-only statements have separate hypotheses; no unrestricted native-depth or fixed-accuracy monomial obstruction is asserted |
+| Two-Clifford mixer screen and rank-one exception | [Proof home](../../research/depth/BANK_MIXING_AND_LOOKUP_PHASE.md#two-clifford-mixer-screen), [exact fixtures](../../tests/test_two_mixer_lookup_screen.py) | Every p=3 bank translation and Walsh coefficient, an actual Clifford-coset source, and common-affine parity slopes check the scoped diagonal-support theorem. All 256 bank columns and actual inverses check the genuine rank-one completion, whose middle is supplied only as a truth-table diagonal; degree checks expose its unpaid lookup phase. The bank-only, fixed-address theorem does not cover active extra work or arbitrary native mixing |
+| Rank-one phase / indicator equivalence | [Proof home](../../research/depth/BANK_MIXING_AND_LOOKUP_PHASE.md#rank-one-indicator-equivalence), [exact fixtures](../../tests/test_rank_one_indicator_equivalence.py) | The literal four-T-band control core and its actual inverse are checked on every finite basis column. Complete forward reduction, arbitrary auxiliary row zero, address/work-moving gauge cancellation and native gate ledgers test both resource reductions. Oracle calls remain explicitly charged; these tests do not supply a shallow indicator compiler |
+| Interleaved Clifford projector Grams | [Proof home](../../research/depth/CLIFFORD_PROJECTOR_GRAM.md#interleaved-clifford-gram-rigidity), [exact fixtures](../../tests/test_clifford_projector_gram.py) | Exact accepted Grams and clean-X stabilizer elimination test quantized amplitudes, the one-clean boundary and the two-clean target. Binary elimination checks the degree-sensitive label formula. This supports a held-address affine-query limitation, not unrestricted native depth |
 | Complete Bell-envelope transfer | [Proof home](../../research/depth/CORANK_FOURIER_BELL_SOURCE.md#bell-acceptance-charge-transfer), [exact fixtures](../../tests/test_bell_acceptance_transfer.py) | Literal paired Bell matrices retain all arbitrary data and auxiliary columns. A non-diagonal coherent auxiliary effect tests the exact whole-space residual, and distinct-address comparisons test the sharp quarter floor. Uniform coset vectors check the separate phase-free permutation screen. These analytic reductions supply no new source or frontier bound |
 | Coupled final encoders and bank dependence | [Proof home](../../research/depth/COUPLED_FINAL_ENCODER.md), [exact native fixtures](../../tests/test_coupled_final_encoder.py) | Complete two-address coefficient-bank and three-address cubic-sign matrices check the hybrid-address kernel on every dirty-tag input and its actual inverse. Bounded full-bank fixtures check the syndrome rewrite, literal inverse, Fourier/Pauli expansion columns and native ledgers. The bank-fiber rank theorem and the separate rotated-bank centralizer obstruction are analytic, including arbitrary middle Clifford boundaries and identity helpers. These encoders are components, not qualifying sources or unrestricted depth lower bounds |
 | Boolean spectral reflection sources | [Proof home](../../research/depth/BOOLEAN_REFLECTION_GRAM_SOURCE.md), [six exact fixtures](../../tests/test_boolean_reflection_gram_source.py) | Native eight-point Fourier transform and actual reverse on every dirty column; spectral truth-table compute/uncompute; literal controlled quarter-phase echo; complete accepted normal form; high-bit and parity p=1 sources; and a commuting-reflection success fixture. Exact spectral evaluation, bounded-clean removal, simultaneous source costs, robust reflection-product criterion and the all-size flat-mixer gap one quarter are analytic. The changed source matches normalized trace but fails complete lookup sectors; finite checks and internal audits are not external mathematical review |

research/README.md

@@ -186,6 +186,7 @@ These are complete interfaces and conditional transfers, not constructions of th
 - [Clean-sector parallelism: what the native schedule actually buys](depth/CLEAN_SECTOR_PARALLELISM_AUDIT.md)
 - [Dirty-tree compilation from complete branch differences](depth/DIRTY_TREE_DIFFERENTIAL_RECURRENCE.md)
 - [Which incomplete indicator interfaces still contain the full operation](depth/WEAKER_INDICATOR_INTERFACES.md)
+- [Bank mixing and the complete lookup phase](depth/BANK_MIXING_AND_LOOKUP_PHASE.md) — scoped mixing screens and the rank-one phase/indicator resource equivalence, including arbitrary address/work motion within the derivative gauge
 - [Table-specific probes and the remaining joint-word freedom](depth/TABLE_SPECIFIC_INDICATOR_INTERFACES.md)
 - [Joint bank routing and the complete dirty indicator](depth/JOINT_ROUTING_INDICATOR_INTERFACES.md)
 
@@ -236,15 +237,16 @@ Use these only with their stated actual-boundary, fiber, normalization or source
 - [Bank-coupled selector dynamics](depth/BANK_COUPLED_SELECTOR_DYNAMICS.md) — paid bank swaps/Hadamards and their signal controls, complete principal-work dynamics, an all-size Bell-cell witness for the specified nonlocal frames, and a finite bank-Hadamard source excluded by its complete marked path Gram
 - [MOD3 zeta transport](depth/MOD3_ZETA_TRANSPORT.md) — binary order-three blocks, paid native baselines and shared cleanup, a native two-band exclusion, and exactness of three-layer observable approximation below the fixed gap; sublogarithmic joint transport remains unpaid
 - [Weak Pauli orbit compression](depth/WEAK_PAULI_ORBIT_COMPRESSION.md) — native single-coordinate and joint two-coordinate sources, complete two-address lookup, four-band nested coefficients, [two-band coefficient shear and complete assembly](depth/WEAK_PAULI_ORBIT_COMPRESSION.md#complete-coefficient-shear) with a paused linear-depth recurrence, and scoped product/prefix-rank/final-block limits
-- [Coupled final encoders](depth/COUPLED_FINAL_ENCODER.md) — paid address/tag and full-bank X-motion families with complete operators; scoped bank-fiber and rotated-bank centralizer obstructions to three-layer completion; [paid syndrome pulses and their thin-acceptance boundary](depth/COUPLED_FINAL_ENCODER.md#syndrome-star-pulse-boundaries); [normalized broad trial](depth/COUPLED_FINAL_ENCODER.md#broad-baseline-syndrome-source) with exact half Gram gap and a baseline-relative rank criterion; [shifted-syndrome commutator](depth/COUPLED_FINAL_ENCODER.md#shifted-syndrome-wide-commutator) with an actual four-band schedule, retained coefficient and an angle-independent missing-row obstruction; [common-probe sources](depth/COUPLED_FINAL_ENCODER.md#common-probe-wide-source) with a paid third frame, paired-state witness and an all-static-diagonal relative-spectrum boundary; [corrected relative block](depth/COUPLED_FINAL_ENCODER.md#relative-probe-involution-repair) with paid involution, complete transition tests and finite asymmetric-fiber trials; [affine/Fourier transitions](depth/COUPLED_FINAL_ENCODER.md#affine-fourier-complete-transition-gap) have an all-angle gap, while [two Clifford mixers](depth/COUPLED_FINAL_ENCODER.md#two-clifford-mixer-screen) retain a genuine rank-one exception with an unpaid lookup derivative; [complete phase/indicator reductions](depth/COUPLED_FINAL_ENCODER.md#rank-one-indicator-equivalence) prove resource equivalence, pay a four-band control bank and expose the full address/work-moving gauge freedom
+- [Coupled final encoders](depth/COUPLED_FINAL_ENCODER.md) — paid address/tag and bank-motion sources, scoped three-layer boundaries, the corrected relative involution, and complete-transition failures of retained repairs
 - [Coupled order interference](depth/COUPLED_ORDER_GRAM_SOURCE.md) — actual joint word, robust direct square readout for balanced two-unitary sources, paid anchors and two distinct finite failed bank-moving trials
 - [Affine orbit reflection source](depth/AFFINE_ORBIT_REFLECTION_SOURCE.md) — paid fixed-point-free charge-preserving motion and orbit coordinates, exact diagonal phase cochains, sharp phase-degree scope and a failed local anchor
 - [Transverse orbit reflections](depth/TRANSVERSE_ORBIT_REFLECTION_SOURCE.md) — arbitrary controlled-dressing normalization, a paid non-diagonal square-root trial and its all-size sector error; the affine orbit is a charge-preserving native change of coordinates
 - [Boolean reflection Gram sources](depth/BOOLEAN_REFLECTION_GRAM_SOURCE.md) — exact spectral Boolean queries without clean work, paid controlled quarter phases, full reflection-product Gram criterion and the flat-mixer sector obstruction
 - [A normalized scalar-kernel partial source](depth/SCALAR_KERNEL_FILTER_SOURCE.md) — correct-charge support, native/error ledger and fixed-diagonal rigidity; a paid rank-one determinant query still has a thin, wrong-sector scalar echo
-- [Corank-one Fourier kernels and Bell acceptance](depth/CORANK_FOURIER_BELL_SOURCE.md) — paid thin-projector source and two-reflection interference: complete p=1 success, all-larger-size common-kernel failure; a [broad four-path source](depth/CORANK_FOURIER_BELL_SOURCE.md#four-path-bell-relative-phase) pays two-clean normalization and controls but has exact half Gram gap; [general auxiliary acceptance](depth/CORANK_FOURIER_BELL_SOURCE.md#bell-acceptance-charge-transfer) inherits exactly the same complete charge-readout obligation, with a sharp quarter gap when address independent; [interleaved Clifford projector Grams](depth/CORANK_FOURIER_BELL_SOURCE.md#interleaved-clifford-gram-rigidity) give clean-signal rigidity and a two-clean affine-query requirement beyond the Bell factorization
+- [Corank-one Fourier kernels and Bell acceptance](depth/CORANK_FOURIER_BELL_SOURCE.md) — complete Bell dilation, normalized thin and broad sources, coherent-sector failures, and transfer of the complete charge-readout error to auxiliary acceptance
 - [Two complete key-mixing tests for observable transport](depth/KEY_MIXING_OBSERVABLE_SCREENS.md)
 - [Gaussian compression with a small clean signal](depth/GAUSSIAN_COMPRESSION_SOURCE_LIMITS.md)
+- [Clifford projector-Gram rigidity](depth/CLIFFORD_PROJECTOR_GRAM.md) — singular accepted Grams of fully interleaved Clifford fibers; clean-signal rigidity and a separate read-only affine-query count boundary
 - [Involutory Gaussian loops and their unsquared scalar limit](depth/INVOLUTORY_GAUSS_SOURCE_LIMITS.md)
 - [Scalar phases of closed Gaussian circuits have bounded degree](depth/GAUSSIAN_SCALAR_LOOP_OBSTRUCTION.md)
 - [Complete-input limits of two approximate equality filters](depth/APPROXIMATE_INDICATOR_FILTER_LIMITS.md)