pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Foundation.RecognitionLattice3

show as:
view Lean formalization →

RecognitionLattice3 defines the three-dimensional recognition lattice with a domain cost function, a positive canonical threshold, and an inhabited certification structure. Foundation researchers cite it when assembling lattice models that support the forcing chain from T0 to T8. The module supplies the relevant definitions together with equality, non-negativity, and positivity lemmas plus a direct inhabitation proof for the certificate.

claimThe module introduces the domain cost function $C$ satisfying equality and non-negativity conditions, the positive canonical threshold $T>0$, and the inhabited three-dimensional recognition lattice certificate $C_3$.

background

The module belongs to the foundation layer of Recognition Science and imports the fundamental time quantum τ₀ = 1 tick together with cost primitives. It introduces the domain cost function over a domain, establishes that the function meets equality conditions at corresponding points, and proves non-negativity. A canonical threshold is declared and shown to be strictly positive. The recognition lattice certificate is defined as a type whose inhabitation is witnessed by an explicit construction.

proof idea

This is a definition module. It declares the domain cost function and supplies two short lemmas for its equality case and non-negativity. It declares the canonical threshold and proves positivity by a direct inequality. The recognition lattice certificate is declared and an inhabitant is constructed by a single term.

why it matters in Recognition Science

The module supplies the lattice structures consumed by the root IndisputableMonolith module, which exposes the master forcing-chain theorem and the T0–T8 sequence that forces J-uniqueness, the self-similar fixed point phi, the eight-tick octave, and D = 3 spatial dimensions. It thereby contributes the certification layer referenced for the Recognition Composition Law and the absolute-floor theorems.

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)