eight_tick_neutral_implies_exact
plain-language theorem explainer
Neutral eight-tick windows admit an integer-valued potential φ such that signed differences between any two positions equal the corresponding potential differences. Ledger-exactness work in Recognition Science cites the result to connect window neutrality directly to exact potentials. The term proof constructs φ explicitly as the signed value at index zero and discharges the equality by simplification.
Claim. Let $w$ be a neutral window of length 8. Then there exists a map $φ$ from 8-patterns to integers such that for all positions $i,j$, the difference between the signed indicator at $j$ and the signed indicator at $i$ equals $φ$ of the constant pattern carrying the value at $j$ minus $φ$ of the constant pattern carrying the value at $i$.
background
The module axiomatizes the link between eight-tick neutrality and ledger exactness, with an explicit extension to the gap weight $w_8$ that enters the $α^{-1}$ derivation. Pattern 8 denotes binary sequences of length 8; isNeutralWindow encodes the neutrality constraint on such a sequence. The eight-tick structure itself originates in the fundamental octave period of 8 ticks, with $w_8$ supplied by the closed-form expression in Constants.GapWeight.w8_from_eight_tick.
proof idea
The proof is a direct term construction. It defines $φ$ to return the signed value of its argument at position 0, then applies use and simp to verify that the position-wise signed differences match the potential differences.
why it matters
The result supplies the existence half of the connection from eight-tick neutrality to the unique gap weight $w_8$ used in the $α^{-1}$ band. It sits inside the T7 eight-tick octave and feeds the scheduler invariants (sumFirst8, blockSumAligned8) that fix $w_8$ from T6 minimality. The module doc states that the neutrality constraints uniquely determine this weight.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.