Invented by Teerth Sharma · research record

resolvent

"The S-matrix is the unitary matrix connecting sets of asymptotically free particle states — the in-states and the out-states — with no account of the path between them."

Wheeler, 1937 (Phys. Rev. 52, 1107); Heisenberg carried it through the 1940s. The full reconciliation →

Softmax attention and Markov path composition are the same operator.

A family of attention operators in which softmax is one corner, read as a forward S-matrix through a resolvent — proved in Lean 4, matched bitwise in code, and every result that failed is kept on the record beside the ones that held. The physics framing is a reconciliation, not a result: it explains why the hop expansion converges, and adds no measurement.

Lean 4 v4.7.0 134 theorems + 41 lemmas sorry 0 corner tests 78/78 Apache-2.0

Read the experimentgithub.com/teerthsharma/resolvent

Represents order

S5, bare integers, matched params holds

0.8620 ± 0.0556 vs commuting-diagonal control 0.2860 ± 0.0150, 404 params, 5/5 seeds pairwise no overlap; control saturated within 0.031 of its ceiling 0.3110. Scope: one budget, one word length, no length-generalization check.

Does not predict

Repaired chess bed unmet

Resolution 0.001469 vs oracle ceiling 0.10117 (1.45%); tied by an 8-bin piece-count histogram of its own input; loses on Brier, 0.6334 vs 0.5020.

Gate closes, cause unknown

Every proposed mechanism refuted open

Gradient starvation, step-0 zero density, eval-only exactness, live-gradient unfreeze — all four refuted; the first two by the same table built to demonstrate them, the other two by pre-registered kills. Twelve checks that could not fail are catalogued alongside them.

Each gate passes a fraction of what crosses it, so the weight from t₈ to t_j is the product of the gates between them — G_ij = ∏_k=j+1..i m_k. This demo runs the real magnitude gate only, with no complex phase anywhere in it (the full operator also carries an e^iθ_k term, shown in the cube below, §3). Closing one gate sends every path across it to zero exactly, not approximately.
A prefix scan in the logit cannot do this: it contributes e^C_i−C_j, and that is never zero. Lean theorem no_prefix_scan_represents_a_zero_gate.

━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
 resolvent · measured 2026-09-11 · Windows 11 · Python 3.11.9 · torch 2.14.0 (CPU)
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
 Lean 4 proofs          13 files · 134 theorems + 41 lemmas · 0 sorry · build exit 0
 Corners in code        78 / 78 tests pass            tests/arm_smprime, tests/arm_pl
 Softmax corner         max |Δ| vs causal softmax     0.000e+00
 Committor closed form  max |Δ|                       4.441e-16
 Curl vs node models    share left unrepresented      mixed 0.6720 · pure curl 1.0000
 Planted negative       pure-gradient target          6.5e-16
 Refusal                sensitivity · specificity     100.00% · 100.00%  (138 + 262)
 Prediction             beats a trivial baseline      not yet — open
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━

Abstract

This is a research programme with one target: an attention mechanism that understands consequences — where a process ends up after an action, not only which token comes next — while standing as an equal to self-attention. Its object is a single causal head whose three switches span softmax attention, unnormalized-kernel attention and the exact path product of a Markov chain; the containments are proved in Lean 4 and matched bitwise in float64. On that head sit two reads: a resolvent read that answers where a process ends up with one triangular solve, and refuses when a counterfactual has no defined answer, and a graded read that sees edge flows with curl, which no node-level model can represent at any size.

The exact machinery holds. The learned side has not yet earned a win: over its first 387 commits (2026-08-25 to 2026-09-19), every matched comparison on prediction ended in a tie or a loss, and each is published beside the number that decided it. In the repository's own words, the family is strictly more reachable, not yet more accurate.

The sections below build the two mechanisms from their definitions before joining them, so the operator, the reads and the scoreboard can be read without prior acquaintance with attention or with Markov chains.

Keywords: causal attention · softmax attention · path products · resolvent · committor functions · Hodge decomposition · selective prediction · pre-registration · formal verification · Lean 4

1The experiment

Transformer attention mixes information across positions. Recurrences and Markov chains pass values along paths. The experiment asks whether one attention head can do both — and whether the path-following half gives a model something softmax attention lacks: reasoning about the consequences of an intervention.

query position

Drag the query slider; the row redraws. Attention is one row of weights over the past, and nothing more.

β divisor

row sum

Move β from 0 to 1; the divisor shrinks every weight by the same factor. Softmax's normalization is a setting, not a law — this is the single most important idea on the page (illustrative values).

The object. One causal head, W_ij = G_ij · exp(qk · q_i·k_j) ⁄ Z_i^β, with three switches: β (normalizer on or off), g (a multiplicative gate whose path product can close exactly) and qk (content comparison on or off). Three settings of those switches are three known operators, and that is a theorem rather than an analogy (§3).

The reads. Treat the causal attention matrix as a Markov chain, make declared boundary rows absorbing, and solve one triangular system: the answer is the committor, the probability that each position ends in each boundary set. When a counterfactual has no defined answer, the read refuses instead of returning a number. A second read covers edge flows with curl (§4).

What is owned by prior work. The resolvent read over attention is ChaCAL's (Fagnou et al., EMNLP 2024). The delta this repository claims is the absorbing boundary rows for K constraint sets, the committor read, the interventional re-solve, the certificate and the Lean proofs — stated in the shape paper and the charter rather than left for a reviewer to find.

The method is adversarial bookkeeping. Predictions are filed with counter-predictions before any run, kill thresholds are frozen, every check carries a planted negative that must fail, and when a kill fires the result is published. The error record holds 74 failure mechanisms, 12 withdrawn constants and a retraction log (§6). The two applications the author names are chess and prediction-market trades.

The north star, and where it stands

The goal as the author states it has three conditions, all required: an attention mechanism that understands causality and consequences, predicts better than anything before it on a named task against a named opponent, and carries the weight of self-attention or JEPA. The repository's sentence of record says the same thing in engineering terms:

"Attention EQUAL to self-attention on its own ground, built FROM softmax and AdamW, capable on ground they cannot occupy — predicting the NEXT STATE toward equilibrium, not the next token."
CEQ_V20_R15_CONTRACT.md:52-55

Condition 1

Understands causality and consequences partial

Holds when the operator is given. The committor is exact to 4.441e-16; refusal scores 100% / 100% on 138 + 262 cases; on 13,479 human K+Q-vs-K positions the exact committor separates consequence swaps from meaning-preserving ones at a ratio of 2.501651.

Not yet learned. The trained read's ratio is 0.999745, below the planted negative's 1.073511. A trained operator head emitted κ 1.34 against a true 93.51, and the OOD-κ claim died on 5/5 seeds.

Condition 2

Predicts better than anything before it unmet

Every matched race is a tie or a loss. On a Kaggle T4 over 115,628 Lichess games, a zero-parameter heuristic matched human moves at 0.3401 [0.3321, 0.3482]; the trained model reached 0.2882 [0.2806, 0.2959].

Against a matched softmax head the gate ties, at 1.91–2.84× the cost. The one narrow gain: a free β lowers held-out log-loss by 0.046–0.063 nats with no change in exact accuracy.

Condition 3

Carries the weight of self-attention or JEPA partial

Parity by containment is earned. The β = 1 corner is softmax to 0.000e+00, and containment survives training (Δ exact +0.00000 at 3 seeds).

Standing is not. The largest run is one T4, no fused kernel exists, the family runs at 1.17–2.84× softmax wall clock, and the JEPA target moved with its encoder by 4.1101× on the synthetic bed and 136.7950× on Kaggle.

2The two mechanisms this joins

Attention and Markov chains are usually taught in different courses and built into different architectures. Both are matrices over the same positions, and the whole programme rests on what each one does with that matrix. This section states both from their definitions.

2.1 What attention computes

A sequence arrives as n positions. Every position i produces three vectors by multiplying its own representation by learned matrices: a query q_i, a key k_i and a value v_i. The query asks; the key advertises; the value is what gets carried if the two match.

score

The dot product q_i·k_j, one number per ordered pair, large when position i's question matches position j's advertisement.

softmax

Exponentiate every score in row i and divide by their sum Z_i. The row becomes positive numbers that add to one — a probability distribution over the positions row i may read.

causal mask

Delete every entry with j > i, so no position reads its own future. The weight matrix is lower triangular.

the output

Row i of the weight matrix times the values: a weighted average of everything position i is allowed to see.

Two properties of that construction matter for everything below. First, the weights are computed per pair, from content alone: the weight from i to j does not depend on what lies between them. Second, each row is normalized across positions, so attention answers "how should this position divide its attention among the others" — a question about proportions, asked once. One layer takes one hop. Depth is what lets information travel further, and each extra hop costs another full layer.

2.2 What a Markov chain computes

A Markov chain is a set of states and a matrix P in which P_ij is the probability of stepping from state i to state j. Rows sum to one for the same reason attention rows do: from any state, the process goes somewhere.

path product

The probability of following one particular route is the product of the entries along it. Probabilities multiply along a path where attention weights do not.

absorbing state

A state that, once entered, is never left. Declaring some states absorbing turns "what happens next" into "where does this end".

transient block

The sub-matrix Q of steps among the states that are not absorbing; R holds the steps from those into the absorbing ones.

committor

For each starting state, the probability of ending in one declared outcome rather than another. It answers "which outcome is reached first", not "what is the next step".

resolvent

The matrix (I − Q)⁻¹ = I + Q + Q² + … , the sum over paths of every length. One inverse carries every number of hops at once.

That last line is the reason a chain is worth putting inside attention. A stack of L attention layers composes L hops and stops; the resolvent composes all of them in closed form. In the causal setting the sum is not even infinite: when steps may only go backwards in position, Q is strictly lower triangular, its powers vanish after n terms, and the inverse is obtained exactly by one pass of forward substitution — no iteration, no truncation, no convergence criterion.

Left, the attention output x + Px: one hop, weights read straight off the pair. Right, the resolvent read (I − gP)⁻¹x: the same matrix, summed over every route, with the weight of a route the product of its steps.

2.3 Where the two meet

A causal softmax weight matrix is non-negative and its rows sum to one. That is precisely the definition of a transition matrix, so reading a head's weights as a chain over positions is not a metaphor — it is the same object under a different question. The difference lies in what is done with it. Attention multiplies by it once. A chain inverts I − gP and gets every path at once. The normalizer sums across positions; the gate multiplies along a path. Sum and product, one matrix.

That observation only becomes an architecture if both sides are reachable by the same layer, under settings a gradient can move. The rest of this page is about the head where they are, the two questions it can then be asked, and the record of what that has and has not bought.

3The operator: one head, three switches

ceq/arm_smprime.py implements a single causal head in which both mechanisms of §2 are settings of the same three parameters.

W_ij =G_ij · exp(qk · q_i·k_j) ⁄ Z_i^βj ≤ i, and 0 above the diagonal

G_ij =∏_{k = j+1 … i} m_k · e^iθ_kthe gate's path product, m_k ∈ [0, 1]

Z_i =Σ_{j ≤ i} |G_ij| · exp(qk · q_i·k_j)the row normalizer

Read the first line as three independent decisions. The exponential of the score is ordinary attention content. G_ij is the chain half: a product over the gates lying between j and i, exactly the path product of §2.2. The denominator is the softmax normalizer, and the exponent β decides how much of it applies.

The three switches as the axes of a cube. The named operators are two corners and one edge of it, and all three settings are live trainable parameters on the shipped module — but a trainable axis is not the same as one that buys something. The gate axis’s complex-phase part is real and trains, and it is also gauge-trivial on every bed this page shows: the read graph is a path, so its first Betti number is 0, a tree gauge removes the phase to 9.602627e-15, and paying for it at all costs 2.61x against a real signed gate that reproduces the same gated product to 1.347111e-15. The separation this axis exists for needs a genuine cycle, which no bed on this page has. Lean: three_corners_containment, corners_are_distinct.

What each switch decides

switch	off	on	what it decides
qk	W ignores content	dot-product logits	Whether positions are compared at all. With qk off the head is pure structure: the weights come from the gates alone, and the content path is gone.
g	G ≡ 1	path product ∏ mk eiθk	Whether values compose along a path. With the gate off, every pair is read directly; with it on, the weight of a pair is the product of everything between them.
β	β = 0, no normalizer	β = 1, rows sum to 1	Whether the read is a mean or a total. The read carries N1−β in the token count, so β = 1 is intensive — an average, insensitive to how many positions were summed — and β = 0 is extensive, a total that grows with them.

Why an exact zero is the whole point of the gate

Decay is usually added to attention inside the logit: a term is subtracted before the exponential, so the contribution of a distant pair becomes e^C_i−C_j. Whatever the prefix scan C contains, that quantity is the exponential of a finite number, and an exponential is never zero. Such a gate can make a path arbitrarily small; it cannot make it absent.

A product of magnitudes can. One factor at zero sends the whole product to zero, and every path crossing that gate with it — the behaviour the figure at the top of this page demonstrates, and the content of the Lean theorem no_prefix_scan_represents_a_zero_gate. The distinction is not numerical fastidiousness. "This path does not exist" is a statement a causal model has to be able to make: a blocked route, an intervention that removes an edge, a constraint that forbids a transition. A model whose gates only ever approach zero can represent none of them exactly.

The β = 0 corner is not O(n) "linear attention". It is the unnormalized exponential kernel exp(q·k), which has no finite feature map: at fixed dk = 8 the numerical rank of the score matrix reads 8, 16, 32, 63, 126, 252 for n = 8 … 256, tracking n instead of saturating. Setting β = 0 removes the division by Z and nothing else, so the corner costs what softmax costs. An earlier README called it linear attention; the Lean definition never did.

Every corner is a theorem, and every theorem has a test

Lean theorem	what it proves
three_corners_containment	one family (β, g, qk) contains all three operators; the softmax corner matches the corpus's own softmaxAttn to 0.000e+00, and ceq/lm.py's attention to 1.110223e-16 — half an ulp — on 19 of 64 entries. It has not been read against a fused kernel
corners_are_distinct	the corners are different operators: at (i, j) = (1, 0) with gate and qk off, β = 1 reads 1/2 and β = 0 reads 1
gate_zero_beta_zero_is_linear_attention	with the gate off, β alone decides softmax-class membership
no_prefix_scan_represents_a_zero_gate	eCi−Cj is never zero, so no prefix scan represents a closed gate; the path product does
Asink_computes_chain	a causal softmax head reproduces a chain's label exactly, for every gate with ak ≠ 1

The theorems live in lean/CEQ/ — 13 files, 134 theorems and 41 lemmas, zero sorry. Each one has a float64 counterpart in ceq/arm_smprime.py or ceq/arm_pl.py that is checked against the statement bitwise at the corners, because a proof about a definition says nothing about the code unless the code is held to it.

4The reads: where a process ends up, and what nodes cannot see

The head is an operator. The two reads turn it into answers to questions attention is not usually asked.

4.1 The resolvent read — one triangular solve

ceqjepa/operator.py builds a causal row-stochastic softmax matrix P, declares some rows absorbing, and solves. Making a row absorbing means replacing it with a row that keeps all its probability on itself: the process, on arriving there, stops. Choosing which rows to absorb is how a question is posed — the absorbing rows are the outcomes whose competition the read is about.

to A

Click a starting state; the read shows the probability of ending in A rather than B. The resolvent answers where a process ends up, which is the question the whole project is about (illustrative values).

state readz = (I − gP)⁻¹ Ṽ

committorq = (I − Q)⁻¹ Rprobability of ending in each boundary state

