Invariants you cannot name
Formal methods. — 2026-06-30. — 2 tracings. — Provisional record.
On the gap between knowing that a thing is preserved and being able to write down what it is.
The most useful thing an invariant does is fail. You perturb the system, you watch the quantity not move, and you learn where the walls are. But before any of that you have to be able to write the quantity down, and there is a stage before writing it down where you can feel it and cannot say it.
I want to take that stage seriously rather than treating it as a failure of rigour. It is not pre-rigorous. It is a different kind of knowledge: you can reliably say whether a given perturbation should preserve the thing, without being able to state the thing. That is an oracle. It is testable. It is just not yet a formula.
The practical version
When I am stuck here, the move that works is not harder thinking. It is finding the smallest system that still has the property and the smallest one that has just lost it, and putting them side by side. The invariant is whatever is different, and it is usually embarrassing how simple it turns out to be once the pair is in front of you.
What I have not solved is how to know whether the stage is productive or whether I am circling a thing that is not there.
Tracings
Drawn from this record.
- P102Legibility of lossPoetry
I spent four months failing to state this invariant and then wrote it in eleven lines without meaning to. I do not know what to conclude from that and I am not going to pretend otherwise.
- N101The legitimacy loopNotes
Traced from
Records that point here.
- P102Legibility of lossPoetry