1 The mathematics that disappears from a proof
On this page · Permalink · Source line 1
A mathematical proof can appear inevitable once it has been found. Definitions arrive in the right order. A lemma supplies exactly the missing implication. The notation seems chosen for the theorem that follows. What the reader sees is a path with its wrong turns removed.
That removal is often a virtue. A proof is meant to establish something, not to document every hour spent discovering it. An invalid argument cannot be rescued by the ingenuity of its author. A conjecture does not become true because it has survived many experiments. The finished proof deserves its economy.
Yet the work that disappears is not always dispensable. An unsuccessful representation may expose a hidden assumption. A counterexample may show that the original statement asked for too much. An alternative proof may reveal a connection that the shortest argument conceals. The difficulty may have been less in proving the eventual theorem than in learning what theorem could reasonably be stated.
Consider a researcher who tries to predict a system from only part of its state. The first calculation works. The second does not. There are several possible responses. One can abandon the approximation, add a corrective term by inspection, or repeat the calculation with greater numerical precision. One can also ask a different question: what exactly was discarded, and through which operation did it return? The last question turns an unsuccessful prediction into a mathematical object. It gives the next attempt something more useful than disappointment.
The Komorebi Methodology gives this change of emphasis a systematic form. Mathematical inquiry has a subject beyond the final implication. It has representations in which the implication becomes visible, transformations that preserve or lose information, and failures whose causes can sometimes be isolated. These are not merely psychological events surrounding mathematics. Once specified, they can have their own definitions, laws, and proofs.
Realization Calculus supplies a language for such transformations. Komorebi Space studies coherent realizations assembled from declared views. Obstruction and resolution methods ask what prevents a construction and what corrections are permitted. Proof-Path Theory distinguishes the certificate establishing a result from the larger field of claims, examples, and alternative routes surrounding it. Together they suggest a research practice in which the path to a theorem becomes more inspectable without being confused with the theorem's justification.[1], [2], [3]
This does not require every inquiry to follow a prescribed sequence. A useful method must accommodate the sudden example, the unmotivated analogy, the calculation whose importance becomes clear only later. It should make exploration easier to criticize, not prohibit exploration until all its reasons can be stated. The demand for exactness applies when a proposed relationship is promoted into a mathematical claim.
The distinction matters especially when a discovery is surprising. An unusual route can produce a valid proof. A familiar route can conceal a mistake. Neither the origin of an argument nor the confidence with which it is presented determines its logical force. What matters is whether the claimed conclusion follows, and whether the statement being proved is the statement the inquiry actually concerns.
Our proposal is therefore to give mathematical work two connected outputs. One is a certificate of what has been established. The other is an organized account of the representations, boundaries, and dependencies that made the certificate reachable. The second output need not preserve every abandoned calculation. It should preserve enough to explain why a route worked, why an important alternative failed, and what remains available for another question.
A proof can be complete while that larger record is impoverished. Conversely, a rich record can exist without a proof of the original target. A methodology becomes useful when it recognizes both situations and does not mistake one for the other. The first invites better preservation. The second invites a sharper statement of the remaining mathematical obligation.