Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

A full physical bank at the LOWER T prefix

Abstract

A canonical original-source LOWER prefix retains the full b row and exact residual w support.

The arithmetic prefix arguments are reused directly from PrefixArithmetic in M5SourceArithmetic. The row-mask, W_J and T proofs are reused from SourcePrefixInventory on its natural row embedding. The generic source-to-row bridge derives these inputs from OriginalSource, while the least-c full-b selection and residual literal w-mask support remain this module’s own arguments. No M5 a0<=z premise or ten-row terminal completion is transported.

The source is the centered doubling source s(i)=((2^i*t+(2^k-2)/2) mod (2^k-1))-(2^k-2)/2 on all physical labels Fin(k). Advance is iteration of finRotate(k). LARGE means absolute value at least Q. An OwnRow is a proper physical parent row with every literal interior SMALL and its next LARGE terminal. The sorted actual LARGE offsets from x define sourceParent and sourceLength. The complete source predicate below is used without identifying equal values or shortening the physical cycle.

There are m actual LARGE labels of each sign and 2m computed rows. Their half-open chronological arcs partition the physical cycle, with x only as the excluded boundary at row 2m. The final negative parent is 2m-1. Row ten is a boundary only when m=5, and row twelve is a boundary only when m=6. The actual row-eight seed a0 has no upper bound by z here. The nonET witness is literally negative and SMALL on the U-inclusive, x-exclusive tail.

structure OriginalSource (m k t L : ℕ) (a b : ℤ) (p d x : Fin k) : Prop where pairs : 5 ≤ m nonzero : ∀ i : Fin k, actualSource k t i ≠ 0 a_positive : 0 < a minimum_inequalities : a < b ∧ b < 2 * a negative_minimum : ∀ i, actualSource k t i < 0 → a ≤ -actualSource k t i positive_minimum : ∀ i, 0 < actualSource k t i → b ≤ actualSource k t i negative_attained : ∃ i, actualSource k t i = -a positive_attained : ∃ i, actualSource k t i = b p_maximum : ∀ i, actualSource k t i ≤ actualSource k t p d_minimum : ∀ i, actualSource k t d ≤ actualSource k t i positive_count : (Finset.univ.filter (fun i : Fin k => quarter k ≤ actualSource k t i)).card = m negative_count : (Finset.univ.filter (fun i : Fin k => actualSource k t i ≤ -quarter k)).card = m x_positive_large : quarter k ≤ actualSource k t x incoming_d : sourceParent t x 1 = d p_row : OwnRow k t p L x_row_length : sourceLength t x 0 = L d_row_length : sourceLength t x 1 = L beta_row_length : sourceLength t x 2 = L gamma_row_short : sourceLength t x 3 < L c0_hard : 2 * a < modulus k - (2 : ℤ) ^ (L + 1) * a beta_alternative : 2 ≤ L ∨ sourceParent t x 2 ≠ p delta_positive : 0 < b - (modulus k - 2 * actualSource k t x) delta_hard : a - 1 < (((2 : ℤ) ^ (L + 1)) ^ 2 + 1) * (b - (modulus k - 2 * actualSource k t x)) b1_hard : 2 * a - 1 ≤ sourceSeed t x 3 w_bounds : a ≤ modulus k - 2 * actualSource k t (sourceParent t x 4) ∧ modulus k - 2 * actualSource k t (sourceParent t x 4) ≤ 2 * a - 3 w_hard : sourceSeed t x 2 + (b - (modulus k - 2 * actualSource k t x)) < modulus k - 2 * actualSource k t (sourceParent t x 4) w_row_length : sourceLength t x 4 = L - 1 nonET : ∃ i : Fin k, sourceOffset t x 7 ≤ i.val ∧ actualSource k t (advance x i.val) < 0 ∧ |actualSource k t (advance x i.val)| < quarter k u_above_z : modulus k - 2 * actualSource k t x < modulus k - 2 * actualSource k t (sourceParent t x 6) power_branch : ((2 : ℤ) ^ (sourceLength t x 6 + 1) = (2 : ℤ) ^ (L + 1) / 2 ∧ 4 ≤ (2 : ℤ) ^ (L + 1) / 2) ∨ (2 : ℤ) ^ (sourceLength t x 6 + 1) ≤ (2 : ℤ) ^ (L + 1) / 4

For h : OriginalSource m k t L a b p d x, sourceCoordinates h has the following computed coordinates. N=modulus k=2^k-1, Q=quarter k=2^(k-2), C=halfCapacity k=(2^k-2)/2, q=2^L, H=2^(L+1), z=sourceSeed t x 0, n=sourceSeed t x 2, Delta=b-z, b1=sourceSeed t x 3, r=2^(sourceLength t x 3), w=sourceSeed t x 4, v=sourceSeed t x 5, e=2^(sourceLength t x 5), u=sourceSeed t x 6, F=2^(sourceLength t x 6+1), y=sourceSeed t x 7 and a0=sourceSeed t x 8. Every sourceSeed is the absolute value at the actual successor of the computed parent. All powers are integer powers. A mask has weight sum of 2^j.val over its actual finite indices. liftMask hr is the inclusion preserving each index value; hence the complement of liftMask(univ on Fin(r+1)) inside Fin(l) consists exactly of indices at least r+1.

/– Literal physical positions in a computed source row. -/ def sourceMask {k : ℕ} (t : ℕ) (x : Fin k) (i : ℕ) (S : Finset (Fin (sourceLength t x i))) : Finset (Fin k) := S.image (fun j => advance (sourceParent t x i) (j.val + 1)) /– Chronological labels starting with row seven, including its parent U, up to the actual boundary at 2m. The boundary x is excluded. -/ def futureLabels {k : ℕ} (m t : ℕ) (x : Fin k) : Finset (Fin k) := (((List.range (2 * m)).filter (fun i => 7 ≤ i)).flatMap (fun i => sourceParent t x i :: rowLabels (sourceParent t x i) (sourceLength t x i))).toFinset

Theorem 1.1 (The complete source-to-prefix statement).

Lean statement: D5/S3/Combinatorics/Circle/OriginalLowerFullBank.canonical_lower_full_bank

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/OriginalLowerFullBank.canonical_lower_full_bank (✓ std3). ∎

Source. Repository-derived.

Commentary.

theorem canonical_lower_full_bank {m k t L : ℕ} {a b : ℤ} {p d x : Fin k} (h : OriginalSource m k t L a b p d x) (hLower : (2 : ℤ) ^ (sourceLength t x 6 + 1) ≤ (2 : ℤ) ^ (L + 1) / 4) : let D := sourceCoordinates h let s := actualSource k t ∃ (A f : ℤ) (c : ℕ) (Sn : Finset (Fin (sourceLength t x 2))) (Sw : Finset (Fin (sourceLength t x 4))) (Sz : Finset (Fin (sourceLength t x 0))) (word : List (Fin k)), 1 ≤ A ∧ A ≤ D.H / 4 ∧ 0 ≤ f ∧ f ≤ (D.w - 1) / 2 ∧ 2 * f = D.n + D.w + D.Δ - 2 * A * (D.w - D.n) ∧ 2 * (D.w - D.n) * (A - 1) < D.n + D.Δ + 1 ∧ D.n + D.Δ + 1 ≤ 2 * (D.w - D.n) * A ∧ (∑ j ∈ Sn, (2 : ℤ) ^ j.val) = A ∧ (∑ j ∈ Sw, (2 : ℤ) ^ j.val) = D.H / 4 - A ∧ (∑ j ∈ Sz, (2 : ℤ) ^ j.val) = (c : ℤ) ∧ (c : ℤ) ≤ D.q - 1 ∧ (∀ j : ℕ, j < c → A * D.n + (D.H / 4 - A) * D.w - (D.q - 1) * D.b + (j : ℤ) * D.z < (D.u - D.z) / 2) ∧ (let Kfull := sourceMask t x 2 Sn ∪ sourceMask t x 4 Sw ∪ sourceMask t x 1 Finset.univ ∪ sourceMask t x 0 Sz ∪ sourceMask t x 6 Finset.univ let Dold := A * D.n + (D.H / 4 - A) * D.w - (D.q - 1) * D.b (D.u - D.z) / 2 ≤ Dold + (c : ℤ) * D.z ∧ Dold + (c : ℤ) * D.z ≤ D.u - (D.z + 1) / 2 ∧ word.Nodup ∧ word.head? = some x ∧ (∀ j : ℕ, 0 ≤ ((word.take j).map (s)).sum ∧ ((word.take j).map (s)).sum ≤ halfCapacity k) ∧ Disjoint word.toFinset Kfull ∧ word.toFinsetᶜ = Kfull ∪ futureLabels m t x ∧ Disjoint Kfull (futureLabels m t x) ∧ 2 * ((word.map (s)).sum + ∑ i ∈ Kfull, s i) = D.z + D.y ∧ (D.e = 1 → 4 ≤ D.F → D.y ≤ 2 * b - 3 → ∃ (hr : sourceLength t x 6 < sourceLength t x 4) (Slow : Finset (Fin (sourceLength t x 4))), (∑ j ∈ Slow, (2 : ℤ) ^ j.val) = (2 : ℤ) ^ sourceLength t x 6 - A ∧ (∀ j ∈ Slow, j.val < sourceLength t x 6) ∧ Disjoint Slow {⟨sourceLength t x 6, hr⟩} ∧ Sw = (liftMask (Nat.succ_le_of_lt hr) Finset.univ)ᶜ ∪ {⟨sourceLength t x 6, hr⟩} ∪ Slow ∧ sourceMask t x 4 Slow ⊆ Kfull ∧ advance (sourceParent t x 4) (sourceLength t x 6 + 1) ∈ Kfull ∧ (2 ≤ A → Sw ≠ Finset.univ)))

