Foundation Primitive Recognition Calculus Multi Distinction Geometry Vtx

The square's corners

In geometry, a square is defined by its four corners. The declaration Vtx does exactly that: it names the four vertices v00, v01, v10, and v11. Each vertex is a configuration of two independent binary distinctions, like two switches that can each be off or on. The first letter or number stands for the first switch, the second for the other. So v10 means the first switch is on and the second is off. This is the entire content of the declaration: it is a definition, a way to label the corners of a square, not a claim about the physical world.

The square these vertices define is not an arbitrary one. The framework builds it from the idea of a ledger, a discrete record of events where each event is a distinction. Two independent distinctions naturally form a square: four possible combinations, four corners. The declaration Vtx is the grammatical subject of the geometry that follows. It lets the framework's library, a machine-checked collection of formal theorems, state and prove that the boundary of the boundary of this square is zero. In plain terms, going around the square's edges and then taking the difference between the start and end of each edge cancels out at every corner. This is a formal theorem, tagged THEOREM, proved in the library as boundary_squared_zero.

What Vtx does not claim is just as important as what it does. It does not assert that physical space is made of such squares. It does not claim that the universe runs on a binary ledger. The declaration is a definitional choice, a MODEL, not a physical law. It is the first step in a formal structure that shows how geometry, in the sense of independent coordinate directions and closed boundaries, can be seen as the algebra of several independent distinctions. But the bridge from this formal algebra to the physical claim that space has three dimensions is a separate, open question. The declaration itself is silent on that bridge.

In Recognition Science, this declaration is the seed of a larger result. The framework's library proves that independent distinction channels commute, meaning the order in which you make two distinctions does not matter, and that boundaries close. These two facts, the independence of coordinate directions and the closure of boundaries, are the load-bearing pieces of geometry. Vtx is the first brick: it names the corners so the rest of the structure can be built. What a reader can now see is that the square, the most basic object of planar geometry, has a precise formal origin as the configuration space of two independent distinctions.

/-- Vertices of the square: the four configurations of two channels. -/
inductive Vtx where
  | v00 | v01 | v10 | v11
  deriving DecidableEq, Repr

/-- **∂² = 0 on the square.** The boundary of the boundary of the face is the zero
0-chain. Closed boundaries are forced by the two-channel cell structure: the
oriented edges around the face cancel at every vertex. -/
theorem boundary_squared_zero (c : ℤ) : d1 (d2 c) = fun _ => 0 := by
  funext v
  cases v <;> simp [d1, d2]

What this page does not claim

Vtx does not claim that physical space is composed of such binary squares. The declaration does not assert that the universe runs on a discrete ledger of distinctions. Vtx does not itself bridge the formal algebra of distinctions to the physical claim of three spatial dimensions.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/MultiDistinctionGeometry.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: