Foundation Substrate Axioms

Substrate axioms in brief

In Recognition Science, the ledger (a discrete record of events) is the starting point. The substrate axioms are the framework's way of saying what kind of space that ledger lives in. The package records four structural inputs: a cellular completion of the cube graph, a one-acyclic substrate, loop entanglement, and compatibility with the realized recognition cycle. Each is a named assumption, not a derived result.

The first three of these are explicitly MODEL-level packaging. The package's own documentation states that smooth-topology content, such as cellular completions, Thom isomorphism, and Alexander/Lefschetz duality, is not yet available in the vocabulary the library can import. The former certificate fields for those clauses were deleted rather than left as hollow placeholders, a move the library calls a vacuity quarantine. What remains is a predicate-level token: a named structure that says "this assumption is in force," without pretending to prove it.

The fourth axiom is different. Compatibility with the realized recognition cycle is a real claim: it asserts the existence of a bijective one-bit-adjacent closed walk on the D-cube, which is a Gray cycle. The library proves this for every dimension D, using the standard binary-reflected construction. This is the one piece of the substrate package that is a theorem, not just a token.

In plain language, the package does two things. It names the structural assumptions the dimension route needs, and it honestly marks which of those are proven and which are not. The three unproven ones are targets for future work, not achievements. The one proven one, the Gray cycle, is a concrete combinatorial fact that holds in every dimension.

What this means for the framework: the substrate axioms are a checkpoint, not a destination. They say "here is what we need to assume about space," and they are explicit about the gap between assumption and proof. That gap is the difference between a model and a theorem, and the package is careful to keep the two apart.

/-- Bundled T7.5/loop substrate package. -/
structure T75SubstratePackage (D : Dimension) : Prop where
  cellular_completion : CellularCompletion D
  one_acyclic : OneAcyclicSubstrate D
  loop_entanglement : LoopEntanglement D
  compatibility : CompatibilityWithRealizedCycle D

/-- T7.5a: a cellular completion of the cube graph in dimension `D`.

Intended clauses (not yet honest Lean Props in-scope):
1. a closed orientable smooth `D`-manifold substrate,
2. a tame cube-graph embedding,
3. a retraction back to the cube graph.

Former fields `closed_orientable_smooth`, `cube_graph_embeds`, and
`retraction_back_to_cube_graph` were typed `True` (inhabited by `trivial`) and
were deleted: no manifold/embedding/retraction predicates exist in the current
import vocabulary, so an honest field type cannot be formed. This structure
remains a named MODEL packaging token for the dimension route. -/
structure CellularCompletion (D : Dimension) : Prop where

/-- T7.5c: integral `1`-acyclicity of the substrate.

Intended claim: the substrate's integral first homology vanishes.
Former field `H1_vanishes : True` was deleted: no chain-complex or homology
predicate is in scope for a dimension-only parameter, so no honest Prop exists
to inhabit. Named MODEL packaging token only. -/
structure OneAcyclicSubstrate (D : Dimension) : Prop where

/-- Dimension-uniform loop-entanglement: there is some recognized sphere
dimension `p ≥ 1` whose complement carries the required nontrivial
homological separator. -/
structure LoopEntanglement (D : Dimension) : Prop where
  exists_p : ∃ p : ℕ, 1 ≤ p ∧ True

/-- Every dimension admits a BRGC Gray-cycle witness. -/
theorem compatibility_trivial (D : Dimension) :
    CompatibilityWithRealizedCycle D where
  witness_is_closed_walk := by
    classical
    refine ⟨brgcPath D, ?_, ?_⟩
    · have h_inj : Function.Injective (brgcPath D) := brgcPath_injective D
      have h_card : Fintype.card (Fin (2 ^ D)) = Fintype.card (Pattern D) := by
        simp
      exact (Fintype.bijective_iff_injective_and_card (brgcPath D)).2 ⟨h_inj, h_card⟩
    · intro i
      cases D with
      | zero => exact Or.inl rfl
      | succ d =>
        exact Or.inr (brgc_oneBit_step (d := d + 1) (Nat.succ_pos d) i)

What this page does not claim

The substrate axioms do not prove that space is three-dimensional; they only package assumptions used by the dimension route. The package does not establish the existence of a smooth manifold substrate; that remains an open target. The Gray cycle theorem does not imply the other three axioms are proven.

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