Which ontological commitments does a formal foundation carry — and what can a formalization actually show about them? A monograph rebuilds logic, ZFC, and dependent type theory from four operators, keeps every claim at the level it can be checked, and treats axioms as conventions.
The repository's own map. Claims are kept at the level they can be checked: a Lean file is judged by what the kernel accepts, a result is reported with its axiom footprint, and a conclusion about a foundation is separated from a conclusion about one formalization of it.
Logic, sets, and type theory from four operators, with a reproducibility protocol and a case study in a non-integer radix.
02 Formal failure & ontological overreachWhat can and cannot be inferred when a formalization breaks.
03 The auditA check of a published Lean listing: verbatim, a repaired neighbor, and what happened.
04 What Lean assumesPlain-language notes on the commitments a proof assistant carries.
One small base. The untyped lambda calculus is recovered by renaming; the classical and intuitionistic propositional logics appear as two disciplines of Refuse; ZFC appears as closure conditions; a Lean-style dependent type theory appears as the internalization of Refuse inside Bind.
Introduce a distinguished item.
Restrict a domain of admissible items.
Relate, or abstract over, items.
Evaluate, or identify.
An operator correspondence has mathematical content only when its domain, interpretation, and preserved structure are specified; otherwise it is notation or analogy, and the monograph labels it as such.
“The axioms … are treated as conventions: arbitrary at the base, and valuable because they give everyone a common language in which results can be checked, combined, and reused.”
Not forced — but determinate in their consequences once fixed. The differences between the three foundations are located precisely, at the point where each decides how Refuse may be used.
Every document and Lean file marks its claims with one of these labels — so a reader can tell what was established, relative to what, and by what kind of check.
Elaboration · tactic · kernel · or a derived contradiction. A tactic that fails does not show the statement is unprovable by another route.
base · footprint · layer · declared axioms · scope · environment · controls.
One of the sources' own numerical experiments, reproduced in this page. For the monomial
trajectories xₙ(t) = tⁿ / n!, which orders satisfy the self-inversion axiom A_k : j = 1/j
(with the nonzero clause)? The repository's simulations/jerk_regress.py answers: only the diagonal.
Result (from jerk_regress.py, exact arithmetic): A_k holds for xₙ exactly when k = n,
and the number of pairs of distinct orders (m, n), m ≠ n, jointly satisfied by any x_p in this family is 0.
A correct derivation from its axioms — a relative result, not an independent one.
It does not claim that TONE is false, and it does not claim that any foundation is neutral. Foundations carry commitments, and the notes name some real ones. The claim under test is narrower: that a particular formalization attempt breaking shows the underlying foundation to be ontologically corrupt. The experiments and the audit are designed so that this claim can be examined directly.