Pith. sign in
module module moderate

IndisputableMonolith.Foundation.RecognitionLattice3

show as:
view Lean formalization →

RecognitionLattice3 supplies the three-dimensional recognition lattice, domain costs, canonical thresholds, and RecogLattice3Cert in the Recognition Science foundation. Lattice users and forcing-chain developers cite it for the 3D structure and basic certificates. The module is definitional, establishing non-negativity and positivity properties from the imported Cost and Constants layers.

claimThe module introduces $\text{domainCost}$ as the lattice-domain cost map, $\text{canonicalThreshold}$ as the positive threshold, and $\text{RecogLattice3Cert}$ as the inhabited certificate for the three-dimensional recognition lattice.

background

The module imports Constants, where the RS time quantum satisfies $\tau_0 = 1$ tick, and Cost, which supplies the underlying cost structures. It defines domainCost, domainCost_at_eq, domainCost_nonneg, canonicalThreshold, canonicalThreshold_pos, RecogLattice3Cert, cert, and cert_inhabited. These objects sit inside the foundation layer that precedes the T0-T8 forcing chain and the Recognition Composition Law.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

RecognitionLattice3 feeds the root IndisputableMonolith module, which exposes the master forcing-chain theorem together with the T-1 and absolute-floor surfaces. It supplies the lattice infrastructure that supports the eight-tick octave and the emergence of D = 3 spatial dimensions.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)