module module moderate

`IndisputableMonolith.Foundation.RecognitionOperator`

Defines the recognition operator and the 8-tick ledger carrier: Signal8, LedgerState, bonds, channels, and the neutral register as the mean-free subspace. Foundation consumers cite it for the discrete state space on which the cyclic shift acts. The module is largely definitional scaffolding over the complex structure forced upstream.

claimThe recognition carrier is an 8-tick signal space $\mathrm{Signal}_8$ with ledger states recording time, $Z$-patterns, global phase, channels, and active bonds. The neutral register is the mean-free subspace of this carrier (zero-mean modes under the eight-tick average).

background

Recognition Science forces an eight-tick octave (T7): the fundamental discrete period is $2^3$. Ledger updates act by a cyclic shift on an 8-component carrier. Upstream, Complex Structure Forcing shows that this shift cannot be diagonalized over $\mathbb{R}$, so complexification is algebraically required rather than optional.

This module names the concrete state types sitting on that carrier: signal vectors, bond and agent identifiers, multipliers and positions, channel data, and a global phase. The neutral register is singled out as the mean-free subspace, i.e. the modes orthogonal to the constant (DC) component under the eight-tick average. That subspace is the natural home for zero-mean recognition fluctuations.

Local setting is Foundation: pure kinematic and algebraic structure before dynamics or gravity are attached.

proof idea

This is a definition module, not a theorem chain. It introduces inductive types and structures (Signal8, LedgerState, bond and channel fields) and records the neutral-register convention as the mean-free subspace of the 8-tick carrier. No substantial proof obligations live here; downstream modules import the types and reason about the cyclic shift and cost on them.

why it matters in Recognition Science

UnifiedForcingChain imports this module while assembling T0–T8 as inevitabilities from the cost foundation (RCL). The eight-tick carrier and its shift are the T7 landmark; without named ledger state and neutral register, the forcing chain has no concrete state space.

LedgerSuperposition (Gravity IV) uses the same carrier: it treats Signal8 as a complex Hilbert space and the one-tick update as $\mathbb{C}$-linear, anchoring Theorem 1 (ledger superposition) and the cost-gradient functoriality story. The neutral (mean-free) register is the natural place to host fluctuation modes once the global mean is quotiented or projected out.

Together these edges place RecognitionOperator between complex-structure forcing and both the absolute forcing chain and the quantum-channel gravity layer.

scope and limits

Does not prove T7 or force the eight-tick period; that lives in the forcing chain.
Does not establish complex Hilbert structure or $\mathbb{C}$-linearity of the shift.
Does not define J-cost, RCL, or mass/ladder formulae.
Does not prove dynamical evolution or gravity; only names carrier and register types.
Does not claim uniqueness of the neutral-register decomposition beyond the mean-free convention.

used by (2)

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

IndisputableMonolith.Foundation.UnifiedForcingChain module_import
IndisputableMonolith.Gravity.LedgerSuperposition module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.ComplexStructureForcing module_import

declarations in this module (48)

abbrev Signal8 L13
abbrev BondId L30
abbrev AgentId L31
abbrev LedgerState L32
def time L36
def Z_patterns L37
def global_phase L38
def channels L39
def active_bonds L40
def bond_multipliers L41
def bond_pos L42
def bond_agents L45
def total_Z L49
def RecognitionCost L50
def net_skew L51
def signed_log_flow L52
def reciprocity_skew L53
def reciprocity_skew_abs L54
def admissible L55
def neutralRegister L58
def quarterTurnCore L73
structure StructuredSector L78
def quarterTurnModes L84
lemma mem_quarterTurnModes L87
def quarterTurnSector L92
structure RecognitionOperator L101
def shiftLinear L105
lemma shiftLinear_apply L116
lemma dft_coefficients_add L120
lemma dft_coefficients_smul L126
lemma dft_coefficients_mode L132
lemma dft8_mode_mem_neutralRegister L138
theorem quarterTurnCore_le_neutralRegister L150
def sectorProject L164
lemma sectorProject_apply L199
lemma sectorProject_mode L203
def recognitionUpdate L224
lemma recognitionUpdate_apply L227
def cyclicShiftIter L253
lemma cyclicShiftIter_add L258
lemma cyclicShiftIter_smul L269
lemma cyclicShiftIter_mode L280
lemma odd_mode_fourth_eigenvalue L301
theorem shift_mem_quarterTurnCore L307
theorem shift_four_eq_neg_on_quarterTurnCore L329
theorem twoBeat_square_eq_neg_on_quarterTurnCore L355
theorem sectorProject_eq_id_on_quarterTurnCore L360
theorem recognitionUpdate_eq_shift_on_quarterTurnCore L382