Foundation Simplicial Ledger Simplex3

The Simplicial Voxel

A simplex is the simplest shape that fills three-dimensional space: a tetrahedron, with four vertices and four triangular faces. In the Recognition Science framework, the declaration Simplex3 defines this tetrahedron as the atom of volume in its ledger, a discrete record of events. The structure pins down four vertices in ordinary three-dimensional coordinates and requires a positive volume, so it cannot collapse into a flat or empty shape. This is a definitional choice, not a derived result: the framework models its fundamental volume element as a tetrahedron rather than a cube.

The same module defines a simplicial ledger as a non-empty collection of these tetrahedra that is intended to cover a manifold, like tiles covering a floor. The covering property is explicitly marked as a scaffold, a placeholder whose proof awaits simplicial complex axioms and manifold topology. A sheaf then assigns a recognition potential, a number, to each tetrahedron. The local cost of recognition on one tetrahedron is the framework's cost function J multiplied by that tetrahedron's volume; the global cost is the sum over all tetrahedra, defined only for finite ledgers.

The module proves one substantive theorem: a recognition loop, a closed cycle of tetrahedra that passes through every 3-bit local pattern state, must have length at least eight. The proof relies on the surjective pass through the eight possible states of a three-bit pattern, so the eight-tick cycle emerges as the unique minimal closure. This is the theorem's real content: the discrete structure of the ledger, not any continuous geometry, forces the minimum cycle length.

In Recognition Science, this simplicial formulation is meant to replace a coordinate-fixed cubic lattice with a coordinate-free sheaf representation, unifying local and global cost variations. The declared theorem local_global_unification states that if the global cost is stationary and a local-global hypothesis holds, then every local potential is at its unit value. That hypothesis, that global stationarity forces local stationarity, is explicitly tagged as an empirical hypothesis with a named falsifier: a global minimum containing non-stationary local sections.

/-- **DEFINITION: Simplicial Voxel**
    A 3-simplex (tetrahedron) representing the atom of volume in the ledger. -/
structure Simplex3 where
  vertices : Fin 4 → (Fin 3 → ℝ)
  volume   : ℝ
  vol_pos  : volume > 0

/-- **THEOREM: Eight-Tick Cycle Uniqueness**
    The 8-tick closure cycle is the unique minimal sequence for a self-consistent
    recognition loop on a simplicial manifold. -/
theorem eight_tick_uniqueness (_L : SimplicialLedger) :
    ∀ cycle : List Simplex3,
    (is_recognition_loop cycle) → 8 ≤ cycle.length := by
  intro cycle hloop
  rcases recognition_loop_has_surjection hloop with ⟨pass, hsurj⟩
  exact eight_tick_min pass hsurj

/-- **DEFINITION: Simplicial Ledger**
    A collection of 3-simplices that form a manifold covering. -/
structure SimplicialLedger where
  simplices : Set Simplex3
  /-- The simplices form a non-empty set (non-vacuity). -/
  non_empty : simplices.Nonempty
  /-- SCAFFOLD: Manifold covering property.
    Proof requires simplicial complex axioms and manifold topology.
    See: LaTeX Manuscript, Chapter "Gravity as Recognition", Section "Simplicial Ledger". -/
  is_covering : Prop

/-- **THEOREM: Local-Global Unification**
    The global J-cost is stationary if and only if every local J-cost is stationary
    within its simplicial section. -/
theorem local_global_unification (L : SimplicialLedger) (S : SimplicialSheaf L)
    [Fintype L.simplices] (h : H_LocalGlobalUnification L S)
    (h_global : ∀ s : L.simplices, local_variation s (S.potential s) = 0) :
    ∀ s : L.simplices, J_stationary (S.potential s) := h h_global

What this page does not claim

The manifold covering property is not proved in this module; it is a scaffold placeholder. The local-global unification theorem does not prove that global stationarity implies local stationarity; that is an empirical hypothesis. Simplex3 does not derive the three-dimensionality of space; it only defines a tetrahedron in three coordinates.

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/SimplicialLedger.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: