The anchor-resolved suffix sums, and the exact conserved-mode count

This file settles — by explicit arithmetic, before any analysis — the question the central-anchor ledger turns on:

how many of the Green brackets produced by collapsing r324CentralAnchorHarvest sit at the conserved mode α + β?

The set-up

r324Col_piChain_integral evaluates an n-fold Green chain carrying one character per internal coordinate to r324ColPiProp n q, one bracket ⟨·⟩⁻² per suffix sum S_i = q_i + … + q_{n-1}. In the anchor-resolved harvest the momentum at internal slot j of a half chain is

q_j = k_j + α·[j = 0] + β·[j = a],

where k are the free covariance modes of the cross legs and a is the tail anchor of the entity (r324CentralLastAnchor puts a = m - 1). That assignment is r324AnchorKeys.

The count (this is the crux)

r324Anchor_colPartial_eq computes every prefix sum, hence (r324Anchor_suffix_eq) every suffix sum:

S_i = T_i(k) + α·[i = 0] + β·[i ≤ a], T_i(k) = k_i + … + k_{n-1}.

So as an identity in the free keys the conserved mode α + β occurs in exactly one suffix sum, the head one S_0 — and S_0 is precisely the one that momentum conservation annihilates: the closed chain (r324Col_piChain_closed) contributes only on S_0 = 0, where the head bracket is ⟨0⟩⁻² = 1 (r324Anchor_colBrk_zero). This is r324Anchor_head_suffix_zero_of_closed.

On the closed sector the remaining suffix sums read (r324Anchor_suffix_closed)

• 1 ≤ i ≤ a : S_i = -α - P_i(k) — the α family;
• a < i < n : S_i = -(α+β) - P_i(k) — the conserved family,

with P_i(k) = k_0 + … + k_{i-1} a free prefix sum that is summed over. Hence the number of brackets sitting at the conserved mode, up to a free lattice shift, is exactly

#{i | a < i < n} = n - 1 - a (r324Anchor_conservedCount).

Consequences, stated as theorems below.

• For the constant r324CentralLastAnchor (a = n - 1, the dominant term of the anchor resolution) the count is 0 (r324Anchor_lastAnchor_conservedCount): no Green bracket of that harvest sits at α + β. So the candidate mechanism "four Green brackets carry the conserved mode" is refuted; the head bracket, which is the only one that carries α + β freely, is 1.
• Even for the shortcut anchors the count n - 1 - a is not bounded below by 4 (it is ≤ n - 2, and vanishes whenever a = n - 1), so no anchor choice funds ⟨α+β⟩⁻⁸ bracket-by-bracket.

What the brackets can fund

The residual mechanism is the one through the free shifts: on the closed sector P_n(k) = -(α+β), so the keys must sum to the conserved mode, and a large conserved mode forces a large key (r324Anchor_conserved_le_prod_keyBrackets):

1 + ‖α+β‖² ≤ (2^n·n + 1) · ∏_{j<n} (1 + ‖k_j‖²).

Each key bracket ⟨k_j⟩ is in turn bought from two neighbouring chain brackets by Peetre (r324Anchor_key_le_peetre), and every chain bracket is available to at most two keys. So a half chain of n internal coordinates carries n - 1 brackets ⟨·⟩⁻², i.e. 2(n-1) unit powers, of which the telescoping consumes all of them to produce a single power ⟨α+β⟩⁻¹; two half chains give ⟨α+β⟩⁻².

Exact power count: the two half chains of the anchor harvest fund ⟨α+β⟩⁻², and do so only by spending their entire bracket budget. The ledger asks for ⟨α+β⟩⁻⁸ and a surviving |log ε|^{m-1} window sum. The shortfall is six orders. Together with the proved r324Central_epsScale_gap (the ε-scaled symbols miss by ε⁻¹⁶) and r324Central_endpointTrade_sq (the endpoint trade needs ⟨α⟩⁻⁸⟨β⟩⁻⁸ where only ⟨α⟩⁻⁴⟨β⟩⁻⁴ is on the table), all three single mechanisms are now priced, and none of them closes R324CentralAnchorLedger on its own. R324AnchorLedgerAssembly therefore isolates the missing input as one named Prop and assembles everything else.

The anchor-resolved key assignment

def Anderson4D.r324AnchorKeys (α β : Z4) (a : ℕ) (k : ℕ → Z4) : ℕ → Z4

The anchor-resolved momentum assignment of one half chain: the free covariance key k j at every internal slot, plus the head mode α at slot 0 and the tail mode β at the anchor slot a.

Equations

• Anderson4D.r324AnchorKeys α β a k j = (k j + if j = 0 then α else 0) + if j = a then β else 0

theorem Anderson4D.r324AnchorKeys_zero (α β : Z4) {a : ℕ} (ha : 0 < a) : (r324AnchorKeys α β a fun (x : ℕ) => 0) = r324CentralKeys α β a

With k = 0 the anchor keys are the proved two-mode assignment r324CentralKeys.

Every prefix sum, exactly

theorem Anderson4D.r324Anchor_colPartial_eq (α β : Z4) (a : ℕ) (k : ℕ → Z4) (i : ℕ) : r324ColPartial (r324AnchorKeys α β a k) i = (r324ColPartial k i + if 0 < i then α else 0) + if a < i then β else 0

The prefix sums of the anchor keys. α enters as soon as the prefix is nonempty; β enters as soon as the prefix passes the anchor.

Every suffix sum, exactly

def Anderson4D.r324AnchorSuffix (q : ℕ → Z4) (n i : ℕ) : Z4

The suffix sum consumed by the i-th factor of r324ColPiProp.

Equations

• Anderson4D.r324AnchorSuffix q n i = Anderson4D.r324ColPartial (fun (j : ℕ) => q (j + i)) (n - i)

theorem Anderson4D.r324AnchorSuffix_eq_sub (q : ℕ → Z4) {n i : ℕ} (hi : i ≤ n) : r324AnchorSuffix q n i = r324ColPartial q n - r324ColPartial q i

A suffix sum is the difference of two prefix sums.

theorem Anderson4D.r324Anchor_suffix_eq (α β : Z4) {a : ℕ} (k : ℕ → Z4) {n i : ℕ} (hi : i ≤ n) (han : a < n) : r324AnchorSuffix (r324AnchorKeys α β a k) n i = (r324AnchorSuffix k n i + if i = 0 then α else 0) + if i ≤ a then β else 0

The suffix sums of the anchor keys. α occurs in the head suffix only; β occurs in every suffix that starts at or before the anchor.

The head suffix is the conserved mode, and conservation kills it

theorem Anderson4D.r324Anchor_head_suffix (α β : Z4) {a : ℕ} (k : ℕ → Z4) {n : ℕ} (han : a < n) : r324AnchorSuffix (r324AnchorKeys α β a k) n 0 = r324ColPartial k n + (α + β)

Momentum conservation at the head. The head suffix sum of the anchor keys is the total key sum plus the conserved mode α + β.

theorem Anderson4D.r324Anchor_colBrk_zero : r324ColBrk 0 = 1

theorem Anderson4D.r324Anchor_head_suffix_zero_of_closed (α β : Z4) {a : ℕ} (k : ℕ → Z4) {n : ℕ} (_han : a < n) (hclosed : r324ColPartial (r324AnchorKeys α β a k) n = 0) : r324ColBrk (r324AnchorSuffix (r324AnchorKeys α β a k) n 0) = 1

The conserved bracket is 1. The closed chain (r324Col_piChain_closed) contributes only where the total momentum vanishes, i.e. exactly where the unique suffix sum containing α + β freely is zero. So the one Green bracket that sits at the conserved mode is ⟨0⟩⁻² = 1 and carries no decay at all.

theorem Anderson4D.r324Anchor_key_sum_closed (α β : Z4) {a : ℕ} (k : ℕ → Z4) {n : ℕ} (han : a < n) (hclosed : r324ColPartial (r324AnchorKeys α β a k) n = 0) : r324ColPartial k n = -(α + β)

The key sum is minus the conserved mode. This is the only place the conserved mode survives on the closed sector: as the constraint on the free covariance keys.

theorem Anderson4D.r324Anchor_suffix_closed (α β : Z4) {a : ℕ} (k : ℕ → Z4) {n i : ℕ} (hi0 : 0 < i) (hi : i ≤ n) (han : a < n) (hclosed : r324ColPartial (r324AnchorKeys α β a k) n = 0) : r324AnchorSuffix (r324AnchorKeys α β a k) n i = (-if i ≤ a then α else α + β) - r324ColPartial k i

Every non-head suffix sum, on the closed sector. For 1 ≤ i ≤ a the suffix carries -α; for a < i it carries -(α+β). In both cases it is shifted by the free prefix sum P_i(k), which is summed over.

The exact conserved-mode count

theorem Anderson4D.r324Anchor_conservedCount {a n : ℕ} (han : a < n) : {i ∈ Finset.Ico 1 n | a < i}.card = n - 1 - a

The conserved-mode bracket count. On the closed sector the suffix sums that carry the full conserved mode α + β (up to a free lattice shift) are exactly those with index i in (a, n), so there are n - 1 - a of them. (Index 0 is excluded: its bracket is 1.)

theorem Anderson4D.r324Anchor_lastAnchor_conservedCount {n : ℕ} (hn : 0 < n) : {i ∈ Finset.Ico 1 n | n - 1 < i}.card = 0

The last anchor carries no conserved bracket. This is the dominant term of the anchor resolution (r324CentralLastAnchor puts the tail character at slot m - 1), and for it the conserved-mode bracket count is 0: the eighth-order ε-free bracket cannot be read off the Green brackets of this half chain.

theorem Anderson4D.r324Anchor_conservedCount_le {a n : ℕ} (han : a < n) (ha : 0 < a) : {i ∈ Finset.Ico 1 n | a < i}.card ≤ n - 2

No anchor funds eight orders. Both half chains together offer at most 2·(n-2) conserved-mode brackets, i.e. ⟨α+β⟩^{-4(n-2)}, and the count is 0 at the last anchor; in particular the count is not ≥ 4 at the orders n = 2, 3 the capped ledger must cover.

What the brackets do fund: a large key is forced

theorem Anderson4D.r324Anchor_paperModeNormSq_zero : paperModeNormSq 0 = 0

theorem Anderson4D.r324Anchor_paperModeNormSq_nonneg (k : Z4) : 0 ≤ paperModeNormSq k

theorem Anderson4D.r324Anchor_paperModeNormSq_sum_le (n : ℕ) (k : ℕ → Z4) : paperModeNormSq (∑ j ∈ Finset.range n, k j) ≤ 2 ^ n * ∑ j ∈ Finset.range n, paperModeNormSq (k j)

The mode norm of a range sum, with a geometric constant.

theorem Anderson4D.r324Anchor_single_le_prod {n : ℕ} (k : ℕ → Z4) {j : ℕ} (hj : j ∈ Finset.range n) : 1 + paperModeNormSq (k j) ≤ ∏ i ∈ Finset.range n, (1 + paperModeNormSq (k i))

Each summand is dominated by the product of the shifted summands.

theorem Anderson4D.r324Anchor_conserved_le_prod_keyBrackets (n : ℕ) (k : ℕ → Z4) : 1 + paperModeNormSq (r324ColPartial k n) ≤ (2 ^ n * ↑n + 1) * ∏ j ∈ Finset.range n, (1 + paperModeNormSq (k j))

The conserved mode is bought from the key brackets. On the closed sector the free keys must sum to -(α+β), so a large conserved mode forces a large key: the product of the key brackets dominates the conserved bracket, with a geometric constant. This — not any single Green bracket — is the only route from the chain to ⟨α+β⟩⁻¹.

theorem Anderson4D.r324Anchor_key_le_peetre (x y : Z4) : 1 + paperModeNormSq (x - y) ≤ 2 * ((1 + paperModeNormSq x) * (1 + paperModeNormSq y))

Peetre for a key. A single key bracket is bought from the two neighbouring chain brackets: the key is the difference of two consecutive prefix sums, and Peetre's inequality prices that difference.