Let G=H/4 and K=w-n. The canonical coefficient A is the unique integer with 2K(A-1)<n+Delta+1<=2KA. The retained n and w masks have weights A and G-A. Their complements, together with the entire positive row after gamma, form the specified first SMALL batch. Its legal ordering and the separate gamma, P and J steps give the canonical W_J prefix at height Z>0. Every SMALL batch has absolute values at most Q-1 and legal endpoints; its individual steps are supplied by the finite SMALL ordering theorem.

Set Dold=A*n+(G-A)*w-(q-1)b and ell=(u-z)/2. The coefficient c is the least natural number with ell<=Dold+cz. The source gives Dold<b and Dold+(q-1)*z=Z+ell+(e-1)*v>ell. Thus c<=q-1. If c>0, minimality gives compensation below ell+z; if c=0, Dold2b give the same upper gate. The retained set is exactly the n mask, the w mask, the entire b row and the z mask of coefficient c. No u label is prepaid. The batch spent before T is exactly the complementary z mask and the entire v row, including every positive v cost.

The theorem constructs a physical prefix containing T, beginning with x, with no repeated physical label and with every natural take sum in the original strip. Its complement is exactly Kfull together with the chronological future beginning at U. Kfull retains the whole u row as well as the new keep. The doubled charge equation is an equality for those literal sets. It supplies the initial physical inventory for the subsequent first-selector construction.

In the residual e=1, F>=4, y<=2b-3, put tau=F/2 and eta=Fw-(F+1)b. The source recurrence gives Heta=(F+1)n-y>0, and F(w-n)=b+eta+FH*Delta>n+Delta+1. Canonical minimality therefore gives A<=tau. Binary-mask injectivity identifies the retained w mask with its disjoint high part, its single tau bit and its low mask of weight tau-A. Both the low mask and that exact physical tau occurrence lie in Kfull. A>=2 makes the w mask genuinely depleted; A=1 gives the full mask.

The setting is the circle configuration problem of Damasdi, Frankl, Pach and Palvolgyi, Monochromatic configurations on a circle, arXiv:2504.10687v2, Conjecture 3.1, DOI 10.5070/C6.68671. This local LOWER prefix does not assert a complete ordering of the unused tail or integer-zero completion. The half-power branch, subsequent first-selector gates, arbitrary-tail survival and original normalization require further results. The cyclic action and its integer coboundary conserve the sum on all original labels; scalar ties, nonunits, short numerical orbits, shifts and repetitions preserve separate physical occurrences.

References