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

IndisputableMonolith.Mathematics.GraphInvariantsFromConfigDim

show as:
view Lean formalization →

The module defines graph invariants derived from configuration dimension in the Recognition Science framework. It introduces GraphInvariant, GraphInvariantsCert, and counting functions as foundational objects. Researchers modeling discrete structures on the phi-ladder would cite these when linking graphs to the forcing chain. The module contains only definitions and no embedded proofs.

claimDefine the graph invariant type $G$ associated to configuration dimension $d$, together with the certificate type $C$ and the counting function $n(G)$ that enumerates invariants for a given dimension.

background

The module sits in the mathematics layer of Recognition Science and imports the fundamental time quantum from Constants, where the RS-native unit satisfies τ₀ = 1 tick. It introduces GraphInvariant as the central type encoding properties preserved under configuration dimension, along with GraphInvariantsCert for certification and graphInvariant_count for enumeration. The setting assumes the upstream forcing chain (T0–T8) that forces phi as the self-similar fixed point and D = 3 spatial dimensions.

proof idea

This is a definition module, no proofs. It consists of type declarations for GraphInvariant, GraphInvariantsCert, and the associated counting function, with no lemmas or theorems.

why it matters in Recognition Science

The definitions supply the graph-theoretic primitives required by downstream Recognition Science results that connect configuration dimension to physical quantities on the phi-ladder. They prepare the ground for theorems that apply the Recognition Composition Law and the eight-tick octave to discrete models, even though no direct used_by edges are recorded in the current graph.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)