The committor line is the whole causal claim in one equation. Q holds the steps among ordinary positions and R the steps into the declared outcomes; the inverse sums over every route of every length; the product with R collects, for each starting position, the probability that it reaches each outcome first. Because the causal mask makes Q strictly lower triangular, this is not an approximation and not an iteration — a single forward substitution returns it, and the published self-check matches the closed form to 4.441e-16, at the float64 floor. With teleport = 0 the same operator matches causal softmax to 0.000e+00: the read adds a question without changing the attention it is asked about.

Refusal as an output

a

Move the slider for a; where the line and curve meet, c = eᵃᶜ has a solution. A solution stops existing — it does not get worse, it stops (illustrative curve, redrawn per a).

A counterfactual can be meaningless rather than merely uncertain. If the state a question asks about cannot be reached at all, there is no distribution to report, and a model that answers anyway is guessing with a confident face. The read separates the two cases in the solve itself: a singular transient block raises SingularTransientBlockError rather than returning a number, and a non-finite logit raises ValueError rather than letting NaN spread into q. Every counterfactual then receives one of three verdicts — UNDEFINED, refused with its reason; NULL, answered with an exact zero; DEFINED, answered.

Scoring a refusal rule needs the two trivial rules beside it, because each of them scores perfectly on one axis alone:

rule	sensitivity	specificity
resolvent (reachability)	100.00%	100.00%
refuse everything	100.00%	0.00%
answer everything	0.00%	100.00%

138 undefined and 262 defined cases, scored against an independent reachability oracle: python -m ceqjepa.dr1.

4.2 The graded read — edge flows with curl

Most models attach numbers to things: a value per node, a state per position. Relations then have to be inferred from the things — an edge is read as the difference between its endpoints. That works for any quantity which is such a difference, and fails completely for one that is not.

grade 0

A number per node. Attention states, embeddings and node features live here.

grade 1

A number per edge, with direction: a flow, a rate, a transfer from one node to another.

grade 2

A number per triangle: how much the flow circulates around a closed three-cycle.

gradient part

The edge flows that are differences of node values, written im(d₀).

curl part

The flows that circulate, im(d₁^⊤): around a triangle they sum to something non-zero, so no assignment of node values produces them.

harmonic part

What is left, ker(L₁): neither a difference nor a circulation, and determined by the shape of the graph — its holes.

The Hodge decomposition states that every edge flow is exactly one sum of those three pieces, R^E = im(d₀) ⊕ im(d₁^⊤) ⊕ ker(L₁), and the pieces are orthogonal. A node-level model lives in the first one. Whatever its width, depth or budget, the curl part of a target is outside its range — not hard for it, unreachable. ceqjepa/dr1.py measures that boundary as the least-squares optimum over the entire node-level class, so the number is not about one trained network that could have been trained better:

pure gradient (planted negative)6.5e-16 mixed0.6720 pure curl1.0000

Share of each target that no node-level model can represent, on a 9-node, 16-edge, 8-triangle complex. The first row is the planted negative: a target built to be a pure gradient must read zero, and does, which is what makes the other two rows evidence rather than arithmetic.

Traffic that circulates around a loop, a market where value flows in a cycle, citations that come back around: these are grade-1 objects with curl, and a graded read is what puts them inside the range of the model instead of outside it. Taking that read to real relational data is the open research direction the README names.

5How it is going

Nine phases, grouped from the commit log. Each ends on the number that decided it. A hollow amber marker is a claim that died; a green one is something that was built and still stands.

1. 2026-08-25 → 08-26 · 66 commits · dfc1591 → 33cb36a

   A signed operator that did not work

   A signed, strictly causal, denominator-free multi-hop path sum, with hops routed through content-selected pivots. The pre-registered kill fired on the shipped operator. The headlines that had said otherwise — a flat slope, a 61× separation — measured an operator the shipped path never called.

   sign-flip slope −1.298 against a bar of −0.3
2. 2026-08-26 · 72 commits · 8ba52e1 → 74e5590

   Certificates, and the finding that nothing had been decided

   Hilbert-metric contraction certificates died three ways, the measured diameter running 11–33× its prediction. The larger finding: the deciding measurement had been taken zero times, because every oracle was a closed-form function of its input, and every task asked for one scalar at one position — where one attention layer is provably optimal. The project reversed course and chose to build on softmax, not against it.

   37% of the way to the deliverable: engineering near 80%, the central claim near 5%
3. 2026-08-30 → 08-31 · 143 commits · 977f715 → ecbedf7

   The planet rounds hit a data-budget wall

   On the C1 vector corpus the first creditable contrast went against the family: at t* = 2 softmax read 0.996745 against 0.999082 and 1.000150 for the two CEQ arms. At t* = 32 every arm sat at or above predict-the-mean — and round 10 showed the wall was data, not architecture, by predicting where softmax becomes learnable before measuring it.

   predicted n* = 48,823, landed within 0.7%
4. 2026-08-31 → 09-01 · 61 commits · 9082e99 → 207e7b9

   Lean enters: parity refuted, the corners proved

   The contract said a zero gate gives bitwise standard attention. Lean refuted it — gate_zero_not_stochastic, row i sums to i+1 — and the repair became three_corners_containment, with β as the switch that decides softmax membership. The R1 deciding cell did not cross its floor.

   R1 0.829151, CI [0.617075, 1.041227] against a floor of 0.7071
5. 2026-09-04 → 09-06 · 4 commits · aa38e11 → 527ffca

   The shape paper, the declutter, the canon

   Round 15 earned 2 of a possible 44 scoreboard points. The shape paper conceded that the resolvent read is ChaCAL's and that no CEQ arm had yet been trained. Fifteen rounds of process documents left the tree, and the canon was written: eight books of verses, each carrying its own kill and a pre-derived replacement.

   350 files and 159,507 lines removed · 188 verses
6. 2026-09-11 → 09-13 · 5 commits · e238db6 → c9a9434

   Pre-registration on real data, and the public release

   REMOVAL-ECHO was registered before any data was downloaded. On Perturb-seq, 118 of 131 gene pairs were non-additive and the prediction held; on NBA injuries the counter-prediction held instead. The README was rewritten around the resolvent family and the repository went public on 2026-09-13.

   D1 0.9008 [0.8376, 0.9411] held · D2 0.979 counter held (commit 6aef750)
7. 2026-09-13 → 09-14 · 11 commits · e3d56cb → b5190d4

   A GPU run, and a heuristic that won

   A rule assigned each latent coordinate its own attention corner, β = 1 − α, and a π-JEPA encoder was trained through it on a Kaggle T4 over 115,628 Lichess games. A zero-parameter box-shrinking heuristic beat it. The rule was retired on three grounds, and the component ledger was born: every future run carries a frozen-random arm and a trivial baseline.

   heuristic 0.3401 against model 0.2882, disjoint intervals
8. 2026-09-14 · 23 commits · 468bc85 → 88a7388

   Component rounds: every lead met its counter

   The gate ties softmax at 1.91–2.84× the cost. An encoder change closed 91.7161% of the committor gap. The consequence-swap headline's zero was an identity of the definition. The depth ladder turned out to measure optimiser steps, not depth. On BED-H a GRU abstaining on its own entropy matched the read's refusal. One lead survived: an estimated operator becomes solvable once whitened, 0.030243 against 0.348321 (commit 82eb2d4; no tracked file prints the Hebbian figure).

   2-layer stack 0.0555 → 0.3005 from optimiser steps alone · GRU recall 0.8959
9. 2026-09-19 · 2 commits · 60bdcc9 → 2e09d51

   Issue closeouts

   The logit-Nash stance was retired over five seeds, including with both of its known defects repaired; one of those defects was a learned parameter no code ever read. The SPRT became torch-free.

   nash 5.2888 ± 0.6041 against signed 2.7333 ± 1.0235, 0/5 seeds
10. 2026-09-20 · ceq/arm_smprime.py

    The gate-kill NaN is fixed

    Closing a gate zeroes every block before it in the merge, exactly, not approximately. A live diagonal entry that overflows gives an honest infinity instead, not a zero (illustrative values). 173 nan became inf, the nan count went from 173 to 0, and the non-finite count held at exactly 339.

    The dead set is now masked before the complex multiply. The dead-shift bed returns [(1+0j), (1.5+0j), (3+0j)], bitwise equal to the block summary, where dense attention had returned (nan+nanj); the live-diagonal artifact inf+nan*j became inf+0j. tests/arm_smprime/ reads 61 passed.

    173 nan became inf; the nan count went 173 to 0, non-finite count held at exactly 339
11. 2026-09-20 · tests/cameron/test_third_collapse_leg.py

    The detector inversion: the encoder that learned nothing reads healthier

    Effective rank at D = 4, N = 20000, K = 4, float64, seed 20260920 (the one width this repository has measured; a sweep across wider D is not yet tracked). The informative representation, which genuinely separated four clusters, pins to erank 3.0047 — clustering is anisotropy, so a representation that learned the task cannot spread across the space it has. The frozen-random encoder, which never received a gradient, is isotropic noise and reads erank 3.9993 — higher, not lower, than the encoder that learned something.

    pi_jepa.collapse_report's two geometric collapse legs, std_min and effective rank, are both computed from the representation alone, before either one ever looks at the label. That is a structural blind spot: the repository's own mandatory frozen-random control — an encoder that receives no gradient, hence isotropic noise independent of the real, unpermuted label — is exactly the plant the blind spot predicts, and it is the one measured above. Both geometric legs read it green, and effective rank reads it healthier than the encoder that actually learned the four clusters; only a label-aware leg (i_q) calls the frozen-random plant dead. pytest tests/cameron/test_third_collapse_leg.py -q is the producer.

    informative erank 3.0047 against frozen-random erank 3.9993, both green under the existing legs (D=4 only)
12. now

    The exact side holds; the learned side is the open question

    The exact identities still hold to float precision. What keeps failing is the learned part — a trained operator head (κ 1.34 against a true 93.51), a trained read (swap ratio 0.999745), a trained encoder — and every claim that the exact read's advantage carries over to a trained model. That is what decides the next move (§7).

6What died, and what killed it

A result nobody can check is worth nothing, so the failures are published with the same precision as the successes. Each row below was a claim this repository made, and each was withdrawn by its own instruments.

x float32/bf16

float64

Move x to see exp(x) grow and where it becomes infinite. The wall is a property of the dtype, not the value — but bf16 and float32 do not share one: bf16 overflows first, at 88.71892521235186, against float32 at 88.72283905206835, and the two disagree across that whole interval (at x = 88.7215, float32’s exp is 3.3982583016316987e+38, finite, while the same result cast to bf16 reads inf). float64 moves the wall out to 709.782712893384. Reproduced with python -c "import torch; print(torch.log(torch.tensor(torch.finfo(torch.float32).max, dtype=torch.float64)).item(), torch.log(torch.tensor(torch.finfo(torch.bfloat16).max, dtype=torch.float64)).item())" on torch 2.14.0+cpu.

claim	what killed it	the number
A signed, pivot-routed path sum reduces sign flips at scale	pre-registered slope kill on the shipped operator	−1.298 vs bar −0.3
A zero gate gives bitwise standard attention	Lean: gate_zero_not_stochastic	row i sums to i+1
Theorem 4: a resolvent read is depth-separated from a fixed-depth stack	fitted coefficients; Cayley–Hamilton caps any separation at n	fit 1.448e-02% vs 112.6157%
Under intervention a resolvent read's error is κ-invariant while a direct read's grows	pre-registered kill, 5/5 seeds, wrong sign	OOD MAE: solve 0.0741, direct 0.0718
κ = 164.25 on the demo's 14×14 grid	a hard-coded string; nothing ever computed it	fabricated
Spearman ρ = 0.743864 on U1/N3	no producer has ever existed	struck
Assign each coordinate its corner by β = 1 − α	no fixed point on the value axis; ranked 21st of 35 on its own null	slope −1.0027
A trained π-JEPA predicts human chess moves	a zero-parameter heuristic won	0.3401 vs 0.2882
The consequence swap moves the read and the null does not	the null's zero was an identity of the definition	learned 0.999745 vs negative 1.073511
The β = 0 corner is linear attention	no finite feature map: rank tracks n	rank 8 … 252
Depth buys reach (stacks of 1/2/4/8 layers)	the ladder measured optimiser steps	2-layer 0.0555 → 0.3005
The read adds an architectural refusal channel	pre-registered counter held: a GRU's own entropy does it	recall 0.8959 @ 0.8903
A logit-Nash stance composes two sign flips	both kills, 5/5 seeds, every configuration	5.2888 vs 2.7333
Smoothing Sherman–Morrison with a teleport is harmless	it attenuates the interventional signal	−43.1%
Capacity on the cube is an area — coexisting basins can be counted	basins never coexist across the swept range	disjoint at [0.5436, 0.7250], [1.0872, 1.6236], [2.1745, unclosed past 120]; sequence 0-1-0-1-0-1
bf16 widens the overflow ceiling	bf16 shares float32's 8-bit exponent but carries fewer mantissa bits, so its own max is smaller — the wall narrows, it does not move outward	float32 wall 88.72283905206835, bf16 wall 88.71892521235186 (bf16 overflows first); headroom 47.31×, 46.24×, 23.19× over 200 AdamW steps
bf16 and float32 share the overflow wall, at 88.72283935546875	this page's own published constant was wrong twice over — wrong in the eighth decimal against the true float32 value, and wrong in kind, since bf16 does not share float32's wall at all	corrected 2026-09-20 to float32 88.72283905206835, bf16 88.71892521235186
The attention family cannot represent a closed class, because exp is never zero	refuted by construction, no training: under a causal mask any row-stochastic matrix is lower-triangular, so its eigenvalues are its diagonal and a closed class is just Pii = 1. A real sparsemax projection reaches it directly, and a second construction gives six closed classes at n=6	two unit eigenvalues, 11 of 14 subsets closed, exact rational and float64 agreeing
The gate closes by content where a mask closes by position, and that separates it	sparsemax, entmax and top-k routing also produce exact, learned, content-dependent zeros, and none is built from exp, so the theorems do not reach them	per-row accuracy 0.9919 sparsemax vs 0.9845 gate — the rival wins
Row disagreement is invisible at k=1 and becomes a corridor under composition	the leak does grow with k, but it grows just as fast on sequences whose rows agree, so it is generic mixing and not a boundary effect	agreeing 0.676408 vs disagreeing 0.732453, within 1.08×
Effective rank detects a collapsed representation	clustering is anisotropy, so a representation that learned K clusters pins near K−1 however wide the layer, while a frozen-random encoder fills all D. No threshold fits between them at any width	noise beats informative at every width; the published ratio is withdrawn as unproduced (CORRECTIONS.md C9)
A hitting-time bed can separate an arm from transition counting	no live cell at any budget across four decades: its unscoreable gate counts the sealed share of the draw, its R² window is 89% draw geometry, and its refusal head loses to a one-line shortcut that reads no structure	refusal recall 0.1095 vs shortcut 0.8000, 7.3×

Most of what stands today was built by one of these deaths. The refuted parity clause became the β switch. The prefix-scan limit became the path-product gate and a theorem about it. The smoothed denominator became refusal as a decision. A raw grep that miscounted the proofs became a counting script that must first count a planted file correctly. The practice that makes the pattern possible is cheap to state and expensive to keep: a claim is written down with the number that would kill it before the run, and the run is reported whichever way it goes.

MISTAKES.md

74 failure mechanisms

V 30 vacuous controls · P 16 provenance · M 21 measurement · D 7 design. Each with the instance, the rule, and the check that stops it recurring.

STRUCK.md

12 withdrawn constants

Rendered from a registry the test suite enforces, so a struck number cannot quietly ship again.

docs/FAILS.md

Retracted, broken, open

Retractions, commands that do not run clean, measured negatives, known defects, and claims that were never verified.

7Where it goes next

The open fronts, each with the bar it has to clear, and the one move chosen from them.

