pith. sign in
module module moderate

IndisputableMonolith.VoxelWalks

show as:
view Lean formalization →

VoxelWalks supplies the core definitions for voxel walks, sigmaCore, fHalfVoxel, fFace, sigmaN, and A2 structures in the Recognition Science framework. Researchers extending discrete geometry or lattice models for QED/QCD would cite these objects. The module consists entirely of definitions and supporting constants built atop Mathlib.

claimThe module defines $\sigma_{\rm core}$, $\sigma_{\rm core,n0}$, $f_{\rm eye}$, $f_{\rm half-voxel}$, $f_{\rm face}$, $\sigma_N$, $A_2$, $A_2^{\rm QED}$, $A_2^{\rm QCD}$, and the convergent and expansion lemmas for $\sigma_N^{\rm QED}$.

background

VoxelWalks operates inside the Recognition Science monolith and imports only Mathlib. It introduces voxel-specific maps and sigma functions that sit between the phi constant and the A2 structures. These objects support the phi-ladder mass formula and the eight-tick octave by providing discrete walk primitives on a three-dimensional lattice.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

VoxelWalks feeds A2_QED and A2_QCD, supplying the voxel walk primitives required for the QED and QCD expansions. It closes part of the discrete geometry layer that precedes the forcing chain steps T7 and T8.

scope and limits

declarations in this module (13)