Recog Geom Core

The starting point

Most geometry begins with a space, a collection of points, and then adds rulers, angles, and distances on top. Recognition geometry reverses the order. Its primitive objects are recognizers, things that take in observations, and events, the discrete outcomes those observations produce, like a detector click or a needle pointing. Space is not assumed; it is whatever structure is needed to make sense of what can be recognized. The core module, RecogGeom.Core, is the first formal step in that project: it defines the two kinds of objects and the single axiom that ties them into a workable starting point.

The first axiom, called RG0, is deliberately spare: it asserts that a configuration space exists and is nonempty. A configuration space is the type of possible states of the world, what the world really has. Recognizers never see a configuration directly; they only receive events. The axiom guarantees there is at least one such state to recognize, and the module proves the corresponding theorem, config_exists, which extracts a concrete witness from that nonemptiness. The second definition, the event space, carries a stronger requirement: it must contain at least two distinct events. One event would make recognition trivial, since every observation would be the same; two distinct outcomes give the recognizer something to distinguish.

These two pieces join in a structure called a recognition triple, which bundles a configuration space, an event space, and the proofs that each satisfies its axiom. This triple is the basic object of study for the whole framework. The module closes by declaring its own status complete: configuration space defined, event space defined, nonemptiness and nontriviality established, and the triple bundled. In plain language, the core module does not yet build any geometry. It establishes the ground rules for what can be recognized and what counts as an observation, the vocabulary the rest of recognition geometry will use to derive space itself.

What this means in practice is that the framework's entire edifice rests on a very small foundation: one existence axiom and one distinctness requirement. The power of the approach lies in what comes next, deriving the structure of space from the forced cost of recognition, but that chain begins here, with the assurance that there is something to recognize and that recognition is not a trivial act.

/-- A configuration space is a type of possible states of the world.
    Configurations are what the world "really" has—recognizers never
    get the configuration itself; they get events.

    RG0: There exists a nonempty configuration space. -/
class ConfigSpace (C : Type*) where
  /-- The configuration space is nonempty -/
  nonempty : Nonempty C

/-- **THEOREM**: A configuration space has at least one element.
    Replaces the vacuous `∃ c : C, True` with a constructive witness. -/
theorem config_exists (C : Type*) [cs : ConfigSpace C] : ∃ c : C, c = ConfigSpace.witness C :=
  ⟨ConfigSpace.witness C, rfl⟩

/-- An event space has at least two distinct elements -/
theorem event_nontrivial (E : Type*) [EventSpace E] : ∃ e₁ e₂ : E, e₁ ≠ e₂ :=
  EventSpace.nontrivial

/-- A recognition triple bundles a configuration space, event space,
    and the implicit structure connecting them. This is the basic
    object of study in recognition geometry. -/
structure RecognitionTriple where
  /-- The type of configurations -/
  Config : Type*
  /-- The type of events -/
  Event : Type*
  /-- Configurations form a valid configuration space -/
  configSpace : ConfigSpace Config
  /-- Events form a valid event space -/
  eventSpace : EventSpace Event

What this page does not claim

This module does not derive any spatial structure; it only establishes the existence and distinctness of the basic objects. The core module does not define what a recognizer is as a computational or physical entity. Recognition geometry does not claim that space is an illusion; it claims space is derived rather than primitive.

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/RecogGeom/Core.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: