neutralWindow
neutralWindow constructs a Window8 by placing each of four LedgerEvents in two consecutive slots, once as itself and once as its conjugate. Algebraists verifying double-entry conservation in the Recognition ledger cite this to produce balanced 8-event blocks. The definition proceeds by direct case analysis on the Fin 8 index with no auxiliary lemmas.
claimGiven four ledger events $e_1,e_2,e_3,e_4$ (signed integer flows with positive values as debits), define the window $w$ by $w(0)=e_1$, $w(1)=-e_1$, $w(2)=e_2$, $w(3)=-e_2$, $w(4)=e_3$, $w(5)=-e_3$, $w(6)=e_4$, $w(7)=-e_4$.
background
LedgerEvent is a signed integer flow on an edge (positive = debit, negative = credit) carrying the additive group structure of the integers; its conjugate is negation, so that $e + (-e) = 0$. Window8 packages eight such events indexed by Fin 8 together with a sum operation that totals the flows and an isNeutral predicate that holds precisely when the sum vanishes. The definition appears inside the LedgerAlgebra module, which assembles the basic group and pairing properties of the ledger before the graded ledger is introduced; it depends only on the LedgerEvent and Window8 structures.
proof idea
The definition is a direct structural construction: it matches on the Fin 8 index and assigns the four input events to positions 0-1, 2-3, 4-5 and 6-7, each paired with its conjugate. No lemmas or tactics are applied; the body is simply the explicit function definition.
why it matters in Recognition Science
The construction supplies the concrete neutral window required by the ledger algebra certificate, which lists eight-window neutrality from four paired events as one of its six verified properties. It realizes the eight-tick octave algebraically and is invoked by the immediate downstream theorem neutralWindow_isNeutral that proves the sum is zero. The definition therefore closes the algebraic step that precedes the graded ledger and conservation statements.
scope and limits
- Does not assign concrete numerical flow values.
- Does not prove that the constructed window sums to zero.
- Does not generalize to windows of length other than eight.
- Does not reference the phi-ladder or physical constants.
formal statement (Lean)
123def neutralWindow (e₁ e₂ e₃ e₄ : LedgerEvent) : Window8 where
124 events := fun i =>
proof body
Definition body.
125 match i with
126 | ⟨0, _⟩ => e₁
127 | ⟨1, _⟩ => e₁.conj
128 | ⟨2, _⟩ => e₂
129 | ⟨3, _⟩ => e₂.conj
130 | ⟨4, _⟩ => e₃
131 | ⟨5, _⟩ => e₃.conj
132 | ⟨6, _⟩ => e₄
133 | ⟨7, _⟩ => e₄.conj
134
135/-- **PROVED: A window of paired events is neutral.** -/