front	the standing bar	state
Prediction leg of the north star	beat a trivial baseline at the family's own prediction task	open
BED-H in-context identification	reported magnitudes of the 2026-09-14 draw, not asserted thresholds (tests/beds/test_bed_h.py:461-462): per-position total variation 0.0802 for the strong form, measured on 32 instances (ceqjepa/beds/bed_h.py:622-635), against 0.1118 for a random other draw. The bar the test asserts is the ordering mean(mean_tv) < mean(draw_tv) (tests/beds/test_bed_h.py:475)	open
The one-solve claim's loss condition	a stack of depth ≤ 2 reaching 0.90; the best so far reads 0.4858	not fired
Depth race, 160-goal point	reach the oracle solve's 1.0000	running
Segmentation at range, against the kernels	the carry-extended merge against FlashAttention varlen and FlexAttention document masks on packed sequences, at matched cost. Dies if either reproduces a carry = 0 bitwise-zero contribution	registered
Whether the instruments measure the model or the draw	the log-ratio pairing regression: slope within one standard error of zero across five seeds. Five instruments have already failed this in its additive form	blocking
Chess fortresses, BED B1	200 fortress positions per cell. KBPKB at depth 6 yields 3 of 75, about 4%, the only cell whose point estimate clears it — its 95% lower bound extrapolates to 140 and misses. Seven cells are undersampled, not void	calibrating
Committor read, component P3	+0.8851; the encoder's widest layer reads +0.8424	open
Joint-training gate	P1 pass, P2 and P3 answered, P4 fails at 0.9997, so joint training stays blocked	blocked
Canon books 00 and 07	listed in the charter as the north-star decision tree and the consolidated attacks	unwritten
A pinned environment	the Hugging Face tests fail on a torch drift, and the full suite has never completed on one CPU	open

The 160-goal point crashed on a constant-label draw: a single absorbing target makes the label constant, and the builder divides by its variance. ZeroDivisionError at ceqjepa/goal_family.py:525, catalogued as MISTAKES V-12. The guard belongs in the builder. Whether near-degenerate draws already reached the published depth-race points is an open audit, not yet settled. The extrapolated 0.4810 and asymptote ≈ 0.4923 are two increments of arithmetic, not a measurement (ceqjepa/depth_race.py:184-185,215).

The next move

Race an estimated operator, not the true one. Every exact-read win on this page was handed the true operator. That makes the solve an oracle rather than a model, which the error ledger files as D-2, so none of those wins can tick the prediction row. The next run estimates the operator from the same transition stream the opponent trains on — the whitened recursive-least-squares estimator already measured at its sampling floor, 0.030243 against Hebbian 0.348321 on a 10,000-transition stream (both figures from commit 82eb2d4; the tracked test tests/curvature/test_lstd_bed.py:54-56 carries the 0.030243 and describes it as the sampling floor, and no tracked file prints the Hebbian figure) — and races one exact solve on that estimate against a masked attention stack at matched parameters, on goals neither has seen.

Registered before it runs: the bar is the best stack published so far on that bed, 0.4858, at matched transitions across five seeds; the kill is the estimated solve at or below it; the planted negative is a shuffled stream, which must drive the solve to the floor; the ceiling is the true-operator solve at 1.0000. Corrected 2026-09-20: that negative was necessary and not sufficient, because the grading was blind to it. An item bootstrap resamples at a fixed fitted read and cannot see the noise of the fit itself, which dominates whenever the read is fit rather than given — measured on the null arm at item SE 0.0003 against an across-stream SD of 0.0011, 3.33× larger, so under the item bootstrap alone (n_streams=12) a zero-information arm's read swings from −12.55σ to +1.73σ across the same five seeds, while under σ_total (n_streams=12) the same arm reads −1.56σ to +0.32σ — noise from fitting the read, not signal in the stream. Any fit arm is now graded by σ_total = margin ⁄ √(se_item² + sd_stream²), with sd_stream taken across independent refits at pinned chain, embedding and items. Under it the shuffled arm reads +0.2σ_total and the live arm falls from +8.3σ_item to +8.1σ_total, against the oracle's +9.1; the regression guard is tests/cameron/test_estimated_operator_margin.py::test_shuffled_stream_is_null_under_sigma_total_not_item_se, whose primary-seed bed asserts this σ_total stays within 2 and goes red the moment the stream permutation is left a no-op. The arm behind these numbers is transition-counting RLS at full rank — 256 free parameters, the entire 16×16 transition table — which the capacity condition in ceqjepa/lstd_bed.py refuses opponent status because it can represent the empirical MLE outright; it is the row's floor, not its opponent, and the prediction row is not ticked.

Why this one. It is the only open comparison that could put a tick in the prediction row honestly — a named opponent, a named task, no oracle — and it tests the step where the recent kills have landed: from a given operator to a learned one. It is also cheap: an estimator, a triangular solve and a stack that already has a pinned test set all run on a CPU. If it wins, the family has its first prediction result. If it dies, the record learns that the read's exactness does not survive estimation, and the claim settles where the README already puts it: strictly more reachable, not more accurate.

Closed 2026-09-20, against itself. That race ran and the move above is retired. Giving the empirical MLE a bolted-on no-trade band at the same cost beat a rank-4 capacity-admitted resolvent arm on realized log-growth on 5 of 5 seeds — means 0.046291 against −0.060393, a gap of 0.10668 against a combined seed spread of 0.01175 — and the ordering did not flip between log-growth and R². The band is a hat anyone can wear.

Where this stands, 2026-09-20

The operator is a kernel, and it has been scored as a model. Eleven claims died on this date, each with the number that killed it, and they share a shape: every one was a claim about representation, and every one died to something cheaper doing the same job. Sparsemax opens arbitrarily many closed classes by direct construction — real Martins–Astudillo projection on [10], [0.5, 0.5], [−5,−5,5], [−5,−5,0.5,0.5] gives diag(P) = [1.0, 0.5, 1.0, 0.5] bitwise and two unit eigenvalues, with all 14 proper subsets agreeing between exact rational and float64 arithmetic. A depth-2 stack recovers 71.36% ± 6.76% IoU of the true separatrix from 27 local features with no operator access at all, against a majority-class floor of 0.0000. So the structural claim — that the attention family cannot represent a closed class — is retracted, and the two Lean theorems bind exp-based scores only.

What survived is draw-free algebra, and it is narrower than what was claimed. The block summary is exact to 2.085e-15 and buys range: on a bed carrying one logit at 800, dense readout is nan at every β while the summary returns the closed form. A path product forces cross-row agreement structurally — 1500 of 1500 held-out sequences exactly consistent against sparsemax's 1352 of 1500 — and pays an exact, enumerated price for it: i reachable zero patterns against sparsemax's 2ⁱ−1, every gate pattern a strict subset, 31.875× at i=8. That consistency is measured with a hand-set boundary at a single application; a learned gate is not bitwise zero under powers (224 of 12,000 values nonzero in 4 of 5 seeds), and the leak that grows with k is generic mixing rather than a boundary corridor — agreeing sequences leak 0.676408 against disagreeing 0.732453, within 1.08×.

The next move is a kernel benchmark, not a model race. The one axis where the summary beats anything before it is the one nobody competes on: exact within-kernel segmentation at range. The carry-extended merge goes against FlashAttention varlen and FlexAttention document masks on packed sequences, at matched cost. The kill: if either reproduces a carry = 0 bitwise-zero contribution at equal cost, the fourth field is a rename and this direction dies.

But one measurement comes first, because nothing can be scored until it lands. Five instruments died on this date of a single disease — each scored a property of the draw rather than of the model. Effective rank prefers a frozen-random encoder by 22× at D=64. A hitting-time bed's R² window is 89% draw geometry: arm error differs 1.06× between draws where counting won and broke, while the label's own spread differs 5.16×. Its refusal head was beaten 7.3× on recall by a one-line non-causal shortcut that reads no structure at all. The proposed cure — pairing each score against a null built from the same draw — appeared to fail its own regression, at slope −1.4513 with a standard error of 0.8439 over five seeds. Whether that failure was the cure or its arithmetic was then tested directly, on the reasoning that a draw entering as a factor rather than a term cancels under a log-ratio and not under a subtraction. It could not be tested at that bed. The null there fires on zero instances at every one of the five seeds, so its precision is undefined and its recall is exactly 0.0, and no ratio can be formed against a twin that scores nothing. The additive slope reproduces bit for bit, but at five seeds its 95% interval runs roughly −3.7 to +0.8 — wide enough to contain zero, no effect, and a doubling at once, which is a statement about power rather than a result. So the question stands open and untested: this project has not yet shown that its instruments measure its models rather than its beds, and the one bed built to settle it has a degenerate null.

8The documents

Every document carrying a measurement, a limitation or a decision, rendered in full and searchable from the tabs above.

The record Retracted, broken, open · Component ledger · The programme · Corner-rule retirement · Kaggle card · DR-2 card

Pre-registrations BED-H · REMOVAL-ECHO v1

Ledgers 74 failure mechanisms · 12 struck constants · Mathematics · Model card · Costs · V17K rulings · V16 calibration

The canon Charter · 01 accuracy · 02 training · 03 kernel · 04 beds · 05 repairs · 06 predictions · 08 architecture · 09 chess and markets · Corrections

The paper The shape of CEQ · PDF · Working sources · Bibliography audit · Aliases

Books 00 and 07 of the canon are listed in the charter and have never been written. The canon changes through one door only, its corrections log.

9Reproduce and cite

Every number on this page comes with the command that reproduces it.

git clone https://github.com/teerthsharma/resolvent && cd resolvent
pip install -r requirements.txt

python -m pytest tests/arm_smprime tests/arm_pl -q   # 78 passed: the Lean corners, in code
python -m ceqjepa.operator                           # ALL SELF-CHECKS PASSED
python -m ceqjepa.dr1                                # ALL SELF-CHECKS PASSED
python scripts/lean_count.py                         # 13 files: 134 theorems + 41 lemmas = 175
(cd lean && lake build CEQ)                          # exit 0

Lean 4 v4.7.0; mathlib is fetched by lake build at the revision pinned in lean/lake-manifest.json, and the first build downloads about 4.2 GB. House rule for contributions: every new number ships with the command that produces it, and every new check ships with a planted negative that fails without the change.

@software{sharma2026resolvent,
  author = {Sharma, Teerth},
  title  = {resolvent: one causal attention family spanning softmax attention,
            unnormalized-kernel attention and exact path products},
  year   = {2026},
  url    = {https://github.com/teerthsharma/resolvent}
}