Witness Independence: The Two Axes

While drafting this very series — the one arguing that you have to file claims honestly — we generated a claim that forced us to file it twice. Not as a stylistic choice. The discipline produced the split on its own filing. The claim arrived as an ordinary result before we applied the filing discipline to it, so the split wasn't staged.

Here is the situation any reviewer recognizes. You have a result. Part of it is airtight — checkable, mechanical, the kind of thing a machine can settle and you stop arguing about. Part of it is an interpretation you believe but cannot mechanically settle. The temptation, every time, is to file the whole thing under one verdict and let the airtight part carry the interpretation across the line. That move feels like rigor. It is the opposite. It is the place confident-wrong output hides — a real certificate vouching for a purchase it never covered.

So let me show you the claim that caught us, exactly as it arrived.

The claim, and why one filing would have lied

A set of six elements can carry two different group structures. One is commutative — the cyclic group Z/6Z, where order doesn't matter. One is non-commutative — the symmetric group S₃, where it does. We had a seven-phase process and wanted to know whether its structure realizes only the commutative sector. A clean, narrow, answerable question.

The honest answer is two filings, because the claim spans two independent questions, and they cost different things to underwrite.

The first filing is the algebra, and it is Proved — machine-checked. On any six-element carrier, any element of order 6 forces the cyclic structure Z/6Z, and S₃ has no element of order 6. That is closed in Lean 4: a kernel decides it, with no gaps. Because a kernel decides it, the result is model-independent — the answer is fixed by the proof, not by any model's judgment; there is nothing left to interpret.

The second filing is the interpretation, and it is Predicted — a framework, not a theorem. The interpretive claim is that this dual structure forbids a canonical, native identity for the six-element object in the system's own terms. The Lean proof does not underwrite that. It can't, because the claim turns on a facet the algebra never speaks to — what the system counts as a "canonical identity" is simply not a question the group theory addresses. So this filing is generated by us, labelled by us as Predicted. The kernel closes a formal statement; taking that formal closure to establish the informal claim — that an order-6 element forcing Z/6Z means the process realizes only the commutative sector — is itself a facet-axis call we make and label, not one the kernel decides for us.

The first filing is a win on what I'll call the model-axis — independence that comes from different reasoners reaching the same answer, which a machine-decidable kernel maxes out by construction. The second filing is a question on the facet-axis — independence that comes from a genuinely different kind of question being asked, here the interpretive question the algebra is silent about. A reader who buys only the first filing has purchased one unit of witness on the model-axis and exactly zero on the facet-axis.

If you collapse the two into a single "verified," you ship something that looks like a proof — the Lean certificate is real, after all — while quietly charging a model-axis win to the facet-axis account. That is the N=1 trap wearing a certificate. The receipt is genuine. It just doesn't cover what you're claiming it covers.

Two axes, two prices, two filings

This is the whole move, and it is smaller than it sounds. Witness independence is not one quantity. It decomposes along two axes that do not substitute for each other:

• The model-axis asks: did independent reasoners converge? A different model family attesting the same result earns witness here. The same model run again earns none — it is one witness, repeated.
• The facet-axis asks: was a different facet attested? A machine certification settles one facet. An interpretive judgment about meaning settles another. They are not interchangeable, and one cannot be paid for with the other.

A claim that lands on both axes gets filed as two units: the part that is proved on the axis where it's proved, and the part that is predicted on the axis where it's only argued. You count witness along each axis, never as an aggregate "checks performed" — because the aggregate is precisely the comfortable middle number that lets the dangerous case through. The split is the honesty.

To be plain: the two-axis decomposition, as an abstract structure, is something we can point at formally — but its identification with this example's algebra-versus-interpretation split is itself an interpretation we're making, not a theorem. So treat the framing as early. It's a way of filing claims that we generate and label as such, demonstrated so far mostly by running it on ourselves. Come break it. If you can show me a claim that spans both axes and is honestly served by a single filing, the discipline is wrong and I want to know.

We didn't go looking for this example — we hit a real claim mid-draft and it refused to file as one unit.

A machine proof that settles the math buys you zero on the question of what the math means — so a claim that spans both gets filed twice, not once.

Proofs for this series: github.com/field-effect-institute/witness-independence-proofs

Piece 1 of 3 | Series introduction: “To Figure Out How Humans and AI Should Work Together, We Had to Ask a Simpler Question First”
Next: “Human-at-the-Loop: Naming the External Axiom the Algebra Requires”