pith. sign in
module module high

IndisputableMonolith.Foundation.RecognitionLattice3

show as:
view Lean formalization →

Module RecognitionLattice3 defines the domain cost function and RecogLattice3Cert for a three-dimensional recognition lattice, building directly on the RS time quantum and cost primitives. It is imported by the root IndisputableMonolith module during assembly of the forcing chain. The module contains only definitions and elementary properties.

claimThe module introduces $\mathrm{domainCost}$ (a non-negative cost on domains) with associated lemmas $\mathrm{domainCost\_at\_eq}$ and $\mathrm{domainCost\_nonneg}$, the positive canonical threshold, and the inhabited certificate $\mathrm{RecogLattice3Cert}$ for the 3D recognition lattice.

background

The module imports the RS time quantum $\tau_0 = 1$ tick from Constants and the cost structures from Cost. It defines $\mathrm{domainCost}$ together with its equality and non-negativity properties, plus the canonical threshold and the certificate $\mathrm{RecogLattice3Cert}$.

The local setting is the foundation layer for a recognition lattice in three spatial dimensions, consistent with the D = 3 result of the forcing chain. Upstream Constants supplies the single sentence: "The fundamental RS time quantum (RS-native). $\tau_0 = 1$ tick."

Sibling declarations supply the concrete objects: domainCost, canonicalThreshold, and the inhabited certificate.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the 3D lattice certificate and domain cost required by the root IndisputableMonolith module. That root exposes the master forcing-chain theorem (T0–T8) together with the Standard-Model Higgs effective-field-theory chain. The lattice construction therefore sits at the interface between the cost primitives and the spatial-dimension step (T8) of the forcing chain.

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)