OAI.SignedSweeps.signed_occurrence_moment_bound
OpenThe theorem states that there is a constant η₀>0 such that for every η with 0<η<η₀ there is a κ₀ with 0<κ₀<η/256 such that for every κ with 0<κ<κ₀ there is a positive integer power r, depending only on η and κ, with the following property for every d≥1. Let λ be a partition of 2^d (a Young diagram with 2^d cells), and let u+v+l=2^d with partitions α of u, β of v and γ of l, such that the signed occurrence condition holds: there is an injective complex-linear map from the tensor product of the Specht modules S^α ⊗ S^(β′) ⊗ S^γ, where β′ is the transpose of β, into S^λ that commutes with the action of S_u×S_v×S_l, embedded in S_(2^d) as block permutations on the consecutive blocks of sizes u, v and l. Here Specht modules are the cyclic submodules of the regular representation of the symmetric group generated by the polytabloid built from the row and column subgroups of a fixed tableau. Identify {0,…,2^d−1} with binary strings of length d, and for each coordinate i let the layer operator be the average of S^λ over the subgroup of permutations preserving every binary coordinate except the i-th. Let the sweep operator be the product of these d layer operators in reverse coordinate order, and let the sweep square be TT with T the sweep operator. Define the weighted moment as dim S^λ times the real part of tr((TT)^r). Then the logarithm of this moment, taken as −∞ when the moment is zero, is at most coefficient(η,d)·H(α,β) + remainderBudget(κ,d,l). Here coefficient(a,d)=a(1−1/(2√d)), the signed entropy H(α,β) is the sum, over all row lengths a of α and of β, of a·log((u+v)/a), and the remainder budget is 0 if l=0 and otherwise max(0, coefficient(κ,d)·l·log(2^d) − l·log(2^d/l)).
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/SignedSweepMoment.lean; bytes 6703..7456 -- Kind: theorem; original declaration names and bodies preserved. -- Source groups are independent. Target: Lean 4.33.1; see compilation.json. import Mathlib import Definitions.Def_SignedSweepMoment namespace OAI noncomputable section open scoped BigOperators TensorProduct open Module namespace SignedSweeps
theorem signed_occurrence_moment_bound :
∃ η₀ : ℝ, 0 < η₀ ∧
∀ η : ℝ, 0 < η → η < η₀ →
∃ κ₀ : ℝ, 0 < κ₀ ∧ κ₀ < η / 256 ∧
∀ κ : ℝ, 0 < κ → κ < κ₀ →
∃ r : ℕ, 1 ≤ r ∧
∀ d : ℕ, 1 ≤ d →
∀ lam : Partition (2 ^ d),
∀ (u v l : ℕ) (h : u + v + l = 2 ^ d)
(α : Partition u) (β : Partition v) (γ : Partition l),
SignedOccurrence h α β γ lam →
logMoment (weightedMoment lam r) ≤
((coefficient η d * signedEntropy α β +
remainderBudget κ d l : ℝ) : EReal) := by
sorry
end SignedSweeps
end
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.