pith. machine review for the scientific record. sign in
abbrev definition def or abbrev high

CoupledCoreIndex

show as:
view Lean formalization →

CoupledCoreIndex(N) is the type of all functions assigning one of four states to each of N sites, serving as the configuration space for coupled ququart cores. Researchers constructing finite-dimensional models of recognition systems cite it when defining basis vectors and displacement operators. The declaration is introduced as a direct type abbreviation with no proof obligations or lemmas.

claimFor a natural number $N$, the configuration space of $N$ coupled ququart cores is the set of all functions from a set of $N$ sites to a 4-element set of states.

background

In this module ququart states denote four-level systems, with sibling definitions supplying operators analogous to Pauli matrices on those levels. The index type supplies the discrete labeling for configurations of multiple such cores at finite sites. Upstream results include structures describing nuclear densities on phi-tiers and carrier frequencies fixed at 5 phi Hz, together with the J-cost structure from PhiForcingDerived; these establish the discrete, phi-scaled setting in which the configuration space is placed.

proof idea

This is a one-line abbreviation that directly sets the configuration space equal to the function type from Fin N to Fin 4.

why it matters in Recognition Science

The definition supplies the indexing type used by addedConfig, coupledBasisKet, and the orthonormal-basis theorem in the same module. It thereby supports the finite-site Hilbert-space construction that feeds into the Recognition framework's discrete models, consistent with the phi-ladder and eight-tick octave landmarks. No open scaffolding is closed here; the type is a prerequisite for later operator definitions.

scope and limits

formal statement (Lean)

 117abbrev CoupledCoreIndex (N : ℕ) := Fin N → Fin 4

proof body

Definition body.

 118
 119/-- The concrete Hilbert carrier of `N` coupled recognition cores. -/

used by (29)

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

depends on (8)

Lean names referenced from this declaration's body.