Large normalized quotients with a small nonzero increment exclude density above five eighths
ProvedLongWagnerLargeNonzeroQuotients.large_nonzero_actual_exclusionadditive-combinatoricscombinatoricscyclic-groupsfibre-countinglong-wagner-auxiliarylong-wagner-five-eighths-20261003
Let , put and , and assume
Let be the canonical reduction map and let modulo .
Let be projective cube-free, with repeated cube generators allowed, and let . For , the conditions
imply a contradiction. The statement does not require .
This auxiliary lemma closes the large nonzero quotient branch. The source-mass and interval-packing estimates in its proof actually yield the strict inequality from the first three displayed link conditions and the preceding numerical hypotheses. The final density hypothesis therefore contradicts that proved bound. The small-increment condition is explicit here and is established separately during the global assembly.
Preamble
/-
Standalone source for the exact original Long-Wagner target.
No local LongWagner imports remain.
Prominent upstream modification notice:
The Kneser and finset-stabilizer portions are by Mantas Bakšys and
Yaël Dillies, copyright 2023, released under Apache 2.0. Upstream:
https://github.com/YaelDillies/misc-yd at commit
cd12c538d66f15a358a6904e7c847cd67661096f. They were ported from
Lean 4.35.0-rc3 to 4.33.1 by removing module/public headers, changing
the local import, and appending diagnostics. Standalone packaging
removes local imports and concatenates isolated sections. The
upstream theorem statements and proofs are unchanged. Original
copyright/authors headers are retained in the body.
Full upstream Apache 2.0 license follows:
Apache License
Version 2.0, January 2004
http://www.apache.org/licenses/
TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
1. Definitions.
"License" shall mean the terms and conditions for use, reproduction,
and distribution as defined by Sections 1 through 9 of this document.
"Licensor" shall mean the copyright owner or entity authorized by
the copyright owner that is granting the License.
"Legal Entity" shall mean the union of the acting entity and all
other entities that control, are controlled by, or are under common
control with that entity. For the purposes of this definition,
"control" means (i) the power, direct or indirect, to cause the
direction or management of such entity, whether by contract or
otherwise, or (ii) ownership of fifty percent (50%) or more of the
outstanding shares, or (iii) beneficial ownership of such entity.
"You" (or "Your") shall mean an individual or Legal Entity
exercising permissions granted by this License.
"Source" form shall mean the preferred form for making modifications,
including but not limited to software source code, documentation
source, and configuration files.
"Object" form shall mean any form resulting from mechanical
transformation or translation of a Source form, including but
not limited to compiled object code, generated documentation,
and conversions to other media types.
"Work" shall mean the work of authorship, whether in Source or
Object form, made available under the License, as indicated by a
copyright notice that is included in or attached to the work
(an example is provided in the Appendix below).
"Derivative Works" shall mean any work, whether in Source or Object
form, that is based on (or derived from) the Work and for which the
editorial revisions, annotations, elaborations, or other modifications
represent, as a whole, an original work of authorship. For the purposes
of this License, Derivative Works shall not include works that remain
separable from, or merely link (or bind by name) to the interfaces of,
the Work and Derivative Works thereof.
"Contribution" shall mean any work of authorship, including
the original version of the Work and any modifications or additions
to that Work or Derivative Works thereof, that is intentionally
submitted to Licensor for inclusion in the Work by the copyright owner
or by an individual or Legal Entity authorized to submit on behalf of
the copyright owner. For the purposes of this definition, "submitted"
means any form of electronic, verbal, or written communication sent
to the Licensor or its representatives, including but not limited to
communication on electronic mailing lists, source code control systems,
and issue tracking systems that are managed by, or on behalf of, the
Licensor for the purpose of discussing and improving the Work, but
excluding communication that is conspicuously marked or otherwise
designated in writing by the copyright owner as "Not a Contribution."
"Contributor" shall mean Licensor and any individual or Legal Entity
on behalf of whom a Contribution has been received by Licensor and
subsequently incorporated within the Work.
2. Grant of Copyright License. Subject to the terms and conditions of
this License, each Contributor hereby grants to You a perpetual,
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
copyright license to reproduce, prepare Derivative Works of,
publicly display, publicly perform, sublicense, and distribute the
Work and such Derivative Works in Source or Object form.
3. Grant of Patent License. Subject to the terms and conditions of
this License, each Contributor hereby grants to You a perpetual,
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
(except as stated in this section) patent license to make, have made,
use, offer to sell, sell, import, and otherwise transfer the Work,
where such license applies only to those patent claims licensable
by such Contributor that are necessarily infringed by their
Contribution(s) alone or by combination of their Contribution(s)
with the Work to which such Contribution(s) was submitted. If You
institute patent litigation against any entity (including a
cross-claim or counterclaim in a lawsuit) alleging that the Work
or a Contribution incorporated within the Work constitutes direct
or contributory patent infringement, then any patent licenses
granted to You under this License for that Work shall terminate
as of the date such litigation is filed.
4. Redistribution. You may reproduce and distribute copies of the
Work or Derivative Works thereof in any medium, with or without
modifications, and in Source or Object form, provided that You
meet the following conditions:
(a) You must give any other recipients of the Work or
Derivative Works a copy of this License; and
(b) You must cause any modified files to carry prominent notices
stating that You changed the files; and
(c) You must retain, in the Source form of any Derivative Works
that You distribute, all copyright, patent, trademark, and
attribution notices from the Source form of the Work,
excluding those notices that do not pertain to any part of
the Derivative Works; and
(d) If the Work includes a "NOTICE" text file as part of its
distribution, then any Derivative Works that You distribute must
include a readable copy of the attribution notices contained
within such NOTICE file, excluding those notices that do not
pertain to any part of the Derivative Works, in at least one
of the following places: within a NOTICE text file distributed
as part of the Derivative Works; within the Source form or
documentation, if provided along with the Derivative Works; or,
within a display generated by the Derivative Works, if and
wherever such third-party notices normally appear. The contents
of the NOTICE file are for informational purposes only and
do not modify the License. You may add Your own attribution
notices within Derivative Works that You distribute, alongside
or as an addendum to the NOTICE text from the Work, provided
that such additional attribution notices cannot be construed
as modifying the License.
You may add Your own copyright statement to Your modifications and
may provide additional or different license terms and conditions
for use, reproduction, or distribution of Your modifications, or
for any such Derivative Works as a whole, provided Your use,
reproduction, and distribution of the Work otherwise complies with
the conditions stated in this License.
5. Submission of Contributions. Unless You explicitly state otherwise,
any Contribution intentionally submitted for inclusion in the Work
by You to the Licensor shall be under the terms and conditions of
this License, without any additional terms or conditions.
Notwithstanding the above, nothing herein shall supersede or modify
the terms of any separate license agreement you may have executed
with Licensor regarding such Contributions.
6. Trademarks. This License does not grant permission to use the trade
names, trademarks, service marks, or product names of the Licensor,
except as required for reasonable and customary use in describing the
origin of the Work and reproducing the content of the NOTICE file.
7. Disclaimer of Warranty. Unless required by applicable law or
agreed to in writing, Licensor provides the Work (and each
Contributor provides its Contributions) on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
implied, including, without limitation, any warranties or conditions
of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
PARTICULAR PURPOSE. You are solely responsible for determining the
appropriateness of using or redistributing the Work and assume any
risks associated with Your exercise of permissions under this License.
8. Limitation of Liability. In no event and under no legal theory,
whether in tort (including negligence), contract, or otherwise,
unless required by applicable law (such as deliberate and grossly
negligent acts) or agreed to in writing, shall any Contributor be
liable to You for damages, including any direct, indirect, special,
incidental, or consequential damages of any character arising as a
result of this License or out of the use or inability to use the
Work (including but not limited to damages for loss of goodwill,
work stoppage, computer failure or malfunction, or any and all
other commercial damages or losses), even if such Contributor
has been advised of the possibility of such damages.
9. Accepting Warranty or Additional Liability. While redistributing
the Work or Derivative Works thereof, You may choose to offer,
and charge a fee for, acceptance of support, warranty, indemnity,
or other liability obligations and/or rights consistent with this
License. However, in accepting such obligations, You may act only
on Your own behalf and on Your sole responsibility, not on behalf
of any other Contributor, and only if You agree to indemnify,
defend, and hold each Contributor harmless for any liability
incurred by, or claims asserted against, such Contributor by reason
of your accepting any such warranty or additional liability.
END OF TERMS AND CONDITIONS
APPENDIX: How to apply the Apache License to your work.
To apply the Apache License to your work, attach the following
boilerplate notice, with the fields enclosed by brackets "[]"
replaced with your own identifying information. (Don't include
the brackets!) The text should be enclosed in the appropriate
comment syntax for the file format. We also recommend that a
file or class name and description of purpose be included on the
same "printed page" as the copyright notice for easier
identification within third-party archives.
Copyright [yyyy] [name of copyright owner]
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import Mathlib
import Definitions.Def_Z2nCubeFreeLayers
import Lean.Elab.Tactic.Omega
/- Source: LongWagnerHPPreparation; SHA256 d7655889ea09a9877be94335035bf63c8e42986bbe67bcb1a742aad68beb2d25. -/
import Definitions.Def_LongWagnerInfrastructure20261003
import Theorems.Thm_LongWagnerQuotientIntervals_actual_source_packing
Formal statement
section LongWagnerStandaloneBody0
open scoped Pointwise
namespace LongWagnerHPPreparation
variable {G : Type*} [AddCommGroup G]
end LongWagnerHPPreparation
end LongWagnerStandaloneBody0
/- Source: LongWagnerLargeSumFreeElementary; SHA256 3c01d8d4efaf415ae3aadbb561e40363046f10d6ddfd960c47dced270a76fe6b. -/
section LongWagnerStandaloneBody1
open scoped Pointwise
namespace LongWagnerLargeSumFreeElementary
variable {G : Type*} [AddCommGroup G] [DecidableEq G]
end LongWagnerLargeSumFreeElementary
end LongWagnerStandaloneBody1
/- Source: LongWagnerHPQuotientElementary; SHA256 bc52b50202c46fa79b5fa92cf42dfb7b7ab53b99afbd8ba8526bf297a87968a5. -/
section LongWagnerStandaloneBody2
open scoped Pointwise
namespace LongWagnerHPQuotientElementary
variable {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G]
end LongWagnerHPQuotientElementary
end LongWagnerStandaloneBody2
/- Source: LongWagnerImportedKneser.MulStab; SHA256 244905adac51ee094709027794c2830159412a56c0df5b5a8bbe9f2fd32fa1b8. -/
section LongWagnerStandaloneBody3
/-
Copyright (c) 2023 Mantas Bakšys, Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mantas Bakšys, Yaël Dillies
-/
/-!
# Stabilizer of a finset
This file defines the stabilizer of a finset of a group as a finset.
## Main declarations
* `Finset.mulStab`: The stabilizer of a **nonempty** finset as a finset.
-/
open Function MulAction
open scoped Pointwise
namespace Finset
variable {ι α : Type*}
local notation s " +ₛ " N => Finset.image ((↑) : α → α ⧸ N) s
local notation s " +ˢ " N => Set.image ((↑) : α → α ⧸ N) s
section Group
variable [Group α] [DecidableEq α] {s t : Finset α} {a : α}
end Group
variable [CommGroup α] [DecidableEq α] {s t : Finset α} {a : α}
end Finset
end LongWagnerStandaloneBody3
/- Source: LongWagnerImportedKneser.Kneser; SHA256 dac47e55af0f8ee24ae03e34fd542652322cf0eb5579a5fce904e1681b259e61. -/
section LongWagnerStandaloneBody4
/-
Copyright (c) 2023 Mantas Bakšys, Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mantas Bakšys, Yaël Dillies
-/
/-!
# Kneser's addition theorem
This file proves Kneser's theorem. This states that `|s + H| + |t + H| - |H| ≤ |s + t|` where `s`,
`t` are finite nonempty sets in a commutative group and `H` is the stabilizer of `s + t`. Further,
if the inequality is strict, then we in fact have `|s + H| + |t + H| ≤ |s + t|`.
## Main declarations
* `Finset.mul_kneser`: Kneser's theorem.
* `Finset.mul_strict_kneser`: Strict Kneser theorem.
## References
* [Imre Ruzsa, *Sumsets and structure*][ruzsa2009]
* Matt DeVos, *A short proof of Kneser's addition theorem*
-/
open Function MulAction
open scoped Pointwise
variable {α : Type*} [CommGroup α] [DecidableEq α] {s s' t t' C : Finset α} {a b : α}
namespace Finset
/-! ### Auxiliary results -/
/-! ### Kneser's theorem -/
variable (s t)
end Finset
end LongWagnerStandaloneBody4
/- Source: LongWagnerQuotientCounting; SHA256 e4a58ee08a07e53119f311ade1560a48bdfef3fac7bd84053815d6cba5bb446b. -/
section LongWagnerStandaloneBody5
open scoped Pointwise
namespace LongWagnerQuotientCounting
end LongWagnerQuotientCounting
end LongWagnerStandaloneBody5
/- Source: LongWagnerKneserQuotient; SHA256 83d9c53110041c11bed85f1b95f48798148a3bd32619e7dff321e80c5f2cd6eb. -/
section LongWagnerStandaloneBody6
open scoped Pointwise
namespace LongWagnerKneserQuotient
variable {G : Type*} [AddCommGroup G] [DecidableEq G]
end LongWagnerKneserQuotient
end LongWagnerStandaloneBody6
/- Source: LongWagnerCriticalQuotient; SHA256 2e31dea2b70d4b3a49bc6956562e5e4aced3962071515f352682029426ac7700. -/
section LongWagnerStandaloneBody7
open scoped Pointwise
namespace LongWagnerCriticalQuotient
variable {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G]
end LongWagnerCriticalQuotient
end LongWagnerStandaloneBody7
/- Source: LongWagnerQuotientTransport; SHA256 71a85b9f0cfe19077123cb2a580c59c81715334eae7d05058e891ba7a4ae22a7. -/
section LongWagnerStandaloneBody8
open scoped Pointwise
namespace LongWagnerQuotientTransport
variable {G K : Type*} [AddCommGroup G] [AddCommGroup K]
end LongWagnerQuotientTransport
end LongWagnerStandaloneBody8
/- Source: LongWagnerAtomCounting; SHA256 fc2cd7b1d1d98ac368c681e046974c25f53609fb64ffd92e8fdecc8a2f6ac699. -/
section LongWagnerStandaloneBody9
open scoped Pointwise
namespace LongWagnerAtomCounting
variable {G : Type*} [AddCommGroup G] [DecidableEq G] [Fintype G]
end LongWagnerAtomCounting
end LongWagnerStandaloneBody9
/- Source: LongWagnerSingleRun; SHA256 748637a96fdea0a18d4e6176d8db847adb84217e835e4a447f552573b556345e. -/
section LongWagnerStandaloneBody10
open scoped Pointwise
namespace LongWagnerSingleRun
variable {G : Type*} [AddCommGroup G] [DecidableEq G]
end LongWagnerSingleRun
end LongWagnerStandaloneBody10
/- Source: LongWagnerCyclicInterval; SHA256 fe832c459527a208a9bc20c79d0a39cf23e9904dfd27c1d754f44fda4f392a8a. -/
section LongWagnerStandaloneBody11
namespace LongWagnerCyclicInterval
end LongWagnerCyclicInterval
end LongWagnerStandaloneBody11
/- Source: LongWagnerSingleRunAP; SHA256 b1421338b9ca07afc5634d8965d15008bc5d1238d2b41de49decf37267c9cef0. -/
section LongWagnerStandaloneBody12
open scoped Pointwise
namespace LongWagnerSingleRunAP
variable {G : Type*} [AddCommGroup G] [DecidableEq G] [Fintype G]
end LongWagnerSingleRunAP
end LongWagnerStandaloneBody12
/- Source: LongWagnerDyadicExpansion; SHA256 161c79f04c5423917e502bfd272473a873ba7cd764c787a7bac95c5149c0563d. -/
section LongWagnerStandaloneBody13
open scoped Pointwise
namespace LongWagnerDyadicExpansion
variable {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G]
end LongWagnerDyadicExpansion
end LongWagnerStandaloneBody13
/- Source: LongWagnerIntervalNormalization; SHA256 ec9149d6f35e6271eb5418315c83ab0248c8a5b4447a43d7ecb4a9203139488f. -/
section LongWagnerStandaloneBody14
open scoped Pointwise
namespace LongWagnerIntervalNormalization
end LongWagnerIntervalNormalization
end LongWagnerStandaloneBody14
/- Source: LongWagnerTwoPointClassification; SHA256 df238e2418fc4f285c6a31da6efd1df817fdb38e137253a9f82abd2a30898416. -/
section LongWagnerStandaloneBody15
open scoped Pointwise
namespace LongWagnerTwoPointClassification
variable {G : Type*} [AddCommGroup G] [DecidableEq G] [Fintype G]
end LongWagnerTwoPointClassification
end LongWagnerStandaloneBody15
/- Source: LongWagnerAtomStructure; SHA256 41d802cbbee1d371ad12e7988709213a187631d15835a41358cfc6e13d9760a3. -/
section LongWagnerStandaloneBody16
open scoped Pointwise
namespace LongWagnerAtomStructure
open LongWagnerAtomCounting
variable {G : Type*} [AddCommGroup G] [DecidableEq G] [Fintype G]
end LongWagnerAtomStructure
end LongWagnerStandaloneBody16
/- Source: LongWagnerAtomBoundary; SHA256 8c6c38c88a2b46abf249c420deb55818b01a090986f57fec07440e5720643ef6. -/
section LongWagnerStandaloneBody17
open scoped Pointwise
namespace LongWagnerAtomBoundary
open LongWagnerAtomCounting
variable {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G]
end LongWagnerAtomBoundary
end LongWagnerStandaloneBody17
/- Source: LongWagnerAtomSeed; SHA256 4896909bc2f177caf24a8a1fa3c2b58d92081d1751e7f5bff61adfbec6e3c075. -/
section LongWagnerStandaloneBody18
open scoped Pointwise
namespace LongWagnerAtomSeed
open LongWagnerAtomCounting
variable {G : Type*} [AddCommGroup G] [DecidableEq G] [Fintype G]
end LongWagnerAtomSeed
end LongWagnerStandaloneBody18
/- Source: LongWagnerTwoPointAtom; SHA256 0a974c5e0a65a32118488cf93fe3da19ec033428c72b16267af93e8ca4e268cd. -/
section LongWagnerStandaloneBody19
open scoped Pointwise
namespace LongWagnerTwoPointAtom
open LongWagnerAtomCounting LongWagnerAtomStructure LongWagnerAtomBoundary
variable {G : Type*} [AddCommGroup G] [DecidableEq G] [Fintype G]
end LongWagnerTwoPointAtom
end LongWagnerStandaloneBody19
/- Source: LongWagnerCriticalClassification; SHA256 06494642f10d77af0a3a42e35c4e456731b432e1f98b23049c442f870c7cdab3. -/
section LongWagnerStandaloneBody20
open scoped Pointwise
namespace LongWagnerCriticalClassification
end LongWagnerCriticalClassification
end LongWagnerStandaloneBody20
/- Source: LongWagnerLinks; SHA256 2a673cfea0314ee7de880b8a5f3ea4cc39fb83f05533ad249b82f5ad1ef6b5d9. -/
section LongWagnerStandaloneBody21
open scoped BigOperators
open Z2nFiveEighths
set_option autoImplicit false
namespace LongWagnerTools
section Links
variable {G : Type*} [AddCommGroup G] [DecidableEq G]
end Links
section HomPreimage
variable {G H : Type*} [AddCommGroup G] [AddCommGroup H]
variable [Fintype G] [DecidableEq H]
end HomPreimage
end LongWagnerTools
end LongWagnerStandaloneBody21
/- Source: LongWagnerThreeLayersNormalization; SHA256 68bec5fafd011c08c27ff9201066b06af9c754d6aa815bcc15ee0b82f78e0e74. -/
section LongWagnerStandaloneBody22
open Z2nFiveEighths LongWagnerTools
set_option autoImplicit false
namespace LongWagnerNormalization
section AdditiveEquivalence
variable {G H : Type*} [AddCommGroup G] [AddCommGroup H]
variable [DecidableEq H]
end AdditiveEquivalence
section UnitScaling
variable {R : Type*} [CommRing R] [DecidableEq R]
end UnitScaling
end LongWagnerNormalization
end LongWagnerStandaloneBody22
/- Source: LongWagnerHighOdd; SHA256 72647bccee01e61e93f6874fc701e5cbeacfbec30587d40ede6ccc9fe76a6386. -/
section LongWagnerStandaloneBody23
/-!
# Long–Wagner: the high-odd-density branch
This file proves the original 5/8 cardinal bound when more than three quarters
of the odd coset belongs to the cube-free set. It imports the actual platform
cube definition through `LongWagnerLinks`, permits repeated cube generators,
and assumes no instance of the universal Long–Wagner conjecture.
The remaining odd-density regimes are outside this file.
-/
open scoped BigOperators
open Z2nFiveEighths LongWagnerTools
set_option autoImplicit false
namespace LongWagnerHighOdd
section FiniteCounting
variable {G : Type*} [AddCommGroup G] [DecidableEq G]
end FiniteCounting
end LongWagnerHighOdd
end LongWagnerStandaloneBody23
/- Source: LongWagnerFibreBounds; SHA256 ecd2a285993cb40e54a5e02f61f552a2913ab0512c17805d22da4a613f2a79ce. -/
section LongWagnerStandaloneBody24
/-!
# Actual dyadic fibres and unconditional diagonal cube inequalities
The quotient has modulus2^(p+1), and each fibre has size2^k. Definitions
use the genuine cyclic reduction homomorphism. No classification is assumed.
-/
open Z2nFiveEighths LongWagnerTools LongWagnerHighOdd
open scoped Pointwise
set_option autoImplicit false
namespace LongWagnerFibreBounds
end LongWagnerFibreBounds
end LongWagnerStandaloneBody24
/- Source: LongWagnerSmallDifference; SHA256 c6d163a48d7aed3ffe4c35b4959d94e7f5db927dc285251ed3a860bbc36ea1ae. -/
section LongWagnerStandaloneBody25
open scoped Pointwise
set_option autoImplicit false
namespace LongWagnerSmallDifference
variable {G : Type*} [AddCommGroup G] [DecidableEq G]
end LongWagnerSmallDifference
end LongWagnerStandaloneBody25
/- Source: LongWagnerBonferroni; SHA256 fd5dd16b3fbf0d8f204b472120587b90e97439e73efdfd7a3b142256790d8ebd. -/
section LongWagnerStandaloneBody26
namespace LongWagner
variable {α : Type*} [DecidableEq α]
end LongWagner
end LongWagnerStandaloneBody26
/- Source: LongWagnerBridge; SHA256 c131691aa065c22957f0ab7a7e9e769e351d9d34227b24a6764314b0827dfb0f. -/
section LongWagnerStandaloneBody27
/-!
# Verified five-eighths closing bridge with one visible paper proposition
This file proves the complete graph/difference-set closing argument for the
actual Prove2Me cyclic groups and CubeFree definition. The mathematical
classification needed to prove AllSelectedLinkCaps is not formalized here.
Consequently the final theorem is conditional on that explicit proposition;
it is not an unconditional formal proof of the old open root.
-/
open scoped Pointwise
set_option autoImplicit false
namespace LongWagnerBridge
open LongWagnerTools LongWagnerSmallDifference
variable {G : Type*} [AddCommGroup G] [DecidableEq G]
end LongWagnerBridge
end LongWagnerStandaloneBody27
/- Source: LongWagnerFibreAnalytic; SHA256 d6376af1d7c5fd6961ef16a14c30654fae1d4d0e88ccee19340eb194c2570e09. -/
section LongWagnerStandaloneBody28
/-!
# Actual link fibre masses and semantic inequalities
All inequalities concern genuine finite subsets of the dyadic cyclic group.
The normalized quotient container is an explicit assumption; its existence
and interval shape are not supplied by this file.
-/
open Z2nFiveEighths LongWagnerTools LongWagnerFibreBounds LongWagnerBridge
set_option autoImplicit false
namespace LongWagnerFibreAnalytic
end LongWagnerFibreAnalytic
end LongWagnerStandaloneBody28
/- Source: LongWagnerFibreNormalization; SHA256 fd526c3348795ffbe1be3ce9f52971c4acf11fd3db43774de0b676411a7609cc. -/
section LongWagnerStandaloneBody29
open scoped Pointwise
namespace LongWagnerFibreNormalization
open LongWagnerTools LongWagnerNormalization LongWagnerFibreBounds LongWagnerFibreAnalytic
open Z2nFiveEighths
variable {G H : Type*} [AddCommGroup G] [AddCommGroup H] [DecidableEq G] [DecidableEq H]
end LongWagnerFibreNormalization
end LongWagnerStandaloneBody29
/- Source: LongWagnerFiniteFibreCertificates; SHA256 ddababde44ec88316bac58b71e8d311f7e87aa8caf9ce4b8acecc6c98f11ca02. -/
section LongWagnerStandaloneBody30
/-!
# Exact finite fibre certificates for Long–Wagner
This module checks the finite integer coefficient identities in the paper.
The analytic premise is explicitly the family of displayed sparse linear
inequalities. No cube-counting or classification premise is hidden as an assumption.
The data are generated from the independently audited rational JSON files.
-/
set_option maxRecDepth 1000000
set_option maxHeartbeats 0
open scoped BigOperators
namespace LongWagnerFiniteFibreCertificates
-- BEGIN GENERATED FINITE CERTIFICATES
end LongWagnerFiniteFibreCertificates
end LongWagnerStandaloneBody30
/- Source: LongWagnerFiniteFibrePremises; SHA256 fcdff7d1ea3feea448a15e5622cf88282937c548b5792d267fbef70caf2cb8ce. -/
section LongWagnerStandaloneBody31
/-!
Semantic adapters for the eight exact finite fibre certificates.
The analytic input is a family of ordinary cardinality/correlation inequalities.
The coefficient table is checked by the ordinary kernel, independently of the
already verified nonnegative-weight certificate identities.
-/
set_option maxRecDepth 1000000
set_option maxHeartbeats 0
open scoped BigOperators
namespace LongWagnerFiniteFibrePremises
open LongWagnerFiniteFibreCertificates
-- BEGIN GENERATED SEMANTIC ROW MAPS
end LongWagnerFiniteFibrePremises
end LongWagnerStandaloneBody31
/- Source: LongWagnerLooseSourceFiniteCertificates; SHA256 ff03ead736efca8d0fa2a1cc47c9ad8d68f76c47843cf842391f5aac757ddb0c. -/
section LongWagnerStandaloneBody32
/-! Two exact additional finite cases for the multiplicity-two source route.
All actual analytic premises remain visible in SemanticPremises.
-/
set_option maxRecDepth 1000000
set_option maxHeartbeats 0
open scoped BigOperators
namespace LongWagnerLooseSourceFiniteCertificates
open LongWagnerFiniteFibreCertificates LongWagnerFiniteFibrePremises
end LongWagnerLooseSourceFiniteCertificates
end LongWagnerStandaloneBody32
/- Source: LongWagnerFibreInnerHighOdd; SHA256 db99ce169166a6d1acaeecb0d125c2e9f6f4486054265d75d389af4c089165d3. -/
section LongWagnerStandaloneBody33
/-!
# Actual inner high-odd bounds for dyadic quotient fibres
The subgroup generated by 2^p has order2^(k+1). Its selected cardinality is
exactly a0+a_(q/2), and its odd selected part is a_(q/2). This makes the
previously verified high-odd theorem applicable without an induction hypothesis.
-/
open Z2nFiveEighths LongWagnerTools LongWagnerHighOdd
open LongWagnerFibreBounds LongWagnerFibreAnalytic
set_option autoImplicit false
namespace LongWagnerFibreInnerHighOdd
end LongWagnerFibreInnerHighOdd
end LongWagnerStandaloneBody33
/- Source: LongWagnerActualFiniteFibreCases; SHA256 4aa18a7d4aede6e93214cf6ba483aa3373a586b1ecb346b1838906b30535d298. -/
section LongWagnerStandaloneBody34
/-!
Actual cyclic dyadic fibre masses satisfy the semantic premises of every finite
certificate. A normalized link container and its quotient increment are explicit
assumptions; no classification theorem is postulated here.
-/
set_option maxRecDepth 1000000
set_option maxHeartbeats 0
open scoped BigOperators
namespace LongWagnerActualFiniteFibreCases
open Z2nFiveEighths LongWagnerTools LongWagnerBridge
open LongWagnerFibreBounds LongWagnerFibreAnalytic LongWagnerFibreInnerHighOdd
open LongWagnerFiniteFibreCertificates LongWagnerFiniteFibrePremises
-- BEGIN ACTUAL FINITE CASES
open LongWagnerLooseSourceFiniteCertificates
end LongWagnerActualFiniteFibreCases
end LongWagnerStandaloneBody34
/- Source: LongWagnerLargeLinkContainer; SHA256 129e9282fc51d9704dd390bebb992d929e1c91e10dda1986a4740c67492653ea. -/
section LongWagnerStandaloneBody35
open scoped Pointwise
namespace LongWagnerLargeLinkContainer
open LongWagnerQuotientTransport LongWagnerFibreBounds LongWagnerTools
end LongWagnerLargeLinkContainer
end LongWagnerStandaloneBody35
/- Source: LongWagnerPacking; SHA256 cd14db4aae071fc84a9c39a583703fedcf6ae95c23899acb1605479757d8f8be. -/
section LongWagnerStandaloneBody36
open scoped BigOperators
set_option autoImplicit false
set_option maxRecDepth 100000
set_option maxHeartbeats 0
namespace LongWagnerPacking
end LongWagnerPacking
end LongWagnerStandaloneBody36
/- Source: LongWagnerWeightedPacking; SHA256 8d270bd935b5dfa6be857fa8c68ff9ee819d4dd0650e52244b6422708a32843a. -/
section LongWagnerStandaloneBody37
open scoped BigOperators
set_option autoImplicit false
set_option maxHeartbeats 0
namespace LongWagnerPacking
end LongWagnerPacking
end LongWagnerStandaloneBody37
/- Source: LongWagnerPackingUniform; SHA256 41e61971da16c3dd02ce5ccb5334c5f02c0462b13a13bc73ebb96fd8a23eea8d. -/
section LongWagnerStandaloneBody38
set_option autoImplicit false
set_option maxHeartbeats 0
namespace LongWagnerPacking
end LongWagnerPacking
end LongWagnerStandaloneBody38
/- Source: LongWagnerPackingBounds; SHA256 ee4b6dd4e0085d475739c5fb5acea4982fbb2dcadd39e14a6982cf21e506cdc0. -/
section LongWagnerStandaloneBody39
set_option autoImplicit false
set_option maxHeartbeats 0
namespace LongWagnerPacking
end LongWagnerPacking
end LongWagnerStandaloneBody39
/- Source: LongWagnerQuotientIntervals; SHA256 51849c86f22fb838151d0b73a7b5a4c1fc0d223ed39fdaf717a61f0c83fcc193. -/
section LongWagnerStandaloneBody40
open scoped BigOperators
set_option autoImplicit false
set_option maxHeartbeats 0
namespace LongWagnerQuotientIntervals
end LongWagnerQuotientIntervals
end LongWagnerStandaloneBody40
/- Source: LongWagnerZeroIntervals; SHA256 018a1cffe1b222ae4bac593443c1b4f76fd5c8aaed3530f02ce267ced4b8eb98. -/
section LongWagnerStandaloneBody41
/-! Exact zero-shift natural interval geometry, independent of the ambient set. -/
open scoped BigOperators
set_option autoImplicit false
set_option maxHeartbeats 0
namespace LongWagnerZeroIntervals
open LongWagnerQuotientIntervals
end LongWagnerZeroIntervals
end LongWagnerStandaloneBody41
/- Source: LongWagnerRelaxedSourceMass; SHA256 06a5628f3bea0702a511067a9ca46eb0d6448b735571edc24a3333088eb9c926. -/
section LongWagnerStandaloneBody42
open scoped BigOperators Pointwise
namespace LongWagnerRelaxedSourceMass
variable {G : Type*} [AddCommGroup G] [DecidableEq G]
end LongWagnerRelaxedSourceMass
end LongWagnerStandaloneBody42
/- Source: LongWagnerFibreSourceMass; SHA256 4c4bef63468708f40faed369ade0cf7bdcff68c0ab82ee64d4ccfe41eb986994. -/
section LongWagnerStandaloneBody43
open scoped BigOperators Pointwise
namespace LongWagnerFibreSourceMass
open Z2nFiveEighths LongWagnerTools LongWagnerHighOdd
open LongWagnerFibreBounds LongWagnerFibreAnalytic LongWagnerRelaxedSourceMass
end LongWagnerFibreSourceMass
end LongWagnerStandaloneBody43
/- Source: LongWagnerZeroLargeQuotients; SHA256 fa5b0c14f771582732e56fc16affc9492c0e8347c51e3ede2adf12b55f0ed2b0. -/
section LongWagnerStandaloneBody44
/-!
# Actual zero-image exclusion in quotients at least128
The middle interval container is explicit. Its existence and normalization are
separate from these unconditional cardinality consequences of genuine CubeFree.
-/
open scoped BigOperators
set_option autoImplicit false
set_option maxHeartbeats 0
namespace LongWagnerZeroLargeQuotients
open Z2nFiveEighths LongWagnerTools LongWagnerHighOdd
open LongWagnerFibreBounds LongWagnerFibreAnalytic LongWagnerFibreSourceMass
open LongWagnerActualFiniteFibreCases LongWagnerRelaxedSourceMass
open LongWagnerQuotientIntervals
end LongWagnerZeroLargeQuotients
end LongWagnerStandaloneBody44
/- Source: LongWagnerFibreCubeRectangles; SHA256 f9f25a542d32055d87c807f342b86cff06f731197d69278d4bfd323ea9e20b27. -/
section LongWagnerStandaloneBody45
/-!
# Actual full-cube rectangle bounds
These inequalities use three selected generators x,a,b and all seven cube
vertices. Repeated a=b is allowed. No quotient classification is assumed.
-/
open Z2nFiveEighths LongWagnerTools LongWagnerFibreBounds
open LongWagnerFibreAnalytic LongWagnerFibreInnerHighOdd
set_option autoImplicit false
namespace LongWagnerFibreCubeRectangles
end LongWagnerFibreCubeRectangles
end LongWagnerStandaloneBody45
/- Source: LongWagnerQ8Zero; SHA256 74bf87167465277ecb03661e3b0fe453dbe338c00d598a972a79455d3698649d. -/
section LongWagnerStandaloneBody46
/-!
# Actual quotient-eight zero-shift exclusion
The normalized quotient container {3,4,5} is explicit. All counting, full-cube,
inner-high-odd and final density steps are proved for actual finite sets.
No maximal sum-free classification or universal density theorem is assumed.
-/
open Z2nFiveEighths LongWagnerTools LongWagnerFibreBounds
open LongWagnerFibreAnalytic LongWagnerFibreInnerHighOdd LongWagnerFibreCubeRectangles
set_option autoImplicit false
namespace LongWagnerQ8Zero
end LongWagnerQ8Zero
end LongWagnerStandaloneBody46
/- Source: LongWagnerQ2Container; SHA256 341a4c3d632db185d38f4fa8e1014df9f69a5b2cb61591baf8bf23a8802241b2. -/
section LongWagnerStandaloneBody47
open Z2nFiveEighths LongWagnerTools LongWagnerFibreBounds LongWagnerFibreAnalytic
open LongWagnerFibreInnerHighOdd
namespace LongWagnerQ2Container
end LongWagnerQ2Container
end LongWagnerStandaloneBody47
/- Source: LongWagnerAllZeroImages; SHA256 6769075ccc3ed89f5c4b7cd44c700099d91009c145d63dbf5bc6aa771f7315c5. -/
section LongWagnerStandaloneBody48
/-! Complete actual zero-image dispatch with its normalized interval container explicit. -/
set_option autoImplicit false
namespace LongWagnerAllZeroImages
open Z2nFiveEighths LongWagnerTools LongWagnerFibreBounds LongWagnerFibreAnalytic
open LongWagnerActualFiniteFibreCases LongWagnerFiniteFibrePremises
open LongWagnerZeroLargeQuotients
end LongWagnerAllZeroImages
end LongWagnerStandaloneBody48
/- Source: LongWagnerQ8Nonzero; SHA256 6f89d147666474a005d010cc95c40b1c4d50bde21b7608e8b7a1d1aed62afa92. -/
section LongWagnerStandaloneBody49
/-! Direct actual-fibre exclusions for all four signed nonzero q8 increments. -/
set_option maxHeartbeats 0
open scoped BigOperators
namespace LongWagnerQ8Nonzero
open Z2nFiveEighths LongWagnerTools LongWagnerBridge
open LongWagnerFibreBounds LongWagnerFibreAnalytic LongWagnerActualFiniteFibreCases
end LongWagnerQ8Nonzero
end LongWagnerStandaloneBody49
/- Source: LongWagnerQ32DirectFiniteCertificate; SHA256 3e438b443cef08531a457e7a91334367f6e32eebb598aa192bb12970c82b7bb3. -/
section LongWagnerStandaloneBody50
/-! Two exact additional finite cases for the multiplicity-two source route.
All actual analytic premises remain visible in SemanticPremises.
-/
set_option maxRecDepth 1000000
set_option maxHeartbeats 0
open scoped BigOperators
namespace LongWagnerQ32DirectFiniteCertificate
open LongWagnerFiniteFibreCertificates LongWagnerFiniteFibrePremises
end LongWagnerQ32DirectFiniteCertificate
end LongWagnerStandaloneBody50
/- Source: LongWagnerSmallQuotientDispatch; SHA256 7d043ae2c76daa27810b2694b7f756e50710d0ec3c620db75a9260abd28d9ffa. -/
section LongWagnerStandaloneBody51
/-! Exact small-quotient dispatch for the relaxed source route.
The progression packing decomposition is an explicit analytic input until its
separate actual adapter is connected. Source charges are actual proved facts.
-/
set_option maxHeartbeats 0
set_option maxRecDepth 1000000
open scoped BigOperators
namespace LongWagnerSmallQuotientDispatch
open Z2nFiveEighths LongWagnerTools LongWagnerBridge
open LongWagnerFibreBounds LongWagnerFibreAnalytic LongWagnerFibreSourceMass
open LongWagnerRelaxedSourceMass LongWagnerPacking
open LongWagnerFiniteFibreCertificates LongWagnerFiniteFibrePremises
open LongWagnerActualFiniteFibreCases
end LongWagnerSmallQuotientDispatch
end LongWagnerStandaloneBody51
/- Source: LongWagnerSourcePacking; SHA256 efc3b97d9d3a698a054c2b6d37b36e1588d3dca92a91e8e3854b38b830f761d7. -/
section LongWagnerStandaloneBody52
open scoped BigOperators
set_option autoImplicit false
set_option maxHeartbeats 0
namespace LongWagnerQuotientIntervals
end LongWagnerQuotientIntervals
end LongWagnerStandaloneBody52
/- Source: LongWagnerQuotientIntervalZMod; SHA256 fa347496764b4db7ff19f37cea226ca5fc5442299e9447d1d298c6c0d54b201c. -/
section LongWagnerStandaloneBody53
set_option autoImplicit false
set_option maxHeartbeats 0
namespace LongWagnerQuotientIntervals
end LongWagnerQuotientIntervals
end LongWagnerStandaloneBody53
/- Source: LongWagnerQuotientIntervalAdapters; SHA256 04fe5778b22f6add2e44d637a846e362911b71dad4487f58ef8aabbf148934aa. -/
section LongWagnerStandaloneBody54
open scoped BigOperators
set_option autoImplicit false
set_option maxHeartbeats 0
namespace LongWagnerQuotientIntervals
end LongWagnerQuotientIntervals
end LongWagnerStandaloneBody54
/- Source: LongWagnerActualSourcePacking; SHA256 8a5b9339fff633106b9871046a1c1f7918fbb01023a2a0aca17783af99a94c33. -/
section LongWagnerStandaloneBody55
open scoped BigOperators
set_option autoImplicit false
set_option maxHeartbeats 0
namespace LongWagnerQuotientIntervals
open Z2nFiveEighths LongWagnerTools LongWagnerHighOdd
open LongWagnerFibreBounds LongWagnerFibreAnalytic
end LongWagnerQuotientIntervals
end LongWagnerStandaloneBody55
/- Source: LongWagnerShiftRestriction; SHA256 f0ec0305069129cfbfadf9b28b362ad0a75977b0f5704133ae6f9e6dec3de85a. -/
section LongWagnerStandaloneBody56
open scoped BigOperators Pointwise
namespace LongWagnerShiftRestriction
open LongWagnerRelaxedSourceMass
open Z2nFiveEighths LongWagnerTools LongWagnerFibreBounds LongWagnerFibreAnalytic LongWagnerFibreSourceMass
end LongWagnerShiftRestriction
end LongWagnerStandaloneBody56
/- Source: LongWagnerSmallQuotientActual; SHA256 2228403e7c6fcbb57ec9a61f86ef586982a88a906441cbc6bb41660ee04a7aa9. -/
section LongWagnerStandaloneBody57
/-! Complete actual small-quotient nonzero exclusion.
The interval packing and source geometry are proved, not supplied as premises.
Only the normalized actual progression container remains an explicit hypothesis.
-/
set_option maxHeartbeats 0
open scoped BigOperators
namespace LongWagnerSmallQuotientActual
open Z2nFiveEighths LongWagnerTools LongWagnerBridge
open LongWagnerFibreBounds LongWagnerFibreAnalytic
open LongWagnerActualFiniteFibreCases LongWagnerSmallQuotientDispatch
open LongWagnerQuotientIntervals LongWagnerRelaxedSourceMass
end LongWagnerSmallQuotientActual
end LongWagnerStandaloneBody57
/- Source: LongWagnerLargeNumericClosure; SHA256 2b854cbbf4fb52caa6d8805d84961f98bfcb8512db187d6099d2df6b2fa5b98d. -/
section LongWagnerStandaloneBody58
namespace LongWagnerLargeNumericClosure
end LongWagnerLargeNumericClosure
end LongWagnerStandaloneBody58
/- Source: LongWagnerLargeNonzeroQuotients; SHA256 a2e711c1f4cd53e14227625f2651fa9a8872395e79c7a6e6c0beeef17cb745f2. -/
section LongWagnerStandaloneBody59
open scoped BigOperators Pointwise
namespace LongWagnerLargeNonzeroQuotients
open Z2nFiveEighths LongWagnerTools
open LongWagnerFibreBounds LongWagnerFibreAnalytic LongWagnerFibreSourceMass
open LongWagnerRelaxedSourceMass LongWagnerQuotientIntervals
open LongWagnerActualFiniteFibreCases LongWagnerShiftRestriction
theorem large_nonzero_actual_exclusion (p k c v : ℕ)
(A : Finset (Ambient p k)) (z : Ambient p k) (hA : CubeFree A)
(hcritical : 3 * c = 2 ^ (p + 1) + 1)
(hqbig : 2048 ≤ 2 ^ (p + 1))
(hcontainer : link A z ⊆ fibreContainer p k (actualContainer p (Finset.Ico c (2 * c))))
(hshift : quotientHom p k z = (v : Quotient p))
(hvpos : 0 < v) (hvsmall : 3 * v ≤ c)
(hlink : 2 ^ ((p + k) + 1) < 3 * (link A z).card)
(hdensity : 5 * 2 ^ ((p + k) + 1) < 8 * A.card) : False := by sorry
end LongWagnerLargeNonzeroQuotients
end LongWagnerStandaloneBody59
/- Source: LongWagnerAllSelectedLinkCaps; SHA256 ee85548c58ef10a7df265a50fc308181ce87643486ff11e238bf1a8a121d22d0. -/
section LongWagnerStandaloneBody60
open Z2nFiveEighths LongWagnerTools LongWagnerFibreBounds LongWagnerFibreAnalytic
open LongWagnerActualFiniteFibreCases
namespace LongWagnerAllSelectedLinkCaps
end LongWagnerAllSelectedLinkCaps
namespace Z2nFiveEighths
end Z2nFiveEighths
end LongWagnerStandaloneBody60
/- Connector entry: exact original four-binder statement, without additional assumptions. -/
Source
Present Lean proof, LongWagnerLargeNonzeroQuotients.lean, declaration LongWagnerLargeNonzeroQuotients.large_nonzero_actual_exclusion. Background problem: Jason Long and Adam Zsolt Wagner, The largest projective cube-free subsets of Z_{2^n}, arXiv:1810.01225, Conjecture 5.1 (https://arxiv.org/html/1810.01225v1#S5). The auxiliary statement is derived in the present proof and is not asserted to be a theorem stated in that paper.