Long–Wagner proof infrastructure and exact finite certificate data

/-
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. -/
section LongWagnerStandaloneBody0
open scoped Pointwise

namespace LongWagnerHPPreparation

variable {G : Type*} [AddCommGroup G]

/-- A sum-free set, allowing repeated summands. -/
def SumFree (s : Set G) : Prop := Disjoint s (s + s)

















end LongWagnerHPPreparation
end LongWagnerStandaloneBody0

/- Source: LongWagnerLargeSumFreeElementary; SHA256 3c01d8d4efaf415ae3aadbb561e40363046f10d6ddfd960c47dced270a76fe6b. -/
section LongWagnerStandaloneBody1
open scoped Pointwise

namespace LongWagnerLargeSumFreeElementary

variable {G : Type*} [AddCommGroup G] [DecidableEq G]

/-- Sum-freeness with repeated summands allowed. -/
def SumFree (s : Finset G) : Prop :=
  ∀ a ∈ s, ∀ b ∈ s, a + b ∉ s





















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 : α}

@[to_additive]
instance (s : Finset α) : DecidablePred (· ∈ stabilizer α (s : Set α)) :=
  fun a ↦ decidable_of_iff (a ∈ stabilizer α s) (by simp)

/-- The stabilizer of `s` as a finset. As an exception, this sends `∅` to `∅`. -/
@[to_additive /-- The stabilizer of `s` as a finset. As an exception, this sends `∅` to `∅`. -/]
def mulStab (s : Finset α) : Finset α := {a ∈ s / s | a • s = s}

@[to_additive (attr := simp)]
lemma mem_mulStab (hs : s.Nonempty) : a ∈ s.mulStab ↔ a • s = s := by
  rw [mulStab, mem_filter, mem_div, and_iff_right_of_imp]
  obtain ⟨b, hb⟩ := hs
  exact fun h ↦ ⟨_, by rw [← h]; exact smul_mem_smul_finset hb, _, hb, mul_div_cancel_right _ _⟩













@[to_additive (attr := simp)]
lemma mulStab_empty : mulStab (∅ : Finset α) = ∅ := by simp [mulStab]



@[to_additive]
lemma Nonempty.of_mulStab : s.mulStab.Nonempty → s.Nonempty := by
  simp_rw [nonempty_iff_ne_empty, not_imp_not]; rintro rfl; exact mulStab_empty

@[to_additive (attr := simp)]
lemma one_mem_mulStab : (1 : α) ∈ s.mulStab ↔ s.Nonempty :=
  ⟨fun h ↦ Nonempty.of_mulStab ⟨_, h⟩, fun h ↦ (mem_mulStab h).2 <| one_smul _ _⟩

@[to_additive] protected alias ⟨_, Nonempty.one_mem_mulStab⟩ := one_mem_mulStab























end Group

variable [CommGroup α] [DecidableEq α] {s t : Finset α} {a : α}



































/-- A fintype instance for the stabilizer of a nonempty finset `s` in terms of `s.mulStab`. -/
@[to_additive (attr := implicit_reducible)
/-- A fintype instance for the stabilizer of a nonempty finset `s` in terms of `s.addStab`. -/]
 def fintypeStabilizerOfMulStab (hs : s.Nonempty) : Fintype (stabilizer α s) where
  elems := s.mulStab.attach.map
    ⟨Subtype.map id fun _ ↦ (mem_mulStab hs).1, Subtype.map_injective _ injective_id⟩
  complete a := mem_map.2
    ⟨⟨_, (mem_mulStab hs).2 a.2⟩, mem_attach _ ⟨_, (mem_mulStab hs).2 a.2⟩, Subtype.ext rfl⟩













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]









/-- The class of one generates every quotient of the actual cyclic dyadic ambient group. -/
theorem quotient_mem_zmultiples_one (n : ℕ) (H : AddSubgroup (ZMod (2 ^ n)))
    (x : ZMod (2 ^ n) ⧸ H) :
    x ∈ AddSubgroup.zmultiples (((1 : ZMod (2 ^ n)) : ZMod (2 ^ n) ⧸ H)) := by
  obtain ⟨a, rfl⟩ := QuotientAddGroup.mk_surjective x
  apply AddSubgroup.mem_zmultiples_iff.mpr
  refine ⟨(a.val : ℤ), ?_⟩
  change (a.val : ℤ) • (QuotientAddGroup.mk' H) 1 = (QuotientAddGroup.mk' H) a
  rw [← map_zsmul]
  congr 1
  simp [zsmul_eq_mul, ZMod.natCast_zmod_val]

/-- Coordinates from the actual cyclic quotient that send the class of one to one. -/
noncomputable def canonicalQuotientZModEquiv (n : ℕ)
    (H : AddSubgroup (ZMod (2 ^ n))) :
    (ZMod (2 ^ n) ⧸ H) ≃+ ZMod (Nat.card (ZMod (2 ^ n) ⧸ H)) :=
  (zmodAddEquivOfGenerator (quotient_mem_zmultiples_one n H) rfl).symm





end LongWagnerCriticalQuotient
end LongWagnerStandaloneBody7

/- Source: LongWagnerQuotientTransport; SHA256 71a85b9f0cfe19077123cb2a580c59c81715334eae7d05058e891ba7a4ae22a7. -/
section LongWagnerStandaloneBody8
open scoped Pointwise

namespace LongWagnerQuotientTransport

variable {G K : Type*} [AddCommGroup G] [AddCommGroup K]











/-- Canonical coordinates specialized to an identified two-power quotient order. -/
noncomputable def canonicalDyadicQuotientZModEquiv (n : ℕ)
    (H : AddSubgroup (ZMod (2 ^ n))) (m : ℕ)
    (hm : Nat.card (ZMod (2 ^ n) ⧸ H) = 2 ^ m) :
    (ZMod (2 ^ n) ⧸ H) ≃+ ZMod (2 ^ m) :=
  (LongWagnerCriticalQuotient.canonicalQuotientZModEquiv n H).trans
    (ZMod.ringEquivCongr hm).toAddEquiv





/-- The actual quotient image represented as a Finset in canonical dyadic coordinates. -/
noncomputable def canonicalModel (n : ℕ) (s : Set (ZMod (2 ^ n))) (m : ℕ)
    (hm : Nat.card (ZMod (2 ^ n) ⧸ AddAction.stabilizer (ZMod (2 ^ n)) (s + s)) =
      2 ^ m) : Finset (ZMod (2 ^ m)) :=
  ((canonicalDyadicQuotientZModEquiv n (AddAction.stabilizer (ZMod (2 ^ n)) (s + s))
    m hm) '' (((↑) : ZMod (2 ^ n) →
      ZMod (2 ^ n) ⧸ AddAction.stabilizer (ZMod (2 ^ n)) (s + s)) '' s)).toFinite.toFinset











end LongWagnerQuotientTransport
end LongWagnerStandaloneBody8

/- Source: LongWagnerAtomCounting; SHA256 fc2cd7b1d1d98ac368c681e046974c25f53609fb64ffd92e8fdecc8a2f6ac699. -/
section LongWagnerStandaloneBody9
open scoped Pointwise

namespace LongWagnerAtomCounting

variable {G : Type*} [AddCommGroup G] [DecidableEq G] [Fintype G]

def exterior (B X : Finset G) : Finset G := Finset.univ \ (X + B)

def BoundaryLowerBound (B : Finset G) (κ : ℕ) : Prop :=
  ∀ X : Finset G, 2 ≤ X.card → 2 ≤ (exterior B X).card →
    X.card + κ ≤ (X + B).card

structure Fragment (B : Finset G) (κ : ℕ) (X : Finset G) : Prop where
  card_ge_two : 2 ≤ X.card
  exterior_card_ge_two : 2 ≤ (exterior B X).card
  add_card_eq : (X + B).card = X.card + κ

structure Atom (B : Finset G) (κ : ℕ) (X : Finset G) : Prop
    extends Fragment B κ X where
  minimal : ∀ Y : Finset G, Fragment B κ Y → X.card ≤ Y.card











































end LongWagnerAtomCounting
end LongWagnerStandaloneBody9

/- Source: LongWagnerSingleRun; SHA256 748637a96fdea0a18d4e6176d8db847adb84217e835e4a447f552573b556345e. -/
section LongWagnerStandaloneBody10
open scoped Pointwise

namespace LongWagnerSingleRun

variable {G : Type*} [AddCommGroup G] [DecidableEq G]

/-- The first `n` nonnegative multiples of a proposed progression step. -/
def progression (d : G) (n : ℕ) : Finset G :=
  (Finset.range n).image (fun j => j • d)

















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]

noncomputable def coordinates (M : Finset G) (d b : G) : Finset ℕ :=
  (Finset.range (addOrderOf d)).filter (fun j => b + j • d ∈ M)













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]

def translate (t : G) (X : Finset G) : Finset G := X.image (fun x => x + t)



























































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]

/-- Proper nontrivial subgroup expansions have boundary at least the subgroup size. -/
def NoSmallSubgroupExpansion (S : Finset G) : Prop :=
  ∀ H : AddSubgroup G, H ≠ ⊥ → H ≠ ⊤ →
    S.card + Nat.card H ≤ ((S : Set G) + (H : Set G)).ncard

















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]

/-- The link at `z`: elements of `A` whose translate by `z` also lies in `A`. -/
def link (A : Finset G) (z : G) : Finset G :=
  A.filter (fun x => x + z ∈ A)



/-- The ordinary sum-free condition, including repeated summands. -/
def SumFree (S : Finset G) : Prop :=
  ∀ x ∈ S, ∀ y ∈ S, x + y ∉ S





end Links

section HomPreimage

variable {G H : Type*} [AddCommGroup G] [AddCommGroup H]
variable [Fintype G] [DecidableEq H]

def homPreimage (f : G →+ H) (A : Finset H) : Finset G :=
  Finset.univ.filter (fun x => f x ∈ A)





end HomPreimage

 def doubleIntHom (n : ℕ) : ℤ →+ ZMod (2 ^ (n + 1)) where
  toFun x := 2 * (x : ZMod (2 ^ (n + 1)))
  map_zero' := by simp
  map_add' x y := by simp [mul_add]

/-- The additive embedding of `ZMod (2^n)` onto the even subgroup upstairs. -/
def evenEmbed (n : ℕ) : ZMod (2 ^ n) →+ ZMod (2 ^ (n + 1)) :=
  ZMod.lift (2 ^ n) ⟨doubleIntHom n, by
    dsimp [doubleIntHom]
    push_cast
    rw [← pow_succ']
    simpa only [Nat.cast_pow, Nat.cast_ofNat] using ZMod.natCast_self (2 ^ (n + 1))⟩









/-- Halving the even elements of `A`, expressed as an exact finite preimage. -/
def evenHalf (n : ℕ) (A : Finset (ZMod (2 ^ (n + 1)))) : Finset (ZMod (2 ^ n)) :=
  homPreimage (evenEmbed n) A









/-- The complementary odd part upstairs; its cardinality is the odd-slice size. -/
def oddPart (n : ℕ) (A : Finset (ZMod (2 ^ (n + 1)))) :
    Finset (ZMod (2 ^ (n + 1))) :=
  A.filter (fun t => ¬ Even t.val)



/-- The full old root's cardinality inequality, without assuming its truth. -/
def FiveEighthsBound (n : ℕ) (A : Finset (ZMod (2 ^ n))) : Prop :=
  8 * A.card ≤ 5 * 2 ^ n

/-- The intended universal theorem interface; this definition adds no assumption. -/
def LongWagnerRoot : Prop :=
  ∀ n : ℕ, 4 ≤ n → ∀ A : Finset (ZMod (2 ^ n)), CubeFree A → FiveEighthsBound n A



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]

def equivImage (e : G ≃+ H) (A : Finset G) : Finset H := A.image e







end AdditiveEquivalence

section UnitScaling
variable {R : Type*} [CommRing R] [DecidableEq R]

/-- Multiplication by a unit is an additive equivalence, with explicit inverse. -/
def unitScale (u : Rˣ) : R ≃+ R where
  toFun x := (u : R) * x
  invFun x := ((u⁻¹ : Rˣ) : R) * x
  left_inv x := by simp [← mul_assoc]
  right_inv x := by simp [← mul_assoc]
  map_add' x y := by simp [mul_add]











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

/-- Odd residues, parametrized without choosing integer representatives. -/
def oddEmbed (n : ℕ) (x : ZMod (2 ^ n)) : ZMod (2 ^ (n + 1)) :=
  evenEmbed n x + 1



def oddUniverse (n : ℕ) : Finset (ZMod (2 ^ (n + 1))) :=
  Finset.univ.image (oddEmbed n)





/-- The embedding onto the subgroup of residues divisible by four. -/
def fourEmbed (n : ℕ) : ZMod (2 ^ n) →+ ZMod (2 ^ (n + 2)) :=
  (evenEmbed (n + 1)).comp (evenEmbed n)

def fourPart (n : ℕ) (A : Finset (ZMod (2 ^ (n + 2)))) : Finset (ZMod (2 ^ n)) :=
  homPreimage (fourEmbed n) A














/-- Exact reduction from the ambient group to its halved modulus. -/
def reduceHom (n : ℕ) : ZMod (2 ^ (n + 1)) →+ ZMod (2 ^ n) :=
  (ZMod.castHom (by rw [pow_succ]; exact dvd_mul_right _ _) (ZMod (2 ^ n))).toAddMonoidHom





































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

abbrev Ambient (p k : ℕ) := ZMod (2 ^ ((p + k) + 1))
abbrev Quotient (p : ℕ) := ZMod (2 ^ (p + 1))

def quotientHom (p k : ℕ) : Ambient p k →+ Quotient p :=
  (ZMod.castHom (Nat.pow_dvd_pow 2 (by omega : p + 1 ≤ (p + k) + 1))
    (Quotient p)).toAddMonoidHom



def fibre (p k : ℕ) (i : Quotient p) : Finset (Ambient p k) :=
  Finset.univ.filter (fun x => quotientHom p k x = i)





def selectedFibre (p k : ℕ) (A : Finset (Ambient p k)) (i : Quotient p) :
    Finset (Ambient p k) := (fibre p k i).filter (fun x => x ∈ A)



def fibreMass (p k : ℕ) (A : Finset (Ambient p k)) (i : Quotient p) : ℕ :=
  (selectedFibre p k A i).card









/-- The half-modulus element in the quotient. -/
def half (p : ℕ) : Quotient p := (2 ^ p : ℕ)































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]

def starts (I : Finset G) (u : G) : Finset G :=
  I.filter (fun x => x + u ∈ I)

theorem twice_card_starts_lt_of_small_difference (I : Finset G)
    (hsmall : 2 * (I - I).card < 3 * I.card) {u : G} (hu : u ∈ I - I) :
    I.card < 2 * (starts I u).card := by
  rcases Finset.mem_sub.mp hu with ⟨a, ha, b, hb, rfl⟩
  let T₁ := I.image (fun x => x - a)
  let T₂ := I.image (fun x => x - b)
  have hT₁ : T₁ ⊆ I - I := by
    intro z hz
    rcases Finset.mem_image.mp hz with ⟨x, hx, rfl⟩
    exact Finset.mem_sub.mpr ⟨x, hx, a, ha, rfl⟩
  have hT₂ : T₂ ⊆ I - I := by
    intro z hz
    rcases Finset.mem_image.mp hz with ⟨x, hx, rfl⟩
    exact Finset.mem_sub.mpr ⟨x, hx, b, hb, rfl⟩
  have hcard₁ : T₁.card = I.card := by
    apply Finset.card_image_of_injective
    intro x y h
    have hh := congrArg (fun t => t + a) h
    simpa using hh
  have hcard₂ : T₂.card = I.card := by
    apply Finset.card_image_of_injective
    intro x y h
    have hh := congrArg (fun t => t + b) h
    simpa using hh
  have huCard : (T₁ ∪ T₂).card ≤ (I - I).card :=
    Finset.card_le_card (Finset.union_subset hT₁ hT₂)
  have hsum := Finset.card_inter_add_card_union T₁ T₂
  have hiCard : (T₁ ∩ T₂).card ≤ (starts I (a - b)).card := by
    apply Finset.card_le_card_of_injOn (fun z => z + b)
    · intro z hz
      rcases Finset.mem_inter.mp hz with ⟨hz₁, hz₂⟩
      rcases Finset.mem_image.mp hz₁ with ⟨x, hx, hxz⟩
      rcases Finset.mem_image.mp hz₂ with ⟨y, hy, hyz⟩
      apply Finset.mem_filter.mpr
      constructor
      · have he : z + b = y := by rw [← hyz]; abel
        change z + b ∈ I
        rw [he]
        exact hy
      · have he : z + b + (a - b) = x := by rw [← hxz]; abel
        change z + b + (a - b) ∈ I
        rw [he]
        exact hx
    · intro z _ w _ hzw
      exact add_right_cancel hzw
  omega

theorem add_mem_difference_of_small (I : Finset G)
    (hsmall : 2 * (I - I).card < 3 * I.card) {u v : G}
    (hu : u ∈ I - I) (hv : v ∈ I - I) : u + v ∈ I - I := by
  have hnv : -v ∈ I - I := by
    rcases Finset.mem_sub.mp hv with ⟨a, ha, b, hb, rfl⟩
    apply Finset.mem_sub.mpr
    exact ⟨b, hb, a, ha, by abel⟩
  have huCard := twice_card_starts_lt_of_small_difference I hsmall hu
  have hvCard := twice_card_starts_lt_of_small_difference I hsmall hnv
  have hUnion : starts I u ∪ starts I (-v) ⊆ I := by
    apply Finset.union_subset
    · exact Finset.filter_subset _ _
    · exact Finset.filter_subset _ _
  have hUnionCard := Finset.card_le_card hUnion
  have hsum := Finset.card_inter_add_card_union (starts I u) (starts I (-v))
  have hpos : 0 < (starts I u ∩ starts I (-v)).card := by omega
  obtain ⟨x, hx⟩ := Finset.card_pos.mp hpos
  rcases Finset.mem_inter.mp hx with ⟨huX, hvX⟩
  have hxu : x + u ∈ I := (Finset.mem_filter.mp huX).2
  have hxv : x + -v ∈ I := (Finset.mem_filter.mp hvX).2
  apply Finset.mem_sub.mpr
  exact ⟨x + u, hxu, x + -v, hxv, by abel⟩

/-- A difference set smaller than three halves of its source is a subgroup. -/
def differenceSubgroup (I : Finset G)
    (hsmall : 2 * (I - I).card < 3 * I.card) : AddSubgroup G where
  carrier := {u | u ∈ I - I}
  zero_mem' := by
    have hp : 0 < I.card := by omega
    obtain ⟨a, ha⟩ := Finset.card_pos.mp hp
    exact Finset.mem_sub.mpr ⟨a, ha, a, ha, sub_self a⟩
  add_mem' := fun hu hv => add_mem_difference_of_small I hsmall hu hv
  neg_mem' := by
    intro u hu
    rcases Finset.mem_sub.mp hu with ⟨a, ha, b, hb, rfl⟩
    exact Finset.mem_sub.mpr ⟨b, hb, a, ha, by abel⟩



noncomputable instance differenceSubgroupFintype [Fintype G] (I : Finset G)
    (hsmall : 2 * (I - I).card < 3 * I.card) :
    Fintype (differenceSubgroup I hsmall) := Fintype.ofFinite _





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]

def symmetricSet (A : Finset G) : Finset G := A ∪ -A

@[simp] theorem mem_symmetricSet (A : Finset G) (x : G) :
    x ∈ symmetricSet A ↔ x ∈ A ∨ -x ∈ A := by
  simp [symmetricSet]

/-- The undirected Cayley graph generated by a finite set and its negatives. -/
def cayley (A : Finset G) : SimpleGraph G where
  Adj x y := x ≠ y ∧ y - x ∈ symmetricSet A
  symm := ⟨by
    intro x y h
    refine ⟨h.1.symm, ?_⟩
    simpa [mem_symmetricSet, neg_sub, or_comm] using h.2⟩
  loopless := ⟨by intro x h; exact h.1 rfl⟩

instance (A : Finset G) : DecidableRel (cayley A).Adj :=
  fun x y => inferInstanceAs (Decidable (x ≠ y ∧ y - x ∈ symmetricSet A))









/-- Translation by a fixed group element, represented as a finite image. -/
def translate (A : Finset G) (t : G) : Finset G := A.image (fun x => x + t)



















/-- The full all-selected-link proposition remains an explicit unproved input.
Unlike the earlier weaker induction interface, it includes residues in 8G. -/
def AllSelectedLinkCaps : Prop :=
  ∀ (n : ℕ), 4 ≤ n → ∀ (A : Finset (ZMod (2 ^ n))),
    Z2nFiveEighths.CubeFree A → 5 * 2 ^ n < 8 * A.card →
    ∀ z ∈ A, 3 * (link A z).card ≤ 2 ^ n



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

/-- The inverse image of a specified quotient container. -/
def fibreContainer (p k : ℕ) (C : Finset (Quotient p)) : Finset (Ambient p k) :=
  Finset.univ.filter (fun x => quotientHom p k x ∈ C)



/-- Actual selected link cardinality in an individual quotient fibre. -/
def linkMass (p k : ℕ) (A : Finset (Ambient p k)) (z : Ambient p k)
    (i : Quotient p) : ℕ := fibreMass p k (link A z) i









































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]













def reflection (G : Type*) [AddCommGroup G] : G ≃+ G where
  toFun := Neg.neg
  invFun := Neg.neg
  left_inv := neg_neg
  right_inv := neg_neg
  map_add' := neg_add





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

structure FibreRow where
  label : String
  terms : List (Nat × Int)
  rhs : Int
  weight : Nat
  deriving DecidableEq

def FibreRow.coeff (row : FibreRow) (j : Nat) : Int :=
  ((row.terms.find? fun t => t.1 == j).map Prod.snd).getD 0

def selectedMass (q : Nat) (x : Fin (2 * q) → ℝ) : ℝ :=
  ∑ j, if j.val < q then x j else 0

def FibrePremises (q : Nat) (rows : Array FibreRow)
    (x : Fin (2 * q) → ℝ) (h : ℝ) : Prop :=
  ∀ i : Fin rows.size,
    ∑ j : Fin (2 * q), (rows[i].coeff j.val : ℝ) * x j ≤ (rows[i].rhs : ℝ) * h







-- BEGIN GENERATED FINITE CERTIFICATES











/-- Exact certificate for q32_v2: normalized bound 223/12; all analytic rows follow. -/
def q32_v2Rows : Array FibreRow := #[
  { label := "['outside_link', 1]", terms := [(1, 1), (3, 1)], rhs := 1, weight := 12 },
  { label := "['outside_link', 9]", terms := [(9, 1), (11, 1)], rhs := 1, weight := 12 },
  { label := "['outside_link', 10]", terms := [(10, 1), (12, 1)], rhs := 1, weight := 12 },
  { label := "['link_source', 11, 11]", terms := [(11, -1), (43, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 12, 12]", terms := [(12, -1), (44, 1)], rhs := 0, weight := 30 },
  { label := "['link_source', 12, 14]", terms := [(14, -1), (44, 1)], rhs := 0, weight := 9 },
  { label := "['link_source', 13, 15]", terms := [(15, -1), (45, 1)], rhs := 0, weight := 39 },
  { label := "['link_source', 14, 14]", terms := [(14, -1), (46, 1)], rhs := 0, weight := 15 },
  { label := "['link_source', 16, 18]", terms := [(18, -1), (48, 1)], rhs := 0, weight := 3 },
  { label := "['link_source', 17, 17]", terms := [(17, -1), (49, 1)], rhs := 0, weight := 39 },
  { label := "['link_source', 18, 20]", terms := [(20, -1), (50, 1)], rhs := 0, weight := 18 },
  { label := "['single_diagonal', 18]", terms := [(4, 2), (18, 1), (22, 1)], rhs := 3, weight := 3 },
  { label := "['link_source', 20, 22]", terms := [(22, -1), (52, 1)], rhs := 0, weight := 39 },
  { label := "['link_source', 21, 23]", terms := [(23, -1), (53, 1)], rhs := 0, weight := 12 },
  { label := "['outside_link', 22]", terms := [(22, 1), (24, 1)], rhs := 1, weight := 12 },
  { label := "['outside_link', 23]", terms := [(23, 1), (25, 1)], rhs := 1, weight := 12 },
  { label := "['single_diagonal', 26]", terms := [(14, 1), (20, 2), (26, 1)], rhs := 3, weight := 12 },
  { label := "['outside_link', 28]", terms := [(28, 1), (30, 1)], rhs := 1, weight := 6 },
  { label := "['outside_link', 29]", terms := [(29, 1), (31, 1)], rhs := 1, weight := 9 },
  { label := "['paired_diagonal', 0]", terms := [(0, 4), (16, 2)], rhs := 4, weight := 3 },
  { label := "['paired_diagonal', 4]", terms := [(4, 1), (8, 2), (12, 1), (20, 1), (28, 1)], rhs := 4, weight := 6 },
  { label := "['paired_diagonal', 6]", terms := [(2, 1), (6, 1), (12, 2), (18, 1), (22, 1)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 7]", terms := [(5, 1), (7, 1), (14, 2), (21, 1), (23, 1)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 11]", terms := [(1, 1), (11, 1), (17, 1), (22, 2), (27, 1)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 15]", terms := [(13, 1), (15, 1), (29, 1), (30, 2), (31, 1)], rhs := 4, weight := 3 },
  { label := "['large_link']", terms := [(32, -3), (33, -3), (34, -3), (35, -3), (36, -3), (37, -3), (38, -3), (39, -3), (40, -3), (41, -3), (42, -3), (43, -3), (44, -3), (45, -3), (46, -3), (47, -3), (48, -3), (49, -3), (50, -3), (51, -3), (52, -3), (53, -3), (54, -3), (55, -3), (56, -3), (57, -3), (58, -3), (59, -3), (60, -3), (61, -3), (62, -3), (63, -3)], rhs := -32, weight := 13 },
  { label := "upper_bound(13)", terms := [(13, 1)], rhs := 1, weight := 9 },
  { label := "upper_bound(15)", terms := [(15, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(16)", terms := [(16, 1)], rhs := 1, weight := 6 },
  { label := "upper_bound(17)", terms := [(17, 1)], rhs := 1, weight := 39 },
  { label := "upper_bound(19)", terms := [(19, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(32)", terms := [(32, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(33)", terms := [(33, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(34)", terms := [(34, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(35)", terms := [(35, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(36)", terms := [(36, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(37)", terms := [(37, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(38)", terms := [(38, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(39)", terms := [(39, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(40)", terms := [(40, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(41)", terms := [(41, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(42)", terms := [(42, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(43)", terms := [(43, 1)], rhs := 1, weight := 27 },
  { label := "upper_bound(46)", terms := [(46, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(47)", terms := [(47, 1)], rhs := 1, weight := 39 },
  { label := "upper_bound(48)", terms := [(48, 1)], rhs := 1, weight := 36 },
  { label := "upper_bound(50)", terms := [(50, 1)], rhs := 1, weight := 21 },
  { label := "upper_bound(51)", terms := [(51, 1)], rhs := 1, weight := 39 },
  { label := "upper_bound(53)", terms := [(53, 1)], rhs := 1, weight := 27 },
  { label := "upper_bound(54)", terms := [(54, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(55)", terms := [(55, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(56)", terms := [(56, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(57)", terms := [(57, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(58)", terms := [(58, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(59)", terms := [(59, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(60)", terms := [(60, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(61)", terms := [(61, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(62)", terms := [(62, 1)], rhs := 0, weight := 39 },
  { label := "upper_bound(63)", terms := [(63, 1)], rhs := 0, weight := 39 },
  { label := "lower_bound(1)", terms := [(1, -1)], rhs := 0, weight := 12 }
]









/-- Exact certificate for q128_v2: normalized bound 155/2; all analytic rows follow. -/
def q128_v2Rows : Array FibreRow := #[
  { label := "['outside_link', 7]", terms := [(7, 1), (9, 1)], rhs := 1, weight := 500000 },
  { label := "['outside_link', 10]", terms := [(10, 1), (12, 1)], rhs := 1, weight := 500000 },
  { label := "['outside_link', 11]", terms := [(11, 1), (13, 1)], rhs := 1, weight := 1000000 },
  { label := "['outside_link', 15]", terms := [(15, 1), (17, 1)], rhs := 1, weight := 500000 },
  { label := "['outside_link', 16]", terms := [(16, 1), (18, 1)], rhs := 1, weight := 1000000 },
  { label := "['outside_link', 19]", terms := [(19, 1), (21, 1)], rhs := 1, weight := 1000000 },
  { label := "['single_diagonal', 24]", terms := [(24, 1), (48, 2), (72, 1)], rhs := 3, weight := 1833333 },
  { label := "['single_diagonal', 25]", terms := [(25, 1), (50, 2), (75, 1)], rhs := 3, weight := 1000000 },
  { label := "['single_diagonal', 26]", terms := [(26, 1), (52, 2), (78, 1)], rhs := 3, weight := 1000000 },
  { label := "['single_diagonal', 27]", terms := [(27, 1), (54, 2), (81, 1)], rhs := 3, weight := 500000 },
  { label := "['single_diagonal', 28]", terms := [(28, 1), (56, 2), (84, 1)], rhs := 3, weight := 1000000 },
  { label := "['single_diagonal', 29]", terms := [(29, 1), (58, 2), (87, 1)], rhs := 3, weight := 500000 },
  { label := "['outside_link', 31]", terms := [(31, 1), (33, 1)], rhs := 1, weight := 500000 },
  { label := "['outside_link', 32]", terms := [(32, 1), (34, 1)], rhs := 1, weight := 1000000 },
  { label := "['outside_link', 33]", terms := [(33, 1), (35, 1)], rhs := 1, weight := 500000 },
  { label := "['outside_link', 37]", terms := [(37, 1), (39, 1)], rhs := 1, weight := 250000 },
  { label := "['outside_link', 41]", terms := [(41, 1), (43, 1)], rhs := 1, weight := 250000 },
  { label := "['outside_link', 42]", terms := [(42, 1), (44, 1)], rhs := 1, weight := 1000000 },
  { label := "['link_source', 43, 43]", terms := [(43, -1), (171, 1)], rhs := 0, weight := 250000 },
  { label := "['link_source', 44, 44]", terms := [(44, -1), (172, 1)], rhs := 0, weight := 3000000 },
  { label := "['link_source', 46, 46]", terms := [(46, -1), (174, 1)], rhs := 0, weight := 1000000 },
  { label := "['link_source', 46, 48]", terms := [(48, -1), (174, 1)], rhs := 0, weight := 2000000 },
  { label := "['link_source', 48, 48]", terms := [(48, -1), (176, 1)], rhs := 0, weight := 666667 },
  { label := "['link_source', 48, 50]", terms := [(50, -1), (176, 1)], rhs := 0, weight := 2333333 },
  { label := "['link_source', 50, 52]", terms := [(52, -1), (178, 1)], rhs := 0, weight := 1500000 },
  { label := "['link_source', 52, 54]", terms := [(54, -1), (180, 1)], rhs := 0, weight := 1000000 },
  { label := "['link_source', 54, 56]", terms := [(56, -1), (182, 1)], rhs := 0, weight := 3000000 },
  { label := "['link_source', 56, 58]", terms := [(58, -1), (184, 1)], rhs := 0, weight := 3000000 },
  { label := "['link_source', 60, 62]", terms := [(62, -1), (188, 1)], rhs := 0, weight := 1000000 },
  { label := "['link_source', 64, 66]", terms := [(66, -1), (192, 1)], rhs := 0, weight := 250000 },
  { label := "['single_diagonal', 66]", terms := [(4, 2), (66, 1), (70, 1)], rhs := 3, weight := 250000 },
  { label := "['link_source', 67, 69]", terms := [(69, -1), (195, 1)], rhs := 0, weight := 250000 },
  { label := "['link_source', 68, 70]", terms := [(70, -1), (196, 1)], rhs := 0, weight := 250000 },
  { label := "['single_diagonal', 69]", terms := [(10, 2), (69, 1), (79, 1)], rhs := 3, weight := 250000 },
  { label := "['single_diagonal', 71]", terms := [(14, 2), (71, 1), (85, 1)], rhs := 3, weight := 500000 },
  { label := "['link_source', 72, 72]", terms := [(72, -1), (200, 1)], rhs := 0, weight := 2833333 },
  { label := "['link_source', 72, 74]", terms := [(74, -1), (200, 1)], rhs := 0, weight := 166667 },
  { label := "['link_source', 74, 74]", terms := [(74, -1), (202, 1)], rhs := 0, weight := 833333 },
  { label := "['link_source', 74, 76]", terms := [(76, -1), (202, 1)], rhs := 0, weight := 2166667 },
  { label := "['link_source', 76, 78]", terms := [(78, -1), (204, 1)], rhs := 0, weight := 3000000 },
  { label := "['link_source', 78, 78]", terms := [(78, -1), (206, 1)], rhs := 0, weight := 2000000 },
  { label := "['link_source', 78, 80]", terms := [(80, -1), (206, 1)], rhs := 0, weight := 1000000 },
  { label := "['link_source', 82, 84]", terms := [(84, -1), (210, 1)], rhs := 0, weight := 3000000 },
  { label := "['link_source', 84, 86]", terms := [(86, -1), (212, 1)], rhs := 0, weight := 3000000 },
  { label := "['link_source', 85, 87]", terms := [(87, -1), (213, 1)], rhs := 0, weight := 3000000 },
  { label := "['outside_link', 86]", terms := [(86, 1), (88, 1)], rhs := 1, weight := 1000000 },
  { label := "['outside_link', 87]", terms := [(87, 1), (89, 1)], rhs := 1, weight := 1000000 },
  { label := "['outside_link', 91]", terms := [(91, 1), (93, 1)], rhs := 1, weight := 500000 },
  { label := "['outside_link', 92]", terms := [(92, 1), (94, 1)], rhs := 1, weight := 500000 },
  { label := "['outside_link', 95]", terms := [(95, 1), (97, 1)], rhs := 1, weight := 500000 },
  { label := "['outside_link', 96]", terms := [(96, 1), (98, 1)], rhs := 1, weight := 1000000 },
  { label := "['outside_link', 97]", terms := [(97, 1), (99, 1)], rhs := 1, weight := 500000 },
  { label := "['single_diagonal', 101]", terms := [(47, 1), (74, 2), (101, 1)], rhs := 3, weight := 250000 },
  { label := "['single_diagonal', 102]", terms := [(50, 1), (76, 2), (102, 1)], rhs := 3, weight := 333333 },
  { label := "['single_diagonal', 103]", terms := [(53, 1), (78, 2), (103, 1)], rhs := 3, weight := 250000 },
  { label := "['single_diagonal', 104]", terms := [(56, 1), (80, 2), (104, 1)], rhs := 3, weight := 1000000 },
  { label := "['single_diagonal', 105]", terms := [(59, 1), (82, 2), (105, 1)], rhs := 3, weight := 250000 },
  { label := "['single_diagonal', 106]", terms := [(62, 1), (84, 2), (106, 1)], rhs := 3, weight := 1000000 },
  { label := "['outside_link', 110]", terms := [(110, 1), (112, 1)], rhs := 1, weight := 1000000 },
  { label := "['single_diagonal', 111]", terms := [(77, 1), (94, 2), (111, 1)], rhs := 3, weight := 250000 },
  { label := "['outside_link', 113]", terms := [(113, 1), (115, 1)], rhs := 1, weight := 750000 },
  { label := "['outside_link', 115]", terms := [(115, 1), (117, 1)], rhs := 1, weight := 250000 },
  { label := "['outside_link', 116]", terms := [(116, 1), (118, 1)], rhs := 1, weight := 500000 },
  { label := "['outside_link', 119]", terms := [(119, 1), (121, 1)], rhs := 1, weight := 500000 },
  { label := "['outside_link', 121]", terms := [(121, 1), (123, 1)], rhs := 1, weight := 500000 },
  { label := "['paired_diagonal', 0]", terms := [(0, 4), (64, 2)], rhs := 4, weight := 250000 },
  { label := "['paired_diagonal', 3]", terms := [(3, 1), (6, 2), (9, 1), (67, 1), (73, 1)], rhs := 4, weight := 500000 },
  { label := "['paired_diagonal', 4]", terms := [(4, 1), (8, 2), (12, 1), (68, 1), (76, 1)], rhs := 4, weight := 500000 },
  { label := "['paired_diagonal', 15]", terms := [(15, 1), (30, 2), (45, 1), (79, 1), (109, 1)], rhs := 4, weight := 500000 },
  { label := "['paired_diagonal', 20]", terms := [(20, 1), (40, 2), (60, 1), (84, 1), (124, 1)], rhs := 4, weight := 500000 },
  { label := "['paired_diagonal', 22]", terms := [(2, 1), (22, 1), (44, 2), (66, 1), (86, 1)], rhs := 4, weight := 1000000 },
  { label := "['paired_diagonal', 23]", terms := [(5, 1), (23, 1), (46, 2), (69, 1), (87, 1)], rhs := 4, weight := 1000000 },
  { label := "['paired_diagonal', 27]", terms := [(17, 1), (27, 1), (54, 2), (81, 1), (91, 1)], rhs := 4, weight := 500000 },
  { label := "['paired_diagonal', 28]", terms := [(20, 1), (28, 1), (56, 2), (84, 1), (92, 1)], rhs := 4, weight := 500000 },
  { label := "['paired_diagonal', 31]", terms := [(29, 1), (31, 1), (62, 2), (93, 1), (95, 1)], rhs := 4, weight := 500000 },
  { label := "['paired_diagonal', 35]", terms := [(35, 1), (41, 1), (70, 2), (99, 1), (105, 1)], rhs := 4, weight := 500000 },
  { label := "['paired_diagonal', 36]", terms := [(36, 1), (44, 1), (72, 2), (100, 1), (108, 1)], rhs := 4, weight := 1000000 },
  { label := "['paired_diagonal', 37]", terms := [(37, 1), (47, 1), (74, 2), (101, 1), (111, 1)], rhs := 4, weight := 750000 },
  { label := "['paired_diagonal', 38]", terms := [(38, 1), (50, 1), (76, 2), (102, 1), (114, 1)], rhs := 4, weight := 1000000 },
  { label := "['paired_diagonal', 39]", terms := [(39, 1), (53, 1), (78, 2), (103, 1), (117, 1)], rhs := 4, weight := 750000 },
  { label := "['paired_diagonal', 41]", terms := [(41, 1), (59, 1), (82, 2), (105, 1), (123, 1)], rhs := 4, weight := 250000 },
  { label := "['paired_diagonal', 43]", terms := [(1, 1), (43, 1), (65, 1), (86, 2), (107, 1)], rhs := 4, weight := 1000000 },
  { label := "['paired_diagonal', 45]", terms := [(7, 1), (45, 1), (71, 1), (90, 2), (109, 1)], rhs := 4, weight := 500000 },
  { label := "['paired_diagonal', 59]", terms := [(49, 1), (59, 1), (113, 1), (118, 2), (123, 1)], rhs := 4, weight := 250000 },
  { label := "['paired_diagonal', 60]", terms := [(52, 1), (60, 1), (116, 1), (120, 2), (124, 1)], rhs := 4, weight := 500000 },
  { label := "['paired_diagonal', 61]", terms := [(55, 1), (61, 1), (119, 1), (122, 2), (125, 1)], rhs := 4, weight := 500000 },
  { label := "['paired_diagonal', 63]", terms := [(61, 1), (63, 1), (125, 1), (126, 2), (127, 1)], rhs := 4, weight := 500000 },
  { label := "['large_link']", terms := [(128, -3), (129, -3), (130, -3), (131, -3), (132, -3), (133, -3), (134, -3), (135, -3), (136, -3), (137, -3), (138, -3), (139, -3), (140, -3), (141, -3), (142, -3), (143, -3), (144, -3), (145, -3), (146, -3), (147, -3), (148, -3), (149, -3), (150, -3), (151, -3), (152, -3), (153, -3), (154, -3), (155, -3), (156, -3), (157, -3), (158, -3), (159, -3), (160, -3), (161, -3), (162, -3), (163, -3), (164, -3), (165, -3), (166, -3), (167, -3), (168, -3), (169, -3), (170, -3), (171, -3), (172, -3), (173, -3), (174, -3), (175, -3), (176, -3), (177, -3), (178, -3), (179, -3), (180, -3), (181, -3), (182, -3), (183, -3), (184, -3), (185, -3), (186, -3), (187, -3), (188, -3), (189, -3), (190, -3), (191, -3), (192, -3), (193, -3), (194, -3), (195, -3), (196, -3), (197, -3), (198, -3), (199, -3), (200, -3), (201, -3), (202, -3), (203, -3), (204, -3), (205, -3), (206, -3), (207, -3), (208, -3), (209, -3), (210, -3), (211, -3), (212, -3), (213, -3), (214, -3), (215, -3), (216, -3), (217, -3), (218, -3), (219, -3), (220, -3), (221, -3), (222, -3), (223, -3), (224, -3), (225, -3), (226, -3), (227, -3), (228, -3), (229, -3), (230, -3), (231, -3), (232, -3), (233, -3), (234, -3), (235, -3), (236, -3), (237, -3), (238, -3), (239, -3), (240, -3), (241, -3), (242, -3), (243, -3), (244, -3), (245, -3), (246, -3), (247, -3), (248, -3), (249, -3), (250, -3), (251, -3), (252, -3), (253, -3), (254, -3), (255, -3)], rhs := -128, weight := 1000000 },
  { label := "upper_bound(3)", terms := [(3, 1)], rhs := 1, weight := 500000 },
  { label := "upper_bound(48)", terms := [(48, 1)], rhs := 1, weight := 1 },
  { label := "upper_bound(49)", terms := [(49, 1)], rhs := 1, weight := 750000 },
  { label := "upper_bound(51)", terms := [(51, 1)], rhs := 1, weight := 1000000 },
  { label := "upper_bound(55)", terms := [(55, 1)], rhs := 1, weight := 500000 },
  { label := "upper_bound(57)", terms := [(57, 1)], rhs := 1, weight := 1000000 },
  { label := "upper_bound(58)", terms := [(58, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(59)", terms := [(59, 1)], rhs := 1, weight := 250000 },
  { label := "upper_bound(63)", terms := [(63, 1)], rhs := 1, weight := 500000 },
  { label := "upper_bound(64)", terms := [(64, 1)], rhs := 1, weight := 500000 },
  { label := "upper_bound(67)", terms := [(67, 1)], rhs := 1, weight := 500000 },
  { label := "upper_bound(68)", terms := [(68, 1)], rhs := 1, weight := 500000 },
  { label := "upper_bound(73)", terms := [(73, 1)], rhs := 1, weight := 500000 },
  { label := "upper_bound(76)", terms := [(76, 1)], rhs := 1, weight := 1 },
  { label := "upper_bound(77)", terms := [(77, 1)], rhs := 1, weight := 750000 },
  { label := "upper_bound(78)", terms := [(78, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(79)", terms := [(79, 1)], rhs := 1, weight := 250000 },
  { label := "upper_bound(83)", terms := [(83, 1)], rhs := 1, weight := 1000000 },
  { label := "upper_bound(85)", terms := [(85, 1)], rhs := 1, weight := 500000 },
  { label := "upper_bound(87)", terms := [(87, 1)], rhs := 1, weight := 1500000 },
  { label := "upper_bound(127)", terms := [(127, 1)], rhs := 1, weight := 500000 },
  { label := "upper_bound(128)", terms := [(128, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(129)", terms := [(129, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(130)", terms := [(130, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(131)", terms := [(131, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(132)", terms := [(132, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(133)", terms := [(133, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(134)", terms := [(134, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(135)", terms := [(135, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(136)", terms := [(136, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(137)", terms := [(137, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(138)", terms := [(138, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(139)", terms := [(139, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(140)", terms := [(140, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(141)", terms := [(141, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(142)", terms := [(142, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(143)", terms := [(143, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(144)", terms := [(144, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(145)", terms := [(145, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(146)", terms := [(146, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(147)", terms := [(147, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(148)", terms := [(148, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(149)", terms := [(149, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(150)", terms := [(150, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(151)", terms := [(151, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(152)", terms := [(152, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(153)", terms := [(153, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(154)", terms := [(154, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(155)", terms := [(155, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(156)", terms := [(156, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(157)", terms := [(157, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(158)", terms := [(158, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(159)", terms := [(159, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(160)", terms := [(160, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(161)", terms := [(161, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(162)", terms := [(162, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(163)", terms := [(163, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(164)", terms := [(164, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(165)", terms := [(165, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(166)", terms := [(166, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(167)", terms := [(167, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(168)", terms := [(168, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(169)", terms := [(169, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(170)", terms := [(170, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(171)", terms := [(171, 1)], rhs := 1, weight := 2750000 },
  { label := "upper_bound(173)", terms := [(173, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(175)", terms := [(175, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(177)", terms := [(177, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(178)", terms := [(178, 1)], rhs := 1, weight := 1500000 },
  { label := "upper_bound(179)", terms := [(179, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(180)", terms := [(180, 1)], rhs := 1, weight := 2000000 },
  { label := "upper_bound(181)", terms := [(181, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(183)", terms := [(183, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(185)", terms := [(185, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(186)", terms := [(186, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(187)", terms := [(187, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(188)", terms := [(188, 1)], rhs := 1, weight := 2000000 },
  { label := "upper_bound(189)", terms := [(189, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(190)", terms := [(190, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(191)", terms := [(191, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(192)", terms := [(192, 1)], rhs := 1, weight := 2750000 },
  { label := "upper_bound(193)", terms := [(193, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(194)", terms := [(194, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(195)", terms := [(195, 1)], rhs := 1, weight := 2750000 },
  { label := "upper_bound(196)", terms := [(196, 1)], rhs := 1, weight := 2750000 },
  { label := "upper_bound(197)", terms := [(197, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(198)", terms := [(198, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(199)", terms := [(199, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(201)", terms := [(201, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(203)", terms := [(203, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(205)", terms := [(205, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(207)", terms := [(207, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(208)", terms := [(208, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(209)", terms := [(209, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(211)", terms := [(211, 1)], rhs := 1, weight := 3000000 },
  { label := "upper_bound(214)", terms := [(214, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(215)", terms := [(215, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(216)", terms := [(216, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(217)", terms := [(217, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(218)", terms := [(218, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(219)", terms := [(219, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(220)", terms := [(220, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(221)", terms := [(221, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(222)", terms := [(222, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(223)", terms := [(223, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(224)", terms := [(224, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(225)", terms := [(225, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(226)", terms := [(226, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(227)", terms := [(227, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(228)", terms := [(228, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(229)", terms := [(229, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(230)", terms := [(230, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(231)", terms := [(231, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(232)", terms := [(232, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(233)", terms := [(233, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(234)", terms := [(234, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(235)", terms := [(235, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(236)", terms := [(236, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(237)", terms := [(237, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(238)", terms := [(238, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(239)", terms := [(239, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(240)", terms := [(240, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(241)", terms := [(241, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(242)", terms := [(242, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(243)", terms := [(243, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(244)", terms := [(244, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(245)", terms := [(245, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(246)", terms := [(246, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(247)", terms := [(247, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(248)", terms := [(248, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(249)", terms := [(249, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(250)", terms := [(250, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(251)", terms := [(251, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(252)", terms := [(252, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(253)", terms := [(253, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(254)", terms := [(254, 1)], rhs := 0, weight := 3000000 },
  { label := "upper_bound(255)", terms := [(255, 1)], rhs := 0, weight := 3000000 },
  { label := "lower_bound(24)", terms := [(24, -1)], rhs := 0, weight := 833333 },
  { label := "lower_bound(28)", terms := [(28, -1)], rhs := 0, weight := 500000 },
  { label := "lower_bound(102)", terms := [(102, -1)], rhs := 0, weight := 333333 }
]









/-- Exact certificate for q128_v6: normalized bound 217/3; all analytic rows follow. -/
def q128_v6Rows : Array FibreRow := #[
  { label := "['outside_link', 3]", terms := [(3, 1), (9, 1)], rhs := 1, weight := 9 },
  { label := "['outside_link', 10]", terms := [(10, 1), (16, 1)], rhs := 1, weight := 6 },
  { label := "['outside_link', 13]", terms := [(13, 1), (19, 1)], rhs := 1, weight := 6 },
  { label := "['outside_link', 14]", terms := [(14, 1), (20, 1)], rhs := 1, weight := 12 },
  { label := "['outside_link', 15]", terms := [(15, 1), (21, 1)], rhs := 1, weight := 12 },
  { label := "['single_diagonal', 26]", terms := [(26, 1), (52, 2), (78, 1)], rhs := 3, weight := 12 },
  { label := "['single_diagonal', 28]", terms := [(28, 1), (56, 2), (84, 1)], rhs := 3, weight := 12 },
  { label := "['single_diagonal', 29]", terms := [(29, 1), (58, 2), (87, 1)], rhs := 3, weight := 12 },
  { label := "['single_diagonal', 30]", terms := [(30, 1), (60, 2), (90, 1)], rhs := 3, weight := 12 },
  { label := "['single_diagonal', 31]", terms := [(31, 1), (62, 2), (93, 1)], rhs := 3, weight := 12 },
  { label := "['single_diagonal', 33]", terms := [(33, 1), (66, 2), (99, 1)], rhs := 3, weight := 12 },
  { label := "['outside_link', 37]", terms := [(37, 1), (43, 1)], rhs := 1, weight := 6 },
  { label := "['outside_link', 38]", terms := [(38, 1), (44, 1)], rhs := 1, weight := 12 },
  { label := "['outside_link', 39]", terms := [(39, 1), (45, 1)], rhs := 1, weight := 12 },
  { label := "['outside_link', 40]", terms := [(40, 1), (46, 1)], rhs := 1, weight := 12 },
  { label := "['outside_link', 41]", terms := [(41, 1), (47, 1)], rhs := 1, weight := 12 },
  { label := "['outside_link', 42]", terms := [(42, 1), (48, 1)], rhs := 1, weight := 12 },
  { label := "['link_source', 43, 43]", terms := [(43, -1), (171, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 44, 44]", terms := [(44, -1), (172, 1)], rhs := 0, weight := 48 },
  { label := "['link_source', 45, 45]", terms := [(45, -1), (173, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 46, 46]", terms := [(46, -1), (174, 1)], rhs := 0, weight := 24 },
  { label := "['link_source', 47, 47]", terms := [(47, -1), (175, 1)], rhs := 0, weight := 18 },
  { label := "['link_source', 48, 48]", terms := [(48, -1), (176, 1)], rhs := 0, weight := 30 },
  { label := "['link_source', 48, 54]", terms := [(54, -1), (176, 1)], rhs := 0, weight := 18 },
  { label := "['link_source', 50, 50]", terms := [(50, -1), (178, 1)], rhs := 0, weight := 24 },
  { label := "['link_source', 50, 56]", terms := [(56, -1), (178, 1)], rhs := 0, weight := 24 },
  { label := "['link_source', 52, 52]", terms := [(52, -1), (180, 1)], rhs := 0, weight := 48 },
  { label := "['link_source', 54, 60]", terms := [(60, -1), (182, 1)], rhs := 0, weight := 18 },
  { label := "['link_source', 56, 62]", terms := [(62, -1), (184, 1)], rhs := 0, weight := 30 },
  { label := "['single_diagonal', 57]", terms := [(43, 1), (57, 1), (114, 2)], rhs := 3, weight := 6 },
  { label := "['link_source', 58, 58]", terms := [(58, -1), (186, 1)], rhs := 0, weight := 18 },
  { label := "['link_source', 60, 66]", terms := [(66, -1), (188, 1)], rhs := 0, weight := 48 },
  { label := "['single_diagonal', 60]", terms := [(52, 1), (60, 1), (120, 2)], rhs := 3, weight := 6 },
  { label := "['single_diagonal', 62]", terms := [(58, 1), (62, 1), (124, 2)], rhs := 3, weight := 6 },
  { label := "['link_source', 63, 69]", terms := [(69, -1), (191, 1)], rhs := 0, weight := 3 },
  { label := "['link_source', 68, 68]", terms := [(68, -1), (196, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 68, 74]", terms := [(74, -1), (196, 1)], rhs := 0, weight := 12 },
  { label := "['single_diagonal', 69]", terms := [(10, 2), (69, 1), (79, 1)], rhs := 3, weight := 3 },
  { label := "['link_source', 70, 76]", terms := [(76, -1), (198, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 72, 72]", terms := [(72, -1), (200, 1)], rhs := 0, weight := 24 },
  { label := "['link_source', 74, 80]", terms := [(80, -1), (202, 1)], rhs := 0, weight := 18 },
  { label := "['link_source', 76, 82]", terms := [(82, -1), (204, 1)], rhs := 0, weight := 24 },
  { label := "['link_source', 78, 78]", terms := [(78, -1), (206, 1)], rhs := 0, weight := 24 },
  { label := "['link_source', 78, 84]", terms := [(84, -1), (206, 1)], rhs := 0, weight := 24 },
  { label := "['link_source', 80, 86]", terms := [(86, -1), (208, 1)], rhs := 0, weight := 36 },
  { label := "['link_source', 81, 81]", terms := [(81, -1), (209, 1)], rhs := 0, weight := 6 },
  { label := "['link_source', 81, 87]", terms := [(87, -1), (209, 1)], rhs := 0, weight := 12 },
  { label := "['single_diagonal', 81]", terms := [(34, 2), (81, 1), (115, 1)], rhs := 3, weight := 6 },
  { label := "['link_source', 82, 88]", terms := [(88, -1), (210, 1)], rhs := 0, weight := 48 },
  { label := "['link_source', 83, 89]", terms := [(89, -1), (211, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 84, 90]", terms := [(90, -1), (212, 1)], rhs := 0, weight := 36 },
  { label := "['outside_link', 86]", terms := [(86, 1), (92, 1)], rhs := 1, weight := 12 },
  { label := "['outside_link', 89]", terms := [(89, 1), (95, 1)], rhs := 1, weight := 12 },
  { label := "['outside_link', 90]", terms := [(90, 1), (96, 1)], rhs := 1, weight := 12 },
  { label := "['single_diagonal', 97]", terms := [(35, 1), (66, 2), (97, 1)], rhs := 3, weight := 12 },
  { label := "['single_diagonal', 100]", terms := [(44, 1), (72, 2), (100, 1)], rhs := 3, weight := 12 },
  { label := "['single_diagonal', 101]", terms := [(47, 1), (74, 2), (101, 1)], rhs := 3, weight := 6 },
  { label := "['single_diagonal', 102]", terms := [(50, 1), (76, 2), (102, 1)], rhs := 3, weight := 12 },
  { label := "['single_diagonal', 103]", terms := [(53, 1), (78, 2), (103, 1)], rhs := 3, weight := 12 },
  { label := "['single_diagonal', 104]", terms := [(56, 1), (80, 2), (104, 1)], rhs := 3, weight := 12 },
  { label := "['single_diagonal', 105]", terms := [(59, 1), (82, 2), (105, 1)], rhs := 3, weight := 12 },
  { label := "['single_diagonal', 106]", terms := [(62, 1), (84, 2), (106, 1)], rhs := 3, weight := 12 },
  { label := "['single_diagonal', 108]", terms := [(68, 1), (88, 2), (108, 1)], rhs := 3, weight := 12 },
  { label := "['outside_link', 110]", terms := [(110, 1), (116, 1)], rhs := 1, weight := 12 },
  { label := "['outside_link', 112]", terms := [(112, 1), (118, 1)], rhs := 1, weight := 6 },
  { label := "['outside_link', 113]", terms := [(113, 1), (119, 1)], rhs := 1, weight := 6 },
  { label := "['outside_link', 115]", terms := [(115, 1), (121, 1)], rhs := 1, weight := 6 },
  { label := "['outside_link', 117]", terms := [(117, 1), (123, 1)], rhs := 1, weight := 12 },
  { label := "['outside_link', 121]", terms := [(121, 1), (127, 1)], rhs := 1, weight := 6 },
  { label := "['paired_diagonal', 0]", terms := [(0, 4), (64, 2)], rhs := 4, weight := 3 },
  { label := "['paired_diagonal', 3]", terms := [(3, 1), (6, 2), (9, 1), (67, 1), (73, 1)], rhs := 4, weight := 3 },
  { label := "['paired_diagonal', 6]", terms := [(6, 1), (12, 2), (18, 1), (70, 1), (82, 1)], rhs := 4, weight := 6 },
  { label := "['paired_diagonal', 16]", terms := [(16, 1), (32, 2), (48, 1), (80, 1), (112, 1)], rhs := 4, weight := 6 },
  { label := "['paired_diagonal', 18]", terms := [(18, 1), (36, 2), (54, 1), (82, 1), (118, 1)], rhs := 4, weight := 6 },
  { label := "['paired_diagonal', 22]", terms := [(2, 1), (22, 1), (44, 2), (66, 1), (86, 1)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 23]", terms := [(5, 1), (23, 1), (46, 2), (69, 1), (87, 1)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 24]", terms := [(8, 1), (24, 1), (48, 2), (72, 1), (88, 1)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 25]", terms := [(11, 1), (25, 1), (50, 2), (75, 1), (89, 1)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 27]", terms := [(17, 1), (27, 1), (54, 2), (81, 1), (91, 1)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 37]", terms := [(37, 1), (47, 1), (74, 2), (101, 1), (111, 1)], rhs := 4, weight := 6 },
  { label := "['paired_diagonal', 43]", terms := [(1, 1), (43, 1), (65, 1), (86, 2), (107, 1)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 44]", terms := [(4, 1), (44, 1), (68, 1), (88, 2), (108, 1)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 45]", terms := [(7, 1), (45, 1), (71, 1), (90, 2), (109, 1)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 47]", terms := [(13, 1), (47, 1), (77, 1), (94, 2), (111, 1)], rhs := 4, weight := 6 },
  { label := "['paired_diagonal', 49]", terms := [(19, 1), (49, 1), (83, 1), (98, 2), (113, 1)], rhs := 4, weight := 6 },
  { label := "['paired_diagonal', 61]", terms := [(55, 1), (61, 1), (119, 1), (122, 2), (125, 1)], rhs := 4, weight := 6 },
  { label := "['paired_diagonal', 63]", terms := [(61, 1), (63, 1), (125, 1), (126, 2), (127, 1)], rhs := 4, weight := 6 },
  { label := "['large_link']", terms := [(128, -3), (129, -3), (130, -3), (131, -3), (132, -3), (133, -3), (134, -3), (135, -3), (136, -3), (137, -3), (138, -3), (139, -3), (140, -3), (141, -3), (142, -3), (143, -3), (144, -3), (145, -3), (146, -3), (147, -3), (148, -3), (149, -3), (150, -3), (151, -3), (152, -3), (153, -3), (154, -3), (155, -3), (156, -3), (157, -3), (158, -3), (159, -3), (160, -3), (161, -3), (162, -3), (163, -3), (164, -3), (165, -3), (166, -3), (167, -3), (168, -3), (169, -3), (170, -3), (171, -3), (172, -3), (173, -3), (174, -3), (175, -3), (176, -3), (177, -3), (178, -3), (179, -3), (180, -3), (181, -3), (182, -3), (183, -3), (184, -3), (185, -3), (186, -3), (187, -3), (188, -3), (189, -3), (190, -3), (191, -3), (192, -3), (193, -3), (194, -3), (195, -3), (196, -3), (197, -3), (198, -3), (199, -3), (200, -3), (201, -3), (202, -3), (203, -3), (204, -3), (205, -3), (206, -3), (207, -3), (208, -3), (209, -3), (210, -3), (211, -3), (212, -3), (213, -3), (214, -3), (215, -3), (216, -3), (217, -3), (218, -3), (219, -3), (220, -3), (221, -3), (222, -3), (223, -3), (224, -3), (225, -3), (226, -3), (227, -3), (228, -3), (229, -3), (230, -3), (231, -3), (232, -3), (233, -3), (234, -3), (235, -3), (236, -3), (237, -3), (238, -3), (239, -3), (240, -3), (241, -3), (242, -3), (243, -3), (244, -3), (245, -3), (246, -3), (247, -3), (248, -3), (249, -3), (250, -3), (251, -3), (252, -3), (253, -3), (254, -3), (255, -3)], rhs := -128, weight := 16 },
  { label := "upper_bound(49)", terms := [(49, 1)], rhs := 1, weight := 6 },
  { label := "upper_bound(51)", terms := [(51, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(52)", terms := [(52, 1)], rhs := 1, weight := 30 },
  { label := "upper_bound(55)", terms := [(55, 1)], rhs := 1, weight := 6 },
  { label := "upper_bound(57)", terms := [(57, 1)], rhs := 1, weight := 6 },
  { label := "upper_bound(63)", terms := [(63, 1)], rhs := 1, weight := 6 },
  { label := "upper_bound(64)", terms := [(64, 1)], rhs := 1, weight := 6 },
  { label := "upper_bound(67)", terms := [(67, 1)], rhs := 1, weight := 9 },
  { label := "upper_bound(70)", terms := [(70, 1)], rhs := 1, weight := 6 },
  { label := "upper_bound(73)", terms := [(73, 1)], rhs := 1, weight := 9 },
  { label := "upper_bound(77)", terms := [(77, 1)], rhs := 1, weight := 6 },
  { label := "upper_bound(79)", terms := [(79, 1)], rhs := 1, weight := 9 },
  { label := "upper_bound(83)", terms := [(83, 1)], rhs := 1, weight := 6 },
  { label := "upper_bound(85)", terms := [(85, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(128)", terms := [(128, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(129)", terms := [(129, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(130)", terms := [(130, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(131)", terms := [(131, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(132)", terms := [(132, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(133)", terms := [(133, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(134)", terms := [(134, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(135)", terms := [(135, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(136)", terms := [(136, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(137)", terms := [(137, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(138)", terms := [(138, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(139)", terms := [(139, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(140)", terms := [(140, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(141)", terms := [(141, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(142)", terms := [(142, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(143)", terms := [(143, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(144)", terms := [(144, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(145)", terms := [(145, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(146)", terms := [(146, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(147)", terms := [(147, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(148)", terms := [(148, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(149)", terms := [(149, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(150)", terms := [(150, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(151)", terms := [(151, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(152)", terms := [(152, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(153)", terms := [(153, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(154)", terms := [(154, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(155)", terms := [(155, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(156)", terms := [(156, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(157)", terms := [(157, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(158)", terms := [(158, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(159)", terms := [(159, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(160)", terms := [(160, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(161)", terms := [(161, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(162)", terms := [(162, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(163)", terms := [(163, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(164)", terms := [(164, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(165)", terms := [(165, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(166)", terms := [(166, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(167)", terms := [(167, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(168)", terms := [(168, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(169)", terms := [(169, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(170)", terms := [(170, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(171)", terms := [(171, 1)], rhs := 1, weight := 36 },
  { label := "upper_bound(173)", terms := [(173, 1)], rhs := 1, weight := 36 },
  { label := "upper_bound(174)", terms := [(174, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(175)", terms := [(175, 1)], rhs := 1, weight := 30 },
  { label := "upper_bound(177)", terms := [(177, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(179)", terms := [(179, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(181)", terms := [(181, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(182)", terms := [(182, 1)], rhs := 1, weight := 30 },
  { label := "upper_bound(183)", terms := [(183, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(184)", terms := [(184, 1)], rhs := 1, weight := 18 },
  { label := "upper_bound(185)", terms := [(185, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(186)", terms := [(186, 1)], rhs := 1, weight := 30 },
  { label := "upper_bound(187)", terms := [(187, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(189)", terms := [(189, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(190)", terms := [(190, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(191)", terms := [(191, 1)], rhs := 1, weight := 45 },
  { label := "upper_bound(192)", terms := [(192, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(193)", terms := [(193, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(194)", terms := [(194, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(195)", terms := [(195, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(196)", terms := [(196, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(197)", terms := [(197, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(198)", terms := [(198, 1)], rhs := 1, weight := 36 },
  { label := "upper_bound(199)", terms := [(199, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(200)", terms := [(200, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(201)", terms := [(201, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(202)", terms := [(202, 1)], rhs := 1, weight := 30 },
  { label := "upper_bound(203)", terms := [(203, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(204)", terms := [(204, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(205)", terms := [(205, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(207)", terms := [(207, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(208)", terms := [(208, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(209)", terms := [(209, 1)], rhs := 1, weight := 30 },
  { label := "upper_bound(211)", terms := [(211, 1)], rhs := 1, weight := 36 },
  { label := "upper_bound(212)", terms := [(212, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(213)", terms := [(213, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(214)", terms := [(214, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(215)", terms := [(215, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(216)", terms := [(216, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(217)", terms := [(217, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(218)", terms := [(218, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(219)", terms := [(219, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(220)", terms := [(220, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(221)", terms := [(221, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(222)", terms := [(222, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(223)", terms := [(223, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(224)", terms := [(224, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(225)", terms := [(225, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(226)", terms := [(226, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(227)", terms := [(227, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(228)", terms := [(228, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(229)", terms := [(229, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(230)", terms := [(230, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(231)", terms := [(231, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(232)", terms := [(232, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(233)", terms := [(233, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(234)", terms := [(234, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(235)", terms := [(235, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(236)", terms := [(236, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(237)", terms := [(237, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(238)", terms := [(238, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(239)", terms := [(239, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(240)", terms := [(240, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(241)", terms := [(241, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(242)", terms := [(242, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(243)", terms := [(243, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(244)", terms := [(244, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(245)", terms := [(245, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(246)", terms := [(246, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(247)", terms := [(247, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(248)", terms := [(248, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(249)", terms := [(249, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(250)", terms := [(250, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(251)", terms := [(251, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(252)", terms := [(252, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(253)", terms := [(253, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(254)", terms := [(254, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(255)", terms := [(255, 1)], rhs := 0, weight := 48 },
  { label := "lower_bound(108)", terms := [(108, -1)], rhs := 0, weight := 12 }
]









/-- Exact certificate for q128_v12: normalized bound 70; all analytic rows follow. -/
def q128_v12Rows : Array FibreRow := #[
  { label := "['outside_link', 3]", terms := [(3, 1), (15, 1)], rhs := 1, weight := 2 },
  { label := "['outside_link', 9]", terms := [(9, 1), (21, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 15]", terms := [(15, 1), (27, 1)], rhs := 1, weight := 2 },
  { label := "['single_diagonal', 30]", terms := [(30, 1), (60, 2), (90, 1)], rhs := 3, weight := 4 },
  { label := "['outside_link', 31]", terms := [(31, 1), (43, 1)], rhs := 1, weight := 2 },
  { label := "['outside_link', 32]", terms := [(32, 1), (44, 1)], rhs := 1, weight := 2 },
  { label := "['outside_link', 33]", terms := [(33, 1), (45, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 34]", terms := [(34, 1), (46, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 35]", terms := [(35, 1), (47, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 36]", terms := [(36, 1), (48, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 37]", terms := [(37, 1), (49, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 38]", terms := [(38, 1), (50, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 39]", terms := [(39, 1), (51, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 40]", terms := [(40, 1), (52, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 41]", terms := [(41, 1), (53, 1)], rhs := 1, weight := 2 },
  { label := "['outside_link', 42]", terms := [(42, 1), (54, 1)], rhs := 1, weight := 4 },
  { label := "['link_source', 44, 44]", terms := [(44, -1), (172, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 45, 45]", terms := [(45, -1), (173, 1)], rhs := 0, weight := 4 },
  { label := "['link_source', 46, 46]", terms := [(46, -1), (174, 1)], rhs := 0, weight := 11 },
  { label := "['link_source', 47, 47]", terms := [(47, -1), (175, 1)], rhs := 0, weight := 4 },
  { label := "['link_source', 48, 48]", terms := [(48, -1), (176, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 49, 49]", terms := [(49, -1), (177, 1)], rhs := 0, weight := 2 },
  { label := "['link_source', 50, 50]", terms := [(50, -1), (178, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 52, 52]", terms := [(52, -1), (180, 1)], rhs := 0, weight := 10 },
  { label := "['link_source', 53, 53]", terms := [(53, -1), (181, 1)], rhs := 0, weight := 2 },
  { label := "['link_source', 54, 54]", terms := [(54, -1), (182, 1)], rhs := 0, weight := 8 },
  { label := "['link_source', 56, 56]", terms := [(56, -1), (184, 1)], rhs := 0, weight := 4 },
  { label := "['single_diagonal', 58]", terms := [(46, 1), (58, 1), (116, 2)], rhs := 3, weight := 1 },
  { label := "['link_source', 60, 60]", terms := [(60, -1), (188, 1)], rhs := 0, weight := 6 },
  { label := "['link_source', 60, 72]", terms := [(72, -1), (188, 1)], rhs := 0, weight := 4 },
  { label := "['link_source', 62, 62]", terms := [(62, -1), (190, 1)], rhs := 0, weight := 3 },
  { label := "['single_diagonal', 62]", terms := [(58, 1), (62, 1), (124, 2)], rhs := 3, weight := 1 },
  { label := "['single_diagonal', 63]", terms := [(61, 1), (63, 1), (126, 2)], rhs := 3, weight := 2 },
  { label := "['link_source', 64, 76]", terms := [(76, -1), (192, 1)], rhs := 0, weight := 4 },
  { label := "['link_source', 66, 78]", terms := [(78, -1), (194, 1)], rhs := 0, weight := 8 },
  { label := "['single_diagonal', 67]", terms := [(6, 2), (67, 1), (73, 1)], rhs := 3, weight := 1 },
  { label := "['link_source', 70, 82]", terms := [(82, -1), (198, 1)], rhs := 0, weight := 2 },
  { label := "['single_diagonal', 73]", terms := [(18, 2), (73, 1), (91, 1)], rhs := 3, weight := 1 },
  { label := "['link_source', 74, 86]", terms := [(86, -1), (202, 1)], rhs := 0, weight := 4 },
  { label := "['link_source', 75, 87]", terms := [(87, -1), (203, 1)], rhs := 0, weight := 4 },
  { label := "['link_source', 76, 88]", terms := [(88, -1), (204, 1)], rhs := 0, weight := 10 },
  { label := "['link_source', 77, 89]", terms := [(89, -1), (205, 1)], rhs := 0, weight := 4 },
  { label := "['link_source', 78, 90]", terms := [(90, -1), (206, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 79, 91]", terms := [(91, -1), (207, 1)], rhs := 0, weight := 1 },
  { label := "['link_source', 80, 92]", terms := [(92, -1), (208, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 81, 93]", terms := [(93, -1), (209, 1)], rhs := 0, weight := 1 },
  { label := "['link_source', 82, 94]", terms := [(94, -1), (210, 1)], rhs := 0, weight := 8 },
  { label := "['link_source', 83, 95]", terms := [(95, -1), (211, 1)], rhs := 0, weight := 1 },
  { label := "['link_source', 84, 96]", terms := [(96, -1), (212, 1)], rhs := 0, weight := 6 },
  { label := "['outside_link', 86]", terms := [(86, 1), (98, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 87]", terms := [(87, 1), (99, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 88]", terms := [(88, 1), (100, 1)], rhs := 1, weight := 2 },
  { label := "['outside_link', 89]", terms := [(89, 1), (101, 1)], rhs := 1, weight := 4 },
  { label := "['single_diagonal', 91]", terms := [(17, 1), (54, 2), (91, 1)], rhs := 3, weight := 2 },
  { label := "['outside_link', 92]", terms := [(92, 1), (104, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 93]", terms := [(93, 1), (105, 1)], rhs := 1, weight := 2 },
  { label := "['outside_link', 94]", terms := [(94, 1), (106, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 95]", terms := [(95, 1), (107, 1)], rhs := 1, weight := 2 },
  { label := "['single_diagonal', 95]", terms := [(29, 1), (62, 2), (95, 1)], rhs := 3, weight := 1 },
  { label := "['single_diagonal', 100]", terms := [(44, 1), (72, 2), (100, 1)], rhs := 3, weight := 2 },
  { label := "['single_diagonal', 102]", terms := [(50, 1), (76, 2), (102, 1)], rhs := 3, weight := 4 },
  { label := "['single_diagonal', 103]", terms := [(53, 1), (78, 2), (103, 1)], rhs := 3, weight := 4 },
  { label := "['outside_link', 113]", terms := [(113, 1), (125, 1)], rhs := 1, weight := 2 },
  { label := "['outside_link', 115]", terms := [(115, 1), (127, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 117]", terms := [(1, 1), (117, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 119]", terms := [(3, 1), (119, 1)], rhs := 1, weight := 2 },
  { label := "['outside_link', 121]", terms := [(5, 1), (121, 1)], rhs := 1, weight := 2 },
  { label := "['paired_diagonal', 0]", terms := [(0, 4), (64, 2)], rhs := 4, weight := 1 },
  { label := "['paired_diagonal', 6]", terms := [(6, 1), (12, 2), (18, 1), (70, 1), (82, 1)], rhs := 4, weight := 2 },
  { label := "['paired_diagonal', 22]", terms := [(2, 1), (22, 1), (44, 2), (66, 1), (86, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 23]", terms := [(5, 1), (23, 1), (46, 2), (69, 1), (87, 1)], rhs := 4, weight := 3 },
  { label := "['paired_diagonal', 24]", terms := [(8, 1), (24, 1), (48, 2), (72, 1), (88, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 25]", terms := [(11, 1), (25, 1), (50, 2), (75, 1), (89, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 26]", terms := [(14, 1), (26, 1), (52, 2), (78, 1), (90, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 27]", terms := [(17, 1), (27, 1), (54, 2), (81, 1), (91, 1)], rhs := 4, weight := 2 },
  { label := "['paired_diagonal', 28]", terms := [(20, 1), (28, 1), (56, 2), (84, 1), (92, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 29]", terms := [(23, 1), (29, 1), (58, 2), (87, 1), (93, 1)], rhs := 4, weight := 1 },
  { label := "['paired_diagonal', 31]", terms := [(29, 1), (31, 1), (62, 2), (93, 1), (95, 1)], rhs := 4, weight := 2 },
  { label := "['paired_diagonal', 32]", terms := [(32, 2), (64, 2), (96, 2)], rhs := 4, weight := 1 },
  { label := "['paired_diagonal', 41]", terms := [(41, 1), (59, 1), (82, 2), (105, 1), (123, 1)], rhs := 4, weight := 2 },
  { label := "['paired_diagonal', 44]", terms := [(4, 1), (44, 1), (68, 1), (88, 2), (108, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 45]", terms := [(7, 1), (45, 1), (71, 1), (90, 2), (109, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 46]", terms := [(10, 1), (46, 1), (74, 1), (92, 2), (110, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 47]", terms := [(13, 1), (47, 1), (77, 1), (94, 2), (111, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 48]", terms := [(16, 1), (48, 1), (80, 1), (96, 2), (112, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 57]", terms := [(43, 1), (57, 1), (107, 1), (114, 2), (121, 1)], rhs := 4, weight := 2 },
  { label := "['paired_diagonal', 59]", terms := [(49, 1), (59, 1), (113, 1), (118, 2), (123, 1)], rhs := 4, weight := 2 },
  { label := "['paired_diagonal', 60]", terms := [(52, 1), (60, 1), (116, 1), (120, 2), (124, 1)], rhs := 4, weight := 2 },
  { label := "['paired_diagonal', 61]", terms := [(55, 1), (61, 1), (119, 1), (122, 2), (125, 1)], rhs := 4, weight := 2 },
  { label := "['large_link']", terms := [(128, -3), (129, -3), (130, -3), (131, -3), (132, -3), (133, -3), (134, -3), (135, -3), (136, -3), (137, -3), (138, -3), (139, -3), (140, -3), (141, -3), (142, -3), (143, -3), (144, -3), (145, -3), (146, -3), (147, -3), (148, -3), (149, -3), (150, -3), (151, -3), (152, -3), (153, -3), (154, -3), (155, -3), (156, -3), (157, -3), (158, -3), (159, -3), (160, -3), (161, -3), (162, -3), (163, -3), (164, -3), (165, -3), (166, -3), (167, -3), (168, -3), (169, -3), (170, -3), (171, -3), (172, -3), (173, -3), (174, -3), (175, -3), (176, -3), (177, -3), (178, -3), (179, -3), (180, -3), (181, -3), (182, -3), (183, -3), (184, -3), (185, -3), (186, -3), (187, -3), (188, -3), (189, -3), (190, -3), (191, -3), (192, -3), (193, -3), (194, -3), (195, -3), (196, -3), (197, -3), (198, -3), (199, -3), (200, -3), (201, -3), (202, -3), (203, -3), (204, -3), (205, -3), (206, -3), (207, -3), (208, -3), (209, -3), (210, -3), (211, -3), (212, -3), (213, -3), (214, -3), (215, -3), (216, -3), (217, -3), (218, -3), (219, -3), (220, -3), (221, -3), (222, -3), (223, -3), (224, -3), (225, -3), (226, -3), (227, -3), (228, -3), (229, -3), (230, -3), (231, -3), (232, -3), (233, -3), (234, -3), (235, -3), (236, -3), (237, -3), (238, -3), (239, -3), (240, -3), (241, -3), (242, -3), (243, -3), (244, -3), (245, -3), (246, -3), (247, -3), (248, -3), (249, -3), (250, -3), (251, -3), (252, -3), (253, -3), (254, -3), (255, -3)], rhs := -128, weight := 4 },
  { label := "upper_bound(19)", terms := [(19, 1)], rhs := 1, weight := 4 },
  { label := "upper_bound(55)", terms := [(55, 1)], rhs := 1, weight := 2 },
  { label := "upper_bound(57)", terms := [(57, 1)], rhs := 1, weight := 2 },
  { label := "upper_bound(63)", terms := [(63, 1)], rhs := 1, weight := 2 },
  { label := "upper_bound(65)", terms := [(65, 1)], rhs := 1, weight := 4 },
  { label := "upper_bound(67)", terms := [(67, 1)], rhs := 1, weight := 3 },
  { label := "upper_bound(69)", terms := [(69, 1)], rhs := 1, weight := 1 },
  { label := "upper_bound(70)", terms := [(70, 1)], rhs := 1, weight := 2 },
  { label := "upper_bound(73)", terms := [(73, 1)], rhs := 1, weight := 2 },
  { label := "upper_bound(79)", terms := [(79, 1)], rhs := 1, weight := 4 },
  { label := "upper_bound(81)", terms := [(81, 1)], rhs := 1, weight := 2 },
  { label := "upper_bound(83)", terms := [(83, 1)], rhs := 1, weight := 4 },
  { label := "upper_bound(85)", terms := [(85, 1)], rhs := 1, weight := 4 },
  { label := "upper_bound(97)", terms := [(97, 1)], rhs := 1, weight := 4 },
  { label := "upper_bound(128)", terms := [(128, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(129)", terms := [(129, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(130)", terms := [(130, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(131)", terms := [(131, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(132)", terms := [(132, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(133)", terms := [(133, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(134)", terms := [(134, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(135)", terms := [(135, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(136)", terms := [(136, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(137)", terms := [(137, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(138)", terms := [(138, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(139)", terms := [(139, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(140)", terms := [(140, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(141)", terms := [(141, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(142)", terms := [(142, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(143)", terms := [(143, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(144)", terms := [(144, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(145)", terms := [(145, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(146)", terms := [(146, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(147)", terms := [(147, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(148)", terms := [(148, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(149)", terms := [(149, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(150)", terms := [(150, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(151)", terms := [(151, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(152)", terms := [(152, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(153)", terms := [(153, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(154)", terms := [(154, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(155)", terms := [(155, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(156)", terms := [(156, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(157)", terms := [(157, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(158)", terms := [(158, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(159)", terms := [(159, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(160)", terms := [(160, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(161)", terms := [(161, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(162)", terms := [(162, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(163)", terms := [(163, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(164)", terms := [(164, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(165)", terms := [(165, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(166)", terms := [(166, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(167)", terms := [(167, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(168)", terms := [(168, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(169)", terms := [(169, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(170)", terms := [(170, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(171)", terms := [(171, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(173)", terms := [(173, 1)], rhs := 1, weight := 8 },
  { label := "upper_bound(174)", terms := [(174, 1)], rhs := 1, weight := 1 },
  { label := "upper_bound(175)", terms := [(175, 1)], rhs := 1, weight := 8 },
  { label := "upper_bound(177)", terms := [(177, 1)], rhs := 1, weight := 10 },
  { label := "upper_bound(179)", terms := [(179, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(180)", terms := [(180, 1)], rhs := 1, weight := 2 },
  { label := "upper_bound(181)", terms := [(181, 1)], rhs := 1, weight := 10 },
  { label := "upper_bound(182)", terms := [(182, 1)], rhs := 1, weight := 4 },
  { label := "upper_bound(183)", terms := [(183, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(184)", terms := [(184, 1)], rhs := 1, weight := 8 },
  { label := "upper_bound(185)", terms := [(185, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(186)", terms := [(186, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(187)", terms := [(187, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(188)", terms := [(188, 1)], rhs := 1, weight := 2 },
  { label := "upper_bound(189)", terms := [(189, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(190)", terms := [(190, 1)], rhs := 1, weight := 9 },
  { label := "upper_bound(191)", terms := [(191, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(192)", terms := [(192, 1)], rhs := 1, weight := 8 },
  { label := "upper_bound(193)", terms := [(193, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(194)", terms := [(194, 1)], rhs := 1, weight := 4 },
  { label := "upper_bound(195)", terms := [(195, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(196)", terms := [(196, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(197)", terms := [(197, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(198)", terms := [(198, 1)], rhs := 1, weight := 10 },
  { label := "upper_bound(199)", terms := [(199, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(200)", terms := [(200, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(201)", terms := [(201, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(202)", terms := [(202, 1)], rhs := 1, weight := 8 },
  { label := "upper_bound(203)", terms := [(203, 1)], rhs := 1, weight := 8 },
  { label := "upper_bound(204)", terms := [(204, 1)], rhs := 1, weight := 2 },
  { label := "upper_bound(205)", terms := [(205, 1)], rhs := 1, weight := 8 },
  { label := "upper_bound(207)", terms := [(207, 1)], rhs := 1, weight := 11 },
  { label := "upper_bound(209)", terms := [(209, 1)], rhs := 1, weight := 11 },
  { label := "upper_bound(210)", terms := [(210, 1)], rhs := 1, weight := 4 },
  { label := "upper_bound(211)", terms := [(211, 1)], rhs := 1, weight := 11 },
  { label := "upper_bound(212)", terms := [(212, 1)], rhs := 1, weight := 6 },
  { label := "upper_bound(213)", terms := [(213, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(214)", terms := [(214, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(215)", terms := [(215, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(216)", terms := [(216, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(217)", terms := [(217, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(218)", terms := [(218, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(219)", terms := [(219, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(220)", terms := [(220, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(221)", terms := [(221, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(222)", terms := [(222, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(223)", terms := [(223, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(224)", terms := [(224, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(225)", terms := [(225, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(226)", terms := [(226, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(227)", terms := [(227, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(228)", terms := [(228, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(229)", terms := [(229, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(230)", terms := [(230, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(231)", terms := [(231, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(232)", terms := [(232, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(233)", terms := [(233, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(234)", terms := [(234, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(235)", terms := [(235, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(236)", terms := [(236, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(237)", terms := [(237, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(238)", terms := [(238, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(239)", terms := [(239, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(240)", terms := [(240, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(241)", terms := [(241, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(242)", terms := [(242, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(243)", terms := [(243, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(244)", terms := [(244, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(245)", terms := [(245, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(246)", terms := [(246, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(247)", terms := [(247, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(248)", terms := [(248, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(249)", terms := [(249, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(250)", terms := [(250, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(251)", terms := [(251, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(252)", terms := [(252, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(253)", terms := [(253, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(254)", terms := [(254, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(255)", terms := [(255, 1)], rhs := 0, weight := 12 },
  { label := "lower_bound(5)", terms := [(5, -1)], rhs := 0, weight := 1 }
]









/-- Exact certificate for q128_v14: normalized bound 143/2; all analytic rows follow. -/
def q128_v14Rows : Array FibreRow := #[
  { label := "['outside_link', 1]", terms := [(1, 1), (15, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 21]", terms := [(21, 1), (35, 1)], rhs := 1, weight := 2 },
  { label := "['outside_link', 29]", terms := [(29, 1), (43, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 30]", terms := [(30, 1), (44, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 31]", terms := [(31, 1), (45, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 33]", terms := [(33, 1), (47, 1)], rhs := 1, weight := 12 },
  { label := "['outside_link', 34]", terms := [(34, 1), (48, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 36]", terms := [(36, 1), (50, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 37]", terms := [(37, 1), (51, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 38]", terms := [(38, 1), (52, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 39]", terms := [(39, 1), (53, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 40]", terms := [(40, 1), (54, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 41]", terms := [(41, 1), (55, 1)], rhs := 1, weight := 3 },
  { label := "['link_source', 44, 44]", terms := [(44, -1), (172, 1)], rhs := 0, weight := 12 },
  { label := "['single_diagonal', 44]", terms := [(4, 1), (44, 1), (88, 2)], rhs := 3, weight := 4 },
  { label := "['link_source', 46, 46]", terms := [(46, -1), (174, 1)], rhs := 0, weight := 9 },
  { label := "['link_source', 47, 47]", terms := [(47, -1), (175, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 48, 48]", terms := [(48, -1), (176, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 49, 49]", terms := [(49, -1), (177, 1)], rhs := 0, weight := 2 },
  { label := "['single_diagonal', 49]", terms := [(19, 1), (49, 1), (98, 2)], rhs := 3, weight := 1 },
  { label := "['link_source', 50, 50]", terms := [(50, -1), (178, 1)], rhs := 0, weight := 10 },
  { label := "['link_source', 52, 52]", terms := [(52, -1), (180, 1)], rhs := 0, weight := 10 },
  { label := "['link_source', 52, 66]", terms := [(66, -1), (180, 1)], rhs := 0, weight := 2 },
  { label := "['link_source', 54, 54]", terms := [(54, -1), (182, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 55, 55]", terms := [(55, -1), (183, 1)], rhs := 0, weight := 1 },
  { label := "['link_source', 56, 56]", terms := [(56, -1), (184, 1)], rhs := 0, weight := 12 },
  { label := "['single_diagonal', 58]", terms := [(46, 1), (58, 1), (116, 2)], rhs := 3, weight := 1 },
  { label := "['single_diagonal', 59]", terms := [(49, 1), (59, 1), (118, 2)], rhs := 3, weight := 2 },
  { label := "['single_diagonal', 62]", terms := [(58, 1), (62, 1), (124, 2)], rhs := 3, weight := 1 },
  { label := "['link_source', 66, 66]", terms := [(66, -1), (194, 1)], rhs := 0, weight := 2 },
  { label := "['link_source', 66, 80]", terms := [(80, -1), (194, 1)], rhs := 0, weight := 8 },
  { label := "['single_diagonal', 67]", terms := [(6, 2), (67, 1), (73, 1)], rhs := 3, weight := 1 },
  { label := "['link_source', 68, 82]", terms := [(82, -1), (196, 1)], rhs := 0, weight := 2 },
  { label := "['link_source', 72, 86]", terms := [(86, -1), (200, 1)], rhs := 0, weight := 4 },
  { label := "['single_diagonal', 73]", terms := [(18, 2), (73, 1), (91, 1)], rhs := 3, weight := 1 },
  { label := "['link_source', 74, 88]", terms := [(88, -1), (202, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 75, 89]", terms := [(89, -1), (203, 1)], rhs := 0, weight := 4 },
  { label := "['link_source', 77, 91]", terms := [(91, -1), (205, 1)], rhs := 0, weight := 3 },
  { label := "['link_source', 78, 92]", terms := [(92, -1), (206, 1)], rhs := 0, weight := 11 },
  { label := "['link_source', 80, 94]", terms := [(94, -1), (208, 1)], rhs := 0, weight := 8 },
  { label := "['link_source', 82, 96]", terms := [(96, -1), (210, 1)], rhs := 0, weight := 8 },
  { label := "['link_source', 84, 84]", terms := [(84, -1), (212, 1)], rhs := 0, weight := 6 },
  { label := "['link_source', 84, 98]", terms := [(98, -1), (212, 1)], rhs := 0, weight := 4 },
  { label := "['outside_link', 86]", terms := [(86, 1), (100, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 88]", terms := [(88, 1), (102, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 89]", terms := [(89, 1), (103, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 91]", terms := [(91, 1), (105, 1)], rhs := 1, weight := 2 },
  { label := "['outside_link', 92]", terms := [(92, 1), (106, 1)], rhs := 1, weight := 1 },
  { label := "['single_diagonal', 92]", terms := [(20, 1), (56, 2), (92, 1)], rhs := 3, weight := 2 },
  { label := "['outside_link', 93]", terms := [(93, 1), (107, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 94]", terms := [(94, 1), (108, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 95]", terms := [(95, 1), (109, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 99]", terms := [(99, 1), (113, 1)], rhs := 1, weight := 1 },
  { label := "['single_diagonal', 99]", terms := [(41, 1), (70, 2), (99, 1)], rhs := 3, weight := 1 },
  { label := "['outside_link', 101]", terms := [(101, 1), (115, 1)], rhs := 1, weight := 4 },
  { label := "['single_diagonal', 102]", terms := [(50, 1), (76, 2), (102, 1)], rhs := 3, weight := 2 },
  { label := "['single_diagonal', 104]", terms := [(56, 1), (80, 2), (104, 1)], rhs := 3, weight := 4 },
  { label := "['single_diagonal', 105]", terms := [(59, 1), (82, 2), (105, 1)], rhs := 3, weight := 2 },
  { label := "['single_diagonal', 106]", terms := [(62, 1), (84, 2), (106, 1)], rhs := 3, weight := 3 },
  { label := "['outside_link', 114]", terms := [(0, 1), (114, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 117]", terms := [(3, 1), (117, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 119]", terms := [(5, 1), (119, 1)], rhs := 1, weight := 2 },
  { label := "['outside_link', 121]", terms := [(7, 1), (121, 1)], rhs := 1, weight := 4 },
  { label := "['outside_link', 123]", terms := [(9, 1), (123, 1)], rhs := 1, weight := 4 },
  { label := "['paired_diagonal', 6]", terms := [(6, 1), (12, 2), (18, 1), (70, 1), (82, 1)], rhs := 4, weight := 2 },
  { label := "['paired_diagonal', 21]", terms := [(21, 1), (42, 2), (63, 1), (85, 1), (127, 1)], rhs := 4, weight := 2 },
  { label := "['paired_diagonal', 22]", terms := [(2, 1), (22, 1), (44, 2), (66, 1), (86, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 23]", terms := [(5, 1), (23, 1), (46, 2), (69, 1), (87, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 24]", terms := [(8, 1), (24, 1), (48, 2), (72, 1), (88, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 25]", terms := [(11, 1), (25, 1), (50, 2), (75, 1), (89, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 26]", terms := [(14, 1), (26, 1), (52, 2), (78, 1), (90, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 27]", terms := [(17, 1), (27, 1), (54, 2), (81, 1), (91, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 28]", terms := [(20, 1), (28, 1), (56, 2), (84, 1), (92, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 32]", terms := [(32, 2), (64, 2), (96, 2)], rhs := 4, weight := 2 },
  { label := "['paired_diagonal', 33]", terms := [(33, 1), (35, 1), (66, 2), (97, 1), (99, 1)], rhs := 4, weight := 2 },
  { label := "['paired_diagonal', 46]", terms := [(10, 1), (46, 1), (74, 1), (92, 2), (110, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 47]", terms := [(13, 1), (47, 1), (77, 1), (94, 2), (111, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 48]", terms := [(16, 1), (48, 1), (80, 1), (96, 2), (112, 1)], rhs := 4, weight := 4 },
  { label := "['paired_diagonal', 49]", terms := [(19, 1), (49, 1), (83, 1), (98, 2), (113, 1)], rhs := 4, weight := 3 },
  { label := "['paired_diagonal', 60]", terms := [(52, 1), (60, 1), (116, 1), (120, 2), (124, 1)], rhs := 4, weight := 2 },
  { label := "['paired_diagonal', 61]", terms := [(55, 1), (61, 1), (119, 1), (122, 2), (125, 1)], rhs := 4, weight := 2 },
  { label := "['paired_diagonal', 63]", terms := [(61, 1), (63, 1), (125, 1), (126, 2), (127, 1)], rhs := 4, weight := 2 },
  { label := "['large_link']", terms := [(128, -3), (129, -3), (130, -3), (131, -3), (132, -3), (133, -3), (134, -3), (135, -3), (136, -3), (137, -3), (138, -3), (139, -3), (140, -3), (141, -3), (142, -3), (143, -3), (144, -3), (145, -3), (146, -3), (147, -3), (148, -3), (149, -3), (150, -3), (151, -3), (152, -3), (153, -3), (154, -3), (155, -3), (156, -3), (157, -3), (158, -3), (159, -3), (160, -3), (161, -3), (162, -3), (163, -3), (164, -3), (165, -3), (166, -3), (167, -3), (168, -3), (169, -3), (170, -3), (171, -3), (172, -3), (173, -3), (174, -3), (175, -3), (176, -3), (177, -3), (178, -3), (179, -3), (180, -3), (181, -3), (182, -3), (183, -3), (184, -3), (185, -3), (186, -3), (187, -3), (188, -3), (189, -3), (190, -3), (191, -3), (192, -3), (193, -3), (194, -3), (195, -3), (196, -3), (197, -3), (198, -3), (199, -3), (200, -3), (201, -3), (202, -3), (203, -3), (204, -3), (205, -3), (206, -3), (207, -3), (208, -3), (209, -3), (210, -3), (211, -3), (212, -3), (213, -3), (214, -3), (215, -3), (216, -3), (217, -3), (218, -3), (219, -3), (220, -3), (221, -3), (222, -3), (223, -3), (224, -3), (225, -3), (226, -3), (227, -3), (228, -3), (229, -3), (230, -3), (231, -3), (232, -3), (233, -3), (234, -3), (235, -3), (236, -3), (237, -3), (238, -3), (239, -3), (240, -3), (241, -3), (242, -3), (243, -3), (244, -3), (245, -3), (246, -3), (247, -3), (248, -3), (249, -3), (250, -3), (251, -3), (252, -3), (253, -3), (254, -3), (255, -3)], rhs := -128, weight := 4 },
  { label := "upper_bound(54)", terms := [(54, 1)], rhs := 1, weight := 4 },
  { label := "upper_bound(57)", terms := [(57, 1)], rhs := 1, weight := 4 },
  { label := "upper_bound(58)", terms := [(58, 1)], rhs := 1, weight := 2 },
  { label := "upper_bound(60)", terms := [(60, 1)], rhs := 1, weight := 2 },
  { label := "upper_bound(65)", terms := [(65, 1)], rhs := 1, weight := 4 },
  { label := "upper_bound(67)", terms := [(67, 1)], rhs := 1, weight := 3 },
  { label := "upper_bound(68)", terms := [(68, 1)], rhs := 1, weight := 4 },
  { label := "upper_bound(71)", terms := [(71, 1)], rhs := 1, weight := 4 },
  { label := "upper_bound(73)", terms := [(73, 1)], rhs := 1, weight := 2 },
  { label := "upper_bound(79)", terms := [(79, 1)], rhs := 1, weight := 4 },
  { label := "upper_bound(83)", terms := [(83, 1)], rhs := 1, weight := 1 },
  { label := "upper_bound(85)", terms := [(85, 1)], rhs := 1, weight := 2 },
  { label := "upper_bound(97)", terms := [(97, 1)], rhs := 1, weight := 2 },
  { label := "upper_bound(128)", terms := [(128, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(129)", terms := [(129, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(130)", terms := [(130, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(131)", terms := [(131, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(132)", terms := [(132, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(133)", terms := [(133, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(134)", terms := [(134, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(135)", terms := [(135, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(136)", terms := [(136, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(137)", terms := [(137, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(138)", terms := [(138, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(139)", terms := [(139, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(140)", terms := [(140, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(141)", terms := [(141, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(142)", terms := [(142, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(143)", terms := [(143, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(144)", terms := [(144, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(145)", terms := [(145, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(146)", terms := [(146, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(147)", terms := [(147, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(148)", terms := [(148, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(149)", terms := [(149, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(150)", terms := [(150, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(151)", terms := [(151, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(152)", terms := [(152, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(153)", terms := [(153, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(154)", terms := [(154, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(155)", terms := [(155, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(156)", terms := [(156, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(157)", terms := [(157, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(158)", terms := [(158, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(159)", terms := [(159, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(160)", terms := [(160, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(161)", terms := [(161, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(162)", terms := [(162, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(163)", terms := [(163, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(164)", terms := [(164, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(165)", terms := [(165, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(166)", terms := [(166, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(167)", terms := [(167, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(168)", terms := [(168, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(169)", terms := [(169, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(170)", terms := [(170, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(171)", terms := [(171, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(173)", terms := [(173, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(174)", terms := [(174, 1)], rhs := 1, weight := 3 },
  { label := "upper_bound(177)", terms := [(177, 1)], rhs := 1, weight := 10 },
  { label := "upper_bound(178)", terms := [(178, 1)], rhs := 1, weight := 2 },
  { label := "upper_bound(179)", terms := [(179, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(181)", terms := [(181, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(183)", terms := [(183, 1)], rhs := 1, weight := 11 },
  { label := "upper_bound(185)", terms := [(185, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(186)", terms := [(186, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(187)", terms := [(187, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(188)", terms := [(188, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(189)", terms := [(189, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(190)", terms := [(190, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(191)", terms := [(191, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(192)", terms := [(192, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(193)", terms := [(193, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(194)", terms := [(194, 1)], rhs := 1, weight := 2 },
  { label := "upper_bound(195)", terms := [(195, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(196)", terms := [(196, 1)], rhs := 1, weight := 10 },
  { label := "upper_bound(197)", terms := [(197, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(198)", terms := [(198, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(199)", terms := [(199, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(200)", terms := [(200, 1)], rhs := 1, weight := 8 },
  { label := "upper_bound(201)", terms := [(201, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(203)", terms := [(203, 1)], rhs := 1, weight := 8 },
  { label := "upper_bound(204)", terms := [(204, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(205)", terms := [(205, 1)], rhs := 1, weight := 9 },
  { label := "upper_bound(206)", terms := [(206, 1)], rhs := 1, weight := 1 },
  { label := "upper_bound(207)", terms := [(207, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(208)", terms := [(208, 1)], rhs := 1, weight := 4 },
  { label := "upper_bound(209)", terms := [(209, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(210)", terms := [(210, 1)], rhs := 1, weight := 4 },
  { label := "upper_bound(211)", terms := [(211, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(212)", terms := [(212, 1)], rhs := 1, weight := 2 },
  { label := "upper_bound(213)", terms := [(213, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(214)", terms := [(214, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(215)", terms := [(215, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(216)", terms := [(216, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(217)", terms := [(217, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(218)", terms := [(218, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(219)", terms := [(219, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(220)", terms := [(220, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(221)", terms := [(221, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(222)", terms := [(222, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(223)", terms := [(223, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(224)", terms := [(224, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(225)", terms := [(225, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(226)", terms := [(226, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(227)", terms := [(227, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(228)", terms := [(228, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(229)", terms := [(229, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(230)", terms := [(230, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(231)", terms := [(231, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(232)", terms := [(232, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(233)", terms := [(233, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(234)", terms := [(234, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(235)", terms := [(235, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(236)", terms := [(236, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(237)", terms := [(237, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(238)", terms := [(238, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(239)", terms := [(239, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(240)", terms := [(240, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(241)", terms := [(241, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(242)", terms := [(242, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(243)", terms := [(243, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(244)", terms := [(244, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(245)", terms := [(245, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(246)", terms := [(246, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(247)", terms := [(247, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(248)", terms := [(248, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(249)", terms := [(249, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(250)", terms := [(250, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(251)", terms := [(251, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(252)", terms := [(252, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(253)", terms := [(253, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(254)", terms := [(254, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(255)", terms := [(255, 1)], rhs := 0, weight := 12 },
  { label := "lower_bound(5)", terms := [(5, -1)], rhs := 0, weight := 2 },
  { label := "lower_bound(20)", terms := [(20, -1)], rhs := 0, weight := 2 },
  { label := "lower_bound(33)", terms := [(33, -1)], rhs := 0, weight := 10 },
  { label := "lower_bound(102)", terms := [(102, -1)], rhs := 0, weight := 2 }
]









/-- Exact certificate for q32_v0_low16: normalized bound 233/12; all analytic rows follow. -/
def q32_v0_low16Rows : Array FibreRow := #[
  { label := "['outside_zero_link', 0]", terms := [(0, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 1]", terms := [(1, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 2]", terms := [(2, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 3]", terms := [(3, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 4]", terms := [(4, 2)], rhs := 1, weight := 6 },
  { label := "['single_diagonal', 6]", terms := [(6, 1), (12, 2), (18, 1)], rhs := 3, weight := 12 },
  { label := "['outside_zero_link', 8]", terms := [(8, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 9]", terms := [(9, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 10]", terms := [(10, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 22]", terms := [(22, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 24]", terms := [(24, 2)], rhs := 1, weight := 6 },
  { label := "['single_diagonal', 25]", terms := [(11, 1), (18, 2), (25, 1)], rhs := 3, weight := 12 },
  { label := "['single_diagonal', 26]", terms := [(14, 1), (20, 2), (26, 1)], rhs := 3, weight := 12 },
  { label := "['outside_zero_link', 27]", terms := [(27, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 28]", terms := [(28, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 29]", terms := [(29, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 30]", terms := [(30, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 31]", terms := [(31, 2)], rhs := 1, weight := 6 },
  { label := "['paired_diagonal', 7]", terms := [(5, 1), (7, 1), (14, 2), (21, 1), (23, 1)], rhs := 4, weight := 12 },
  { label := "['large_link_sources']", terms := [(11, -3), (12, -3), (13, -3), (14, -3), (15, -3), (16, -3), (17, -3), (18, -3), (19, -3), (20, -3), (21, -3)], rhs := -32, weight := 8 },
  { label := "['low16']", terms := [(16, 4)], rhs := 3, weight := 9 },
  { label := "upper_bound(11)", terms := [(11, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(12)", terms := [(12, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(13)", terms := [(13, 1)], rhs := 1, weight := 36 },
  { label := "upper_bound(15)", terms := [(15, 1)], rhs := 1, weight := 36 },
  { label := "upper_bound(17)", terms := [(17, 1)], rhs := 1, weight := 36 },
  { label := "upper_bound(19)", terms := [(19, 1)], rhs := 1, weight := 36 },
  { label := "upper_bound(20)", terms := [(20, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(21)", terms := [(21, 1)], rhs := 1, weight := 24 }
]









/-- Exact certificate for q32_v0_high16: normalized bound 239/12; all analytic rows follow. -/
def q32_v0_high16Rows : Array FibreRow := #[
  { label := "['outside_zero_link', 1]", terms := [(1, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 2]", terms := [(2, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 3]", terms := [(3, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 4]", terms := [(4, 2)], rhs := 1, weight := 6 },
  { label := "['single_diagonal', 6]", terms := [(6, 1), (12, 2), (18, 1)], rhs := 3, weight := 12 },
  { label := "['outside_zero_link', 8]", terms := [(8, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 9]", terms := [(9, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 10]", terms := [(10, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 22]", terms := [(22, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 24]", terms := [(24, 2)], rhs := 1, weight := 6 },
  { label := "['single_diagonal', 25]", terms := [(11, 1), (18, 2), (25, 1)], rhs := 3, weight := 12 },
  { label := "['single_diagonal', 26]", terms := [(14, 1), (20, 2), (26, 1)], rhs := 3, weight := 12 },
  { label := "['outside_zero_link', 27]", terms := [(27, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 28]", terms := [(28, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 29]", terms := [(29, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 30]", terms := [(30, 2)], rhs := 1, weight := 6 },
  { label := "['outside_zero_link', 31]", terms := [(31, 2)], rhs := 1, weight := 6 },
  { label := "['paired_diagonal', 7]", terms := [(5, 1), (7, 1), (14, 2), (21, 1), (23, 1)], rhs := 4, weight := 12 },
  { label := "['large_link_sources']", terms := [(11, -3), (12, -3), (13, -3), (14, -3), (15, -3), (16, -3), (17, -3), (18, -3), (19, -3), (20, -3), (21, -3)], rhs := -32, weight := 8 },
  { label := "['inner_high_odd']", terms := [(0, 4), (16, 4)], rhs := 5, weight := 3 },
  { label := "upper_bound(11)", terms := [(11, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(12)", terms := [(12, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(13)", terms := [(13, 1)], rhs := 1, weight := 36 },
  { label := "upper_bound(15)", terms := [(15, 1)], rhs := 1, weight := 36 },
  { label := "upper_bound(16)", terms := [(16, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(17)", terms := [(17, 1)], rhs := 1, weight := 36 },
  { label := "upper_bound(19)", terms := [(19, 1)], rhs := 1, weight := 36 },
  { label := "upper_bound(20)", terms := [(20, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(21)", terms := [(21, 1)], rhs := 1, weight := 24 }
]









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

def aCoord (q : ℕ) (i : Fin q) : Fin (2*q) := ⟨i.val, by omega⟩
def bCoord (q : ℕ) (i : Fin q) : Fin (2*q) := ⟨q+i.val, by omega⟩
def aValue (q : ℕ) (x : Fin (2*q) → ℝ) (i : Fin q) : ℝ := x (aCoord q i)
def bValue (q : ℕ) (x : Fin (2*q) → ℝ) (i : Fin q) : ℝ := x (bCoord q i)
def residue (q : ℕ) (hq : 0 < q) (i : ℕ) : Fin q := ⟨i % q, Nat.mod_lt _ hq⟩

structure SemanticPremises (q v : ℕ) (hq : 0 < q) (C : Finset ℕ)
    (x : Fin (2*q) → ℝ) (h : ℝ) : Prop where
  a_nonneg : ∀ i, 0 ≤ aValue q x i
  a_upper : ∀ i, aValue q x i ≤ h
  b_nonneg : ∀ i, 0 ≤ bValue q x i
  b_upper : ∀ i, bValue q x i ≤ if i.val ∈ C then h else 0
  outside : ∀ i, i.val ∉ C →
    aValue q x i + aValue q x (residue q hq (i.val+v)) ≤ h
  link_source : ∀ i, bValue q x i ≤ aValue q x i
  link_target : ∀ i, bValue q x i ≤ aValue q x (residue q hq (i.val+v))
  single_diagonal : ∀ i,
    aValue q x i + aValue q x (residue q hq (3*i.val)) +
      2*aValue q x (residue q hq (2*i.val)) ≤ 3*h
  paired_diagonal : ∀ i,
    aValue q x i + aValue q x (residue q hq (i.val+q/2)) +
      aValue q x (residue q hq (3*i.val)) +
      aValue q x (residue q hq (3*i.val+q/2)) +
      2*aValue q x (residue q hq (2*i.val)) ≤ 4*h
  large_link : (q : ℝ)*h ≤ 3*∑ i, bValue q x i

structure ExtraPremises (q : ℕ) (hq : 0 < q) (x : Fin (2*q) → ℝ)
    (h : ℝ) (low inner : Bool) : Prop where
  low16 : low = true → 4*aValue q x (residue q hq 16) ≤ 3*h
  inner_high_odd : inner = true →
    4*(aValue q x (residue q hq 0)+aValue q x (residue q hq 16)) ≤ 5*h

inductive Rule where
  | upper (j : ℕ)
  | lower (j : ℕ)
  | outside (i : ℕ)
  | source (i : ℕ) (target : Bool)
  | single (i : ℕ)
  | paired (i : ℕ)
  | largeLink
  | largeSources
  | low16
  | innerHighOdd
  deriving DecidableEq

def delta (j i : ℕ) : ℤ := if j = i then 1 else 0

def ruleCoeff (q v : ℕ) (C : Finset ℕ) (r : Rule) (j : ℕ) : ℤ :=
  match r with
  | .upper i => delta j i
  | .lower i => -delta j i
  | .outside i => delta j (i%q)+delta j ((i+v)%q)
  | .source i target => delta j (q+i%q)-delta j ((i+(if target then v else 0))%q)
  | .single i => delta j (i%q)+delta j ((3*i)%q)+2*delta j ((2*i)%q)
  | .paired i => delta j (i%q)+delta j ((i+q/2)%q)+delta j ((3*i)%q)+
      delta j ((3*i+q/2)%q)+2*delta j ((2*i)%q)
  | .largeLink => if q ≤ j then -3 else 0
  | .largeSources => if j < q ∧ j ∈ C then -3 else 0
  | .low16 => 4*delta j (16%q)
  | .innerHighOdd => 4*delta j (0%q)+4*delta j (16%q)

def ruleRhs (q : ℕ) (C : Finset ℕ) (r : Rule) : ℤ :=
  match r with
  | .upper j => if j < q ∨ j-q ∈ C then 1 else 0
  | .lower _ => 0
  | .outside _ => 1
  | .source _ _ => 0
  | .single _ => 3
  | .paired _ => 4
  | .largeLink | .largeSources => -(q : ℤ)
  | .low16 => 3
  | .innerHighOdd => 5

def RuleValid (q : ℕ) (C : Finset ℕ) (low inner : Bool) (r : Rule) : Prop :=
  match r with
  | .upper j | .lower j => j < 2*q
  | .outside i => i < q ∧ i ∉ C
  | .source i _ | .single i | .paired i => i < q
  | .largeLink | .largeSources => True
  | .low16 => low = true
  | .innerHighOdd => inner = true

















def ruleSupport (q v : ℕ) (C : Finset ℕ) (r : Rule) : List ℕ :=
  match r with
  | .upper j | .lower j => [j]
  | .outside i => [i%q, (i+v)%q]
  | .source i target => [q+i%q, (i+(if target then v else 0))%q]
  | .single i => [i%q, (3*i)%q, (2*i)%q]
  | .paired i => [i%q, (i+q/2)%q, (3*i)%q, (3*i+q/2)%q, (2*i)%q]
  | .largeLink => (List.range q).map (fun i => q+i)
  | .largeSources => (List.range q).filter (fun i => i ∈ C)
  | .low16 => [16%q]
  | .innerHighOdd => [0%q, 16%q]





def RowCompatible (q v : ℕ) (C : Finset ℕ) (low inner : Bool)
    (row : FibreRow) (rule : Rule) : Prop :=
  RuleValid q C low inner rule ∧ row.rhs = ruleRhs q C rule ∧
    (∀ term ∈ row.terms, term.1 ∈ ruleSupport q v C rule) ∧
    ∀ j ∈ ruleSupport q v C rule, row.coeff j = ruleCoeff q v C rule j

instance (q v : ℕ) (C : Finset ℕ) (low inner : Bool)
    (row : FibreRow) (rule : Rule) : Decidable (RowCompatible q v C low inner row rule) := by
  unfold RowCompatible RuleValid
  cases rule <;> infer_instance







-- BEGIN GENERATED SEMANTIC ROW MAPS
def progression32 : Finset ℕ := {11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21}

def progression128 : Finset ℕ := {43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85}









def q32_v2Rules : List Rule := [
  .outside 1,
  .outside 9,
  .outside 10,
  .source 11 false,
  .source 12 false,
  .source 12 true,
  .source 13 true,
  .source 14 false,
  .source 16 true,
  .source 17 false,
  .source 18 true,
  .single 18,
  .source 20 true,
  .source 21 true,
  .outside 22,
  .outside 23,
  .single 26,
  .outside 28,
  .outside 29,
  .paired 0,
  .paired 4,
  .paired 6,
  .paired 7,
  .paired 11,
  .paired 15,
  .largeLink,
  .upper 13,
  .upper 15,
  .upper 16,
  .upper 17,
  .upper 19,
  .upper 32,
  .upper 33,
  .upper 34,
  .upper 35,
  .upper 36,
  .upper 37,
  .upper 38,
  .upper 39,
  .upper 40,
  .upper 41,
  .upper 42,
  .upper 43,
  .upper 46,
  .upper 47,
  .upper 48,
  .upper 50,
  .upper 51,
  .upper 53,
  .upper 54,
  .upper 55,
  .upper 56,
  .upper 57,
  .upper 58,
  .upper 59,
  .upper 60,
  .upper 61,
  .upper 62,
  .upper 63,
  .lower 1
]





def q128_v2Rules : List Rule := [
  .outside 7,
  .outside 10,
  .outside 11,
  .outside 15,
  .outside 16,
  .outside 19,
  .single 24,
  .single 25,
  .single 26,
  .single 27,
  .single 28,
  .single 29,
  .outside 31,
  .outside 32,
  .outside 33,
  .outside 37,
  .outside 41,
  .outside 42,
  .source 43 false,
  .source 44 false,
  .source 46 false,
  .source 46 true,
  .source 48 false,
  .source 48 true,
  .source 50 true,
  .source 52 true,
  .source 54 true,
  .source 56 true,
  .source 60 true,
  .source 64 true,
  .single 66,
  .source 67 true,
  .source 68 true,
  .single 69,
  .single 71,
  .source 72 false,
  .source 72 true,
  .source 74 false,
  .source 74 true,
  .source 76 true,
  .source 78 false,
  .source 78 true,
  .source 82 true,
  .source 84 true,
  .source 85 true,
  .outside 86,
  .outside 87,
  .outside 91,
  .outside 92,
  .outside 95,
  .outside 96,
  .outside 97,
  .single 101,
  .single 102,
  .single 103,
  .single 104,
  .single 105,
  .single 106,
  .outside 110,
  .single 111,
  .outside 113,
  .outside 115,
  .outside 116,
  .outside 119,
  .outside 121,
  .paired 0,
  .paired 3,
  .paired 4,
  .paired 15,
  .paired 20,
  .paired 22,
  .paired 23,
  .paired 27,
  .paired 28,
  .paired 31,
  .paired 35,
  .paired 36,
  .paired 37,
  .paired 38,
  .paired 39,
  .paired 41,
  .paired 43,
  .paired 45,
  .paired 59,
  .paired 60,
  .paired 61,
  .paired 63,
  .largeLink,
  .upper 3,
  .upper 48,
  .upper 49,
  .upper 51,
  .upper 55,
  .upper 57,
  .upper 58,
  .upper 59,
  .upper 63,
  .upper 64,
  .upper 67,
  .upper 68,
  .upper 73,
  .upper 76,
  .upper 77,
  .upper 78,
  .upper 79,
  .upper 83,
  .upper 85,
  .upper 87,
  .upper 127,
  .upper 128,
  .upper 129,
  .upper 130,
  .upper 131,
  .upper 132,
  .upper 133,
  .upper 134,
  .upper 135,
  .upper 136,
  .upper 137,
  .upper 138,
  .upper 139,
  .upper 140,
  .upper 141,
  .upper 142,
  .upper 143,
  .upper 144,
  .upper 145,
  .upper 146,
  .upper 147,
  .upper 148,
  .upper 149,
  .upper 150,
  .upper 151,
  .upper 152,
  .upper 153,
  .upper 154,
  .upper 155,
  .upper 156,
  .upper 157,
  .upper 158,
  .upper 159,
  .upper 160,
  .upper 161,
  .upper 162,
  .upper 163,
  .upper 164,
  .upper 165,
  .upper 166,
  .upper 167,
  .upper 168,
  .upper 169,
  .upper 170,
  .upper 171,
  .upper 173,
  .upper 175,
  .upper 177,
  .upper 178,
  .upper 179,
  .upper 180,
  .upper 181,
  .upper 183,
  .upper 185,
  .upper 186,
  .upper 187,
  .upper 188,
  .upper 189,
  .upper 190,
  .upper 191,
  .upper 192,
  .upper 193,
  .upper 194,
  .upper 195,
  .upper 196,
  .upper 197,
  .upper 198,
  .upper 199,
  .upper 201,
  .upper 203,
  .upper 205,
  .upper 207,
  .upper 208,
  .upper 209,
  .upper 211,
  .upper 214,
  .upper 215,
  .upper 216,
  .upper 217,
  .upper 218,
  .upper 219,
  .upper 220,
  .upper 221,
  .upper 222,
  .upper 223,
  .upper 224,
  .upper 225,
  .upper 226,
  .upper 227,
  .upper 228,
  .upper 229,
  .upper 230,
  .upper 231,
  .upper 232,
  .upper 233,
  .upper 234,
  .upper 235,
  .upper 236,
  .upper 237,
  .upper 238,
  .upper 239,
  .upper 240,
  .upper 241,
  .upper 242,
  .upper 243,
  .upper 244,
  .upper 245,
  .upper 246,
  .upper 247,
  .upper 248,
  .upper 249,
  .upper 250,
  .upper 251,
  .upper 252,
  .upper 253,
  .upper 254,
  .upper 255,
  .lower 24,
  .lower 28,
  .lower 102
]





def q128_v6Rules : List Rule := [
  .outside 3,
  .outside 10,
  .outside 13,
  .outside 14,
  .outside 15,
  .single 26,
  .single 28,
  .single 29,
  .single 30,
  .single 31,
  .single 33,
  .outside 37,
  .outside 38,
  .outside 39,
  .outside 40,
  .outside 41,
  .outside 42,
  .source 43 false,
  .source 44 false,
  .source 45 false,
  .source 46 false,
  .source 47 false,
  .source 48 false,
  .source 48 true,
  .source 50 false,
  .source 50 true,
  .source 52 false,
  .source 54 true,
  .source 56 true,
  .single 57,
  .source 58 false,
  .source 60 true,
  .single 60,
  .single 62,
  .source 63 true,
  .source 68 false,
  .source 68 true,
  .single 69,
  .source 70 true,
  .source 72 false,
  .source 74 true,
  .source 76 true,
  .source 78 false,
  .source 78 true,
  .source 80 true,
  .source 81 false,
  .source 81 true,
  .single 81,
  .source 82 true,
  .source 83 true,
  .source 84 true,
  .outside 86,
  .outside 89,
  .outside 90,
  .single 97,
  .single 100,
  .single 101,
  .single 102,
  .single 103,
  .single 104,
  .single 105,
  .single 106,
  .single 108,
  .outside 110,
  .outside 112,
  .outside 113,
  .outside 115,
  .outside 117,
  .outside 121,
  .paired 0,
  .paired 3,
  .paired 6,
  .paired 16,
  .paired 18,
  .paired 22,
  .paired 23,
  .paired 24,
  .paired 25,
  .paired 27,
  .paired 37,
  .paired 43,
  .paired 44,
  .paired 45,
  .paired 47,
  .paired 49,
  .paired 61,
  .paired 63,
  .largeLink,
  .upper 49,
  .upper 51,
  .upper 52,
  .upper 55,
  .upper 57,
  .upper 63,
  .upper 64,
  .upper 67,
  .upper 70,
  .upper 73,
  .upper 77,
  .upper 79,
  .upper 83,
  .upper 85,
  .upper 128,
  .upper 129,
  .upper 130,
  .upper 131,
  .upper 132,
  .upper 133,
  .upper 134,
  .upper 135,
  .upper 136,
  .upper 137,
  .upper 138,
  .upper 139,
  .upper 140,
  .upper 141,
  .upper 142,
  .upper 143,
  .upper 144,
  .upper 145,
  .upper 146,
  .upper 147,
  .upper 148,
  .upper 149,
  .upper 150,
  .upper 151,
  .upper 152,
  .upper 153,
  .upper 154,
  .upper 155,
  .upper 156,
  .upper 157,
  .upper 158,
  .upper 159,
  .upper 160,
  .upper 161,
  .upper 162,
  .upper 163,
  .upper 164,
  .upper 165,
  .upper 166,
  .upper 167,
  .upper 168,
  .upper 169,
  .upper 170,
  .upper 171,
  .upper 173,
  .upper 174,
  .upper 175,
  .upper 177,
  .upper 179,
  .upper 181,
  .upper 182,
  .upper 183,
  .upper 184,
  .upper 185,
  .upper 186,
  .upper 187,
  .upper 189,
  .upper 190,
  .upper 191,
  .upper 192,
  .upper 193,
  .upper 194,
  .upper 195,
  .upper 196,
  .upper 197,
  .upper 198,
  .upper 199,
  .upper 200,
  .upper 201,
  .upper 202,
  .upper 203,
  .upper 204,
  .upper 205,
  .upper 207,
  .upper 208,
  .upper 209,
  .upper 211,
  .upper 212,
  .upper 213,
  .upper 214,
  .upper 215,
  .upper 216,
  .upper 217,
  .upper 218,
  .upper 219,
  .upper 220,
  .upper 221,
  .upper 222,
  .upper 223,
  .upper 224,
  .upper 225,
  .upper 226,
  .upper 227,
  .upper 228,
  .upper 229,
  .upper 230,
  .upper 231,
  .upper 232,
  .upper 233,
  .upper 234,
  .upper 235,
  .upper 236,
  .upper 237,
  .upper 238,
  .upper 239,
  .upper 240,
  .upper 241,
  .upper 242,
  .upper 243,
  .upper 244,
  .upper 245,
  .upper 246,
  .upper 247,
  .upper 248,
  .upper 249,
  .upper 250,
  .upper 251,
  .upper 252,
  .upper 253,
  .upper 254,
  .upper 255,
  .lower 108
]





def q128_v12Rules : List Rule := [
  .outside 3,
  .outside 9,
  .outside 15,
  .single 30,
  .outside 31,
  .outside 32,
  .outside 33,
  .outside 34,
  .outside 35,
  .outside 36,
  .outside 37,
  .outside 38,
  .outside 39,
  .outside 40,
  .outside 41,
  .outside 42,
  .source 44 false,
  .source 45 false,
  .source 46 false,
  .source 47 false,
  .source 48 false,
  .source 49 false,
  .source 50 false,
  .source 52 false,
  .source 53 false,
  .source 54 false,
  .source 56 false,
  .single 58,
  .source 60 false,
  .source 60 true,
  .source 62 false,
  .single 62,
  .single 63,
  .source 64 true,
  .source 66 true,
  .single 67,
  .source 70 true,
  .single 73,
  .source 74 true,
  .source 75 true,
  .source 76 true,
  .source 77 true,
  .source 78 true,
  .source 79 true,
  .source 80 true,
  .source 81 true,
  .source 82 true,
  .source 83 true,
  .source 84 true,
  .outside 86,
  .outside 87,
  .outside 88,
  .outside 89,
  .single 91,
  .outside 92,
  .outside 93,
  .outside 94,
  .outside 95,
  .single 95,
  .single 100,
  .single 102,
  .single 103,
  .outside 113,
  .outside 115,
  .outside 117,
  .outside 119,
  .outside 121,
  .paired 0,
  .paired 6,
  .paired 22,
  .paired 23,
  .paired 24,
  .paired 25,
  .paired 26,
  .paired 27,
  .paired 28,
  .paired 29,
  .paired 31,
  .paired 32,
  .paired 41,
  .paired 44,
  .paired 45,
  .paired 46,
  .paired 47,
  .paired 48,
  .paired 57,
  .paired 59,
  .paired 60,
  .paired 61,
  .largeLink,
  .upper 19,
  .upper 55,
  .upper 57,
  .upper 63,
  .upper 65,
  .upper 67,
  .upper 69,
  .upper 70,
  .upper 73,
  .upper 79,
  .upper 81,
  .upper 83,
  .upper 85,
  .upper 97,
  .upper 128,
  .upper 129,
  .upper 130,
  .upper 131,
  .upper 132,
  .upper 133,
  .upper 134,
  .upper 135,
  .upper 136,
  .upper 137,
  .upper 138,
  .upper 139,
  .upper 140,
  .upper 141,
  .upper 142,
  .upper 143,
  .upper 144,
  .upper 145,
  .upper 146,
  .upper 147,
  .upper 148,
  .upper 149,
  .upper 150,
  .upper 151,
  .upper 152,
  .upper 153,
  .upper 154,
  .upper 155,
  .upper 156,
  .upper 157,
  .upper 158,
  .upper 159,
  .upper 160,
  .upper 161,
  .upper 162,
  .upper 163,
  .upper 164,
  .upper 165,
  .upper 166,
  .upper 167,
  .upper 168,
  .upper 169,
  .upper 170,
  .upper 171,
  .upper 173,
  .upper 174,
  .upper 175,
  .upper 177,
  .upper 179,
  .upper 180,
  .upper 181,
  .upper 182,
  .upper 183,
  .upper 184,
  .upper 185,
  .upper 186,
  .upper 187,
  .upper 188,
  .upper 189,
  .upper 190,
  .upper 191,
  .upper 192,
  .upper 193,
  .upper 194,
  .upper 195,
  .upper 196,
  .upper 197,
  .upper 198,
  .upper 199,
  .upper 200,
  .upper 201,
  .upper 202,
  .upper 203,
  .upper 204,
  .upper 205,
  .upper 207,
  .upper 209,
  .upper 210,
  .upper 211,
  .upper 212,
  .upper 213,
  .upper 214,
  .upper 215,
  .upper 216,
  .upper 217,
  .upper 218,
  .upper 219,
  .upper 220,
  .upper 221,
  .upper 222,
  .upper 223,
  .upper 224,
  .upper 225,
  .upper 226,
  .upper 227,
  .upper 228,
  .upper 229,
  .upper 230,
  .upper 231,
  .upper 232,
  .upper 233,
  .upper 234,
  .upper 235,
  .upper 236,
  .upper 237,
  .upper 238,
  .upper 239,
  .upper 240,
  .upper 241,
  .upper 242,
  .upper 243,
  .upper 244,
  .upper 245,
  .upper 246,
  .upper 247,
  .upper 248,
  .upper 249,
  .upper 250,
  .upper 251,
  .upper 252,
  .upper 253,
  .upper 254,
  .upper 255,
  .lower 5
]





def q128_v14Rules : List Rule := [
  .outside 1,
  .outside 21,
  .outside 29,
  .outside 30,
  .outside 31,
  .outside 33,
  .outside 34,
  .outside 36,
  .outside 37,
  .outside 38,
  .outside 39,
  .outside 40,
  .outside 41,
  .source 44 false,
  .single 44,
  .source 46 false,
  .source 47 false,
  .source 48 false,
  .source 49 false,
  .single 49,
  .source 50 false,
  .source 52 false,
  .source 52 true,
  .source 54 false,
  .source 55 false,
  .source 56 false,
  .single 58,
  .single 59,
  .single 62,
  .source 66 false,
  .source 66 true,
  .single 67,
  .source 68 true,
  .source 72 true,
  .single 73,
  .source 74 true,
  .source 75 true,
  .source 77 true,
  .source 78 true,
  .source 80 true,
  .source 82 true,
  .source 84 false,
  .source 84 true,
  .outside 86,
  .outside 88,
  .outside 89,
  .outside 91,
  .outside 92,
  .single 92,
  .outside 93,
  .outside 94,
  .outside 95,
  .outside 99,
  .single 99,
  .outside 101,
  .single 102,
  .single 104,
  .single 105,
  .single 106,
  .outside 114,
  .outside 117,
  .outside 119,
  .outside 121,
  .outside 123,
  .paired 6,
  .paired 21,
  .paired 22,
  .paired 23,
  .paired 24,
  .paired 25,
  .paired 26,
  .paired 27,
  .paired 28,
  .paired 32,
  .paired 33,
  .paired 46,
  .paired 47,
  .paired 48,
  .paired 49,
  .paired 60,
  .paired 61,
  .paired 63,
  .largeLink,
  .upper 54,
  .upper 57,
  .upper 58,
  .upper 60,
  .upper 65,
  .upper 67,
  .upper 68,
  .upper 71,
  .upper 73,
  .upper 79,
  .upper 83,
  .upper 85,
  .upper 97,
  .upper 128,
  .upper 129,
  .upper 130,
  .upper 131,
  .upper 132,
  .upper 133,
  .upper 134,
  .upper 135,
  .upper 136,
  .upper 137,
  .upper 138,
  .upper 139,
  .upper 140,
  .upper 141,
  .upper 142,
  .upper 143,
  .upper 144,
  .upper 145,
  .upper 146,
  .upper 147,
  .upper 148,
  .upper 149,
  .upper 150,
  .upper 151,
  .upper 152,
  .upper 153,
  .upper 154,
  .upper 155,
  .upper 156,
  .upper 157,
  .upper 158,
  .upper 159,
  .upper 160,
  .upper 161,
  .upper 162,
  .upper 163,
  .upper 164,
  .upper 165,
  .upper 166,
  .upper 167,
  .upper 168,
  .upper 169,
  .upper 170,
  .upper 171,
  .upper 173,
  .upper 174,
  .upper 177,
  .upper 178,
  .upper 179,
  .upper 181,
  .upper 183,
  .upper 185,
  .upper 186,
  .upper 187,
  .upper 188,
  .upper 189,
  .upper 190,
  .upper 191,
  .upper 192,
  .upper 193,
  .upper 194,
  .upper 195,
  .upper 196,
  .upper 197,
  .upper 198,
  .upper 199,
  .upper 200,
  .upper 201,
  .upper 203,
  .upper 204,
  .upper 205,
  .upper 206,
  .upper 207,
  .upper 208,
  .upper 209,
  .upper 210,
  .upper 211,
  .upper 212,
  .upper 213,
  .upper 214,
  .upper 215,
  .upper 216,
  .upper 217,
  .upper 218,
  .upper 219,
  .upper 220,
  .upper 221,
  .upper 222,
  .upper 223,
  .upper 224,
  .upper 225,
  .upper 226,
  .upper 227,
  .upper 228,
  .upper 229,
  .upper 230,
  .upper 231,
  .upper 232,
  .upper 233,
  .upper 234,
  .upper 235,
  .upper 236,
  .upper 237,
  .upper 238,
  .upper 239,
  .upper 240,
  .upper 241,
  .upper 242,
  .upper 243,
  .upper 244,
  .upper 245,
  .upper 246,
  .upper 247,
  .upper 248,
  .upper 249,
  .upper 250,
  .upper 251,
  .upper 252,
  .upper 253,
  .upper 254,
  .upper 255,
  .lower 5,
  .lower 20,
  .lower 33,
  .lower 102
]





def q32_v0_low16Rules : List Rule := [
  .outside 0,
  .outside 1,
  .outside 2,
  .outside 3,
  .outside 4,
  .single 6,
  .outside 8,
  .outside 9,
  .outside 10,
  .outside 22,
  .outside 24,
  .single 25,
  .single 26,
  .outside 27,
  .outside 28,
  .outside 29,
  .outside 30,
  .outside 31,
  .paired 7,
  .largeSources,
  .low16,
  .upper 11,
  .upper 12,
  .upper 13,
  .upper 15,
  .upper 17,
  .upper 19,
  .upper 20,
  .upper 21
]





def q32_v0_high16Rules : List Rule := [
  .outside 1,
  .outside 2,
  .outside 3,
  .outside 4,
  .single 6,
  .outside 8,
  .outside 9,
  .outside 10,
  .outside 22,
  .outside 24,
  .single 25,
  .single 26,
  .outside 27,
  .outside 28,
  .outside 29,
  .outside 30,
  .outside 31,
  .paired 7,
  .largeSources,
  .innerHighOdd,
  .upper 11,
  .upper 12,
  .upper 13,
  .upper 15,
  .upper 16,
  .upper 17,
  .upper 19,
  .upper 20,
  .upper 21
]





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


/-- Exact certificate for q32_v1: normalized bound 170/9; all analytic rows follow. -/
def q32_v1Rows : Array FibreRow := #[
  { label := "['outside_link', 2]", terms := [(2, 1), (3, 1)], rhs := 1, weight := 36 },
  { label := "['outside_link', 3]", terms := [(3, 1), (4, 1)], rhs := 1, weight := 36 },
  { label := "['single_diagonal', 6]", terms := [(6, 1), (12, 2), (18, 1)], rhs := 3, weight := 42 },
  { label := "['single_diagonal', 7]", terms := [(7, 1), (14, 2), (21, 1)], rhs := 3, weight := 12 },
  { label := "['outside_link', 8]", terms := [(8, 1), (9, 1)], rhs := 1, weight := 72 },
  { label := "['outside_link', 10]", terms := [(10, 1), (11, 1)], rhs := 1, weight := 48 },
  { label := "['link_source', 11, 11]", terms := [(11, -1), (43, 1)], rhs := 0, weight := 120 },
  { label := "['link_source', 12, 12]", terms := [(12, -1), (44, 1)], rhs := 0, weight := 120 },
  { label := "['link_source', 13, 14]", terms := [(14, -1), (45, 1)], rhs := 0, weight := 120 },
  { label := "['link_source', 14, 14]", terms := [(14, -1), (46, 1)], rhs := 0, weight := 24 },
  { label := "['single_diagonal', 15]", terms := [(13, 1), (15, 1), (30, 2)], rhs := 3, weight := 18 },
  { label := "['link_source', 17, 17]", terms := [(17, -1), (49, 1)], rhs := 0, weight := 90 },
  { label := "['link_source', 17, 18]", terms := [(18, -1), (49, 1)], rhs := 0, weight := 30 },
  { label := "['link_source', 18, 18]", terms := [(18, -1), (50, 1)], rhs := 0, weight := 120 },
  { label := "['link_source', 19, 20]", terms := [(20, -1), (51, 1)], rhs := 0, weight := 108 },
  { label := "['link_source', 20, 21]", terms := [(21, -1), (52, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 21, 22]", terms := [(22, -1), (53, 1)], rhs := 0, weight := 120 },
  { label := "['outside_link', 22]", terms := [(22, 1), (23, 1)], rhs := 1, weight := 12 },
  { label := "['single_diagonal', 25]", terms := [(11, 1), (18, 2), (25, 1)], rhs := 3, weight := 72 },
  { label := "['single_diagonal', 26]", terms := [(14, 1), (20, 2), (26, 1)], rhs := 3, weight := 72 },
  { label := "['outside_link', 28]", terms := [(28, 1), (29, 1)], rhs := 1, weight := 36 },
  { label := "['outside_link', 29]", terms := [(29, 1), (30, 1)], rhs := 1, weight := 36 },
  { label := "['outside_link', 31]", terms := [(0, 1), (31, 1)], rhs := 1, weight := 60 },
  { label := "['paired_diagonal', 0]", terms := [(0, 4), (16, 2)], rhs := 4, weight := 3 },
  { label := "['paired_diagonal', 5]", terms := [(5, 1), (10, 2), (15, 1), (21, 1), (31, 1)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 6]", terms := [(2, 1), (6, 1), (12, 2), (18, 1), (22, 1)], rhs := 4, weight := 36 },
  { label := "['paired_diagonal', 7]", terms := [(5, 1), (7, 1), (14, 2), (21, 1), (23, 1)], rhs := 4, weight := 60 },
  { label := "['paired_diagonal', 11]", terms := [(1, 1), (11, 1), (17, 1), (22, 2), (27, 1)], rhs := 4, weight := 72 },
  { label := "['paired_diagonal', 12]", terms := [(4, 1), (12, 1), (20, 1), (24, 2), (28, 1)], rhs := 4, weight := 36 },
  { label := "['large_link']", terms := [(32, -3), (33, -3), (34, -3), (35, -3), (36, -3), (37, -3), (38, -3), (39, -3), (40, -3), (41, -3), (42, -3), (43, -3), (44, -3), (45, -3), (46, -3), (47, -3), (48, -3), (49, -3), (50, -3), (51, -3), (52, -3), (53, -3), (54, -3), (55, -3), (56, -3), (57, -3), (58, -3), (59, -3), (60, -3), (61, -3), (62, -3), (63, -3)], rhs := -32, weight := 40 },
  { label := "upper_bound(13)", terms := [(13, 1)], rhs := 1, weight := 54 },
  { label := "upper_bound(15)", terms := [(15, 1)], rhs := 1, weight := 42 },
  { label := "upper_bound(16)", terms := [(16, 1)], rhs := 1, weight := 66 },
  { label := "upper_bound(17)", terms := [(17, 1)], rhs := 1, weight := 90 },
  { label := "upper_bound(19)", terms := [(19, 1)], rhs := 1, weight := 72 },
  { label := "upper_bound(32)", terms := [(32, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(33)", terms := [(33, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(34)", terms := [(34, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(35)", terms := [(35, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(36)", terms := [(36, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(37)", terms := [(37, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(38)", terms := [(38, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(39)", terms := [(39, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(40)", terms := [(40, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(41)", terms := [(41, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(42)", terms := [(42, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(46)", terms := [(46, 1)], rhs := 1, weight := 96 },
  { label := "upper_bound(47)", terms := [(47, 1)], rhs := 1, weight := 120 },
  { label := "upper_bound(48)", terms := [(48, 1)], rhs := 1, weight := 120 },
  { label := "upper_bound(51)", terms := [(51, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(52)", terms := [(52, 1)], rhs := 1, weight := 108 },
  { label := "upper_bound(54)", terms := [(54, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(55)", terms := [(55, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(56)", terms := [(56, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(57)", terms := [(57, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(58)", terms := [(58, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(59)", terms := [(59, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(60)", terms := [(60, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(61)", terms := [(61, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(62)", terms := [(62, 1)], rhs := 0, weight := 120 },
  { label := "upper_bound(63)", terms := [(63, 1)], rhs := 0, weight := 120 },
  { label := "lower_bound(6)", terms := [(6, -1)], rhs := 0, weight := 6 }
]








def q32_v1Rules : List Rule := [
  .outside 2,
  .outside 3,
  .single 6,
  .single 7,
  .outside 8,
  .outside 10,
  .source 11 false,
  .source 12 false,
  .source 13 true,
  .source 14 false,
  .single 15,
  .source 17 false,
  .source 17 true,
  .source 18 false,
  .source 19 true,
  .source 20 true,
  .source 21 true,
  .outside 22,
  .single 25,
  .single 26,
  .outside 28,
  .outside 29,
  .outside 31,
  .paired 0,
  .paired 5,
  .paired 6,
  .paired 7,
  .paired 11,
  .paired 12,
  .largeLink,
  .upper 13,
  .upper 15,
  .upper 16,
  .upper 17,
  .upper 19,
  .upper 32,
  .upper 33,
  .upper 34,
  .upper 35,
  .upper 36,
  .upper 37,
  .upper 38,
  .upper 39,
  .upper 40,
  .upper 41,
  .upper 42,
  .upper 46,
  .upper 47,
  .upper 48,
  .upper 51,
  .upper 52,
  .upper 54,
  .upper 55,
  .upper 56,
  .upper 57,
  .upper 58,
  .upper 59,
  .upper 60,
  .upper 61,
  .upper 62,
  .upper 63,
  .lower 6
]








/-- Exact certificate for q128_v13: normalized bound 1687/24; all analytic rows follow. -/
def q128_v13Rows : Array FibreRow := #[
  { label := "['outside_link', 2]", terms := [(2, 1), (15, 1)], rhs := 1, weight := 15 },
  { label := "['outside_link', 8]", terms := [(8, 1), (21, 1)], rhs := 1, weight := 15 },
  { label := "['outside_link', 21]", terms := [(21, 1), (34, 1)], rhs := 1, weight := 9 },
  { label := "['single_diagonal', 22]", terms := [(22, 1), (44, 2), (66, 1)], rhs := 3, weight := 24 },
  { label := "['single_diagonal', 24]", terms := [(24, 1), (48, 2), (72, 1)], rhs := 3, weight := 15 },
  { label := "['outside_link', 30]", terms := [(30, 1), (43, 1)], rhs := 1, weight := 24 },
  { label := "['outside_link', 31]", terms := [(31, 1), (44, 1)], rhs := 1, weight := 12 },
  { label := "['outside_link', 33]", terms := [(33, 1), (46, 1)], rhs := 1, weight := 24 },
  { label := "['outside_link', 34]", terms := [(34, 1), (47, 1)], rhs := 1, weight := 15 },
  { label := "['outside_link', 36]", terms := [(36, 1), (49, 1)], rhs := 1, weight := 24 },
  { label := "['outside_link', 37]", terms := [(37, 1), (50, 1)], rhs := 1, weight := 24 },
  { label := "['outside_link', 38]", terms := [(38, 1), (51, 1)], rhs := 1, weight := 24 },
  { label := "['outside_link', 39]", terms := [(39, 1), (52, 1)], rhs := 1, weight := 9 },
  { label := "['outside_link', 40]", terms := [(40, 1), (53, 1)], rhs := 1, weight := 24 },
  { label := "['outside_link', 42]", terms := [(42, 1), (55, 1)], rhs := 1, weight := 24 },
  { label := "['link_source', 43, 43]", terms := [(43, -1), (171, 1)], rhs := 0, weight := 48 },
  { label := "['link_source', 44, 44]", terms := [(44, -1), (172, 1)], rhs := 0, weight := 48 },
  { label := "['link_source', 45, 58]", terms := [(58, -1), (173, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 46, 46]", terms := [(46, -1), (174, 1)], rhs := 0, weight := 48 },
  { label := "['link_source', 47, 47]", terms := [(47, -1), (175, 1)], rhs := 0, weight := 24 },
  { label := "['link_source', 48, 48]", terms := [(48, -1), (176, 1)], rhs := 0, weight := 48 },
  { label := "['link_source', 49, 49]", terms := [(49, -1), (177, 1)], rhs := 0, weight := 24 },
  { label := "['link_source', 50, 50]", terms := [(50, -1), (178, 1)], rhs := 0, weight := 48 },
  { label := "['link_source', 52, 52]", terms := [(52, -1), (180, 1)], rhs := 0, weight := 45 },
  { label := "['link_source', 53, 53]", terms := [(53, -1), (181, 1)], rhs := 0, weight := 24 },
  { label := "['link_source', 54, 54]", terms := [(54, -1), (182, 1)], rhs := 0, weight := 24 },
  { label := "['link_source', 55, 55]", terms := [(55, -1), (183, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 56, 56]", terms := [(56, -1), (184, 1)], rhs := 0, weight := 24 },
  { label := "['single_diagonal', 57]", terms := [(43, 1), (57, 1), (114, 2)], rhs := 3, weight := 12 },
  { label := "['single_diagonal', 58]", terms := [(46, 1), (58, 1), (116, 2)], rhs := 3, weight := 12 },
  { label := "['single_diagonal', 60]", terms := [(52, 1), (60, 1), (120, 2)], rhs := 3, weight := 12 },
  { label := "['link_source', 65, 78]", terms := [(78, -1), (193, 1)], rhs := 0, weight := 42 },
  { label := "['link_source', 66, 66]", terms := [(66, -1), (194, 1)], rhs := 0, weight := 48 },
  { label := "['link_source', 69, 82]", terms := [(82, -1), (197, 1)], rhs := 0, weight := 30 },
  { label := "['single_diagonal', 70]", terms := [(12, 2), (70, 1), (82, 1)], rhs := 3, weight := 6 },
  { label := "['link_source', 73, 86]", terms := [(86, -1), (201, 1)], rhs := 0, weight := 48 },
  { label := "['single_diagonal', 73]", terms := [(18, 2), (73, 1), (91, 1)], rhs := 3, weight := 12 },
  { label := "['link_source', 74, 87]", terms := [(87, -1), (202, 1)], rhs := 0, weight := 27 },
  { label := "['link_source', 75, 88]", terms := [(88, -1), (203, 1)], rhs := 0, weight := 48 },
  { label := "['link_source', 76, 89]", terms := [(89, -1), (204, 1)], rhs := 0, weight := 24 },
  { label := "['link_source', 77, 90]", terms := [(90, -1), (205, 1)], rhs := 0, weight := 48 },
  { label := "['link_source', 78, 91]", terms := [(91, -1), (206, 1)], rhs := 0, weight := 36 },
  { label := "['link_source', 79, 92]", terms := [(92, -1), (207, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 80, 93]", terms := [(93, -1), (208, 1)], rhs := 0, weight := 24 },
  { label := "['link_source', 81, 94]", terms := [(94, -1), (209, 1)], rhs := 0, weight := 30 },
  { label := "['link_source', 83, 96]", terms := [(96, -1), (211, 1)], rhs := 0, weight := 48 },
  { label := "['link_source', 84, 97]", terms := [(97, -1), (212, 1)], rhs := 0, weight := 48 },
  { label := "['link_source', 85, 98]", terms := [(98, -1), (213, 1)], rhs := 0, weight := 24 },
  { label := "['outside_link', 86]", terms := [(86, 1), (99, 1)], rhs := 1, weight := 24 },
  { label := "['outside_link', 87]", terms := [(87, 1), (100, 1)], rhs := 1, weight := 24 },
  { label := "['single_diagonal', 87]", terms := [(5, 1), (46, 2), (87, 1)], rhs := 3, weight := 3 },
  { label := "['outside_link', 88]", terms := [(88, 1), (101, 1)], rhs := 1, weight := 15 },
  { label := "['outside_link', 89]", terms := [(89, 1), (102, 1)], rhs := 1, weight := 24 },
  { label := "['single_diagonal', 90]", terms := [(14, 1), (52, 2), (90, 1)], rhs := 3, weight := 6 },
  { label := "['outside_link', 91]", terms := [(91, 1), (104, 1)], rhs := 1, weight := 24 },
  { label := "['outside_link', 93]", terms := [(93, 1), (106, 1)], rhs := 1, weight := 24 },
  { label := "['single_diagonal', 94]", terms := [(26, 1), (60, 2), (94, 1)], rhs := 3, weight := 6 },
  { label := "['outside_link', 97]", terms := [(97, 1), (110, 1)], rhs := 1, weight := 18 },
  { label := "['single_diagonal', 97]", terms := [(35, 1), (66, 2), (97, 1)], rhs := 3, weight := 24 },
  { label := "['single_diagonal', 101]", terms := [(47, 1), (74, 2), (101, 1)], rhs := 3, weight := 9 },
  { label := "['single_diagonal', 103]", terms := [(53, 1), (78, 2), (103, 1)], rhs := 3, weight := 9 },
  { label := "['single_diagonal', 108]", terms := [(68, 1), (88, 2), (108, 1)], rhs := 3, weight := 12 },
  { label := "['outside_link', 115]", terms := [(0, 1), (115, 1)], rhs := 1, weight := 24 },
  { label := "['outside_link', 117]", terms := [(2, 1), (117, 1)], rhs := 1, weight := 9 },
  { label := "['outside_link', 118]", terms := [(3, 1), (118, 1)], rhs := 1, weight := 24 },
  { label := "['outside_link', 119]", terms := [(4, 1), (119, 1)], rhs := 1, weight := 12 },
  { label := "['outside_link', 121]", terms := [(6, 1), (121, 1)], rhs := 1, weight := 24 },
  { label := "['outside_link', 124]", terms := [(9, 1), (124, 1)], rhs := 1, weight := 24 },
  { label := "['outside_link', 127]", terms := [(12, 1), (127, 1)], rhs := 1, weight := 12 },
  { label := "['paired_diagonal', 5]", terms := [(5, 1), (10, 2), (15, 1), (69, 1), (79, 1)], rhs := 4, weight := 9 },
  { label := "['paired_diagonal', 23]", terms := [(5, 1), (23, 1), (46, 2), (69, 1), (87, 1)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 24]", terms := [(8, 1), (24, 1), (48, 2), (72, 1), (88, 1)], rhs := 4, weight := 9 },
  { label := "['paired_diagonal', 25]", terms := [(11, 1), (25, 1), (50, 2), (75, 1), (89, 1)], rhs := 4, weight := 24 },
  { label := "['paired_diagonal', 26]", terms := [(14, 1), (26, 1), (52, 2), (78, 1), (90, 1)], rhs := 4, weight := 18 },
  { label := "['paired_diagonal', 27]", terms := [(17, 1), (27, 1), (54, 2), (81, 1), (91, 1)], rhs := 4, weight := 24 },
  { label := "['paired_diagonal', 28]", terms := [(20, 1), (28, 1), (56, 2), (84, 1), (92, 1)], rhs := 4, weight := 24 },
  { label := "['paired_diagonal', 29]", terms := [(23, 1), (29, 1), (58, 2), (87, 1), (93, 1)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 31]", terms := [(29, 1), (31, 1), (62, 2), (93, 1), (95, 1)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 32]", terms := [(32, 2), (64, 2), (96, 2)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 39]", terms := [(39, 1), (53, 1), (78, 2), (103, 1), (117, 1)], rhs := 4, weight := 15 },
  { label := "['paired_diagonal', 41]", terms := [(41, 1), (59, 1), (82, 2), (105, 1), (123, 1)], rhs := 4, weight := 24 },
  { label := "['paired_diagonal', 43]", terms := [(1, 1), (43, 1), (65, 1), (86, 2), (107, 1)], rhs := 4, weight := 24 },
  { label := "['paired_diagonal', 44]", terms := [(4, 1), (44, 1), (68, 1), (88, 2), (108, 1)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 45]", terms := [(7, 1), (45, 1), (71, 1), (90, 2), (109, 1)], rhs := 4, weight := 24 },
  { label := "['paired_diagonal', 46]", terms := [(10, 1), (46, 1), (74, 1), (92, 2), (110, 1)], rhs := 4, weight := 6 },
  { label := "['paired_diagonal', 47]", terms := [(13, 1), (47, 1), (77, 1), (94, 2), (111, 1)], rhs := 4, weight := 24 },
  { label := "['paired_diagonal', 48]", terms := [(16, 1), (48, 1), (80, 1), (96, 2), (112, 1)], rhs := 4, weight := 24 },
  { label := "['paired_diagonal', 49]", terms := [(19, 1), (49, 1), (83, 1), (98, 2), (113, 1)], rhs := 4, weight := 24 },
  { label := "['paired_diagonal', 61]", terms := [(55, 1), (61, 1), (119, 1), (122, 2), (125, 1)], rhs := 4, weight := 12 },
  { label := "['paired_diagonal', 63]", terms := [(61, 1), (63, 1), (125, 1), (126, 2), (127, 1)], rhs := 4, weight := 12 },
  { label := "['large_link']", terms := [(128, -3), (129, -3), (130, -3), (131, -3), (132, -3), (133, -3), (134, -3), (135, -3), (136, -3), (137, -3), (138, -3), (139, -3), (140, -3), (141, -3), (142, -3), (143, -3), (144, -3), (145, -3), (146, -3), (147, -3), (148, -3), (149, -3), (150, -3), (151, -3), (152, -3), (153, -3), (154, -3), (155, -3), (156, -3), (157, -3), (158, -3), (159, -3), (160, -3), (161, -3), (162, -3), (163, -3), (164, -3), (165, -3), (166, -3), (167, -3), (168, -3), (169, -3), (170, -3), (171, -3), (172, -3), (173, -3), (174, -3), (175, -3), (176, -3), (177, -3), (178, -3), (179, -3), (180, -3), (181, -3), (182, -3), (183, -3), (184, -3), (185, -3), (186, -3), (187, -3), (188, -3), (189, -3), (190, -3), (191, -3), (192, -3), (193, -3), (194, -3), (195, -3), (196, -3), (197, -3), (198, -3), (199, -3), (200, -3), (201, -3), (202, -3), (203, -3), (204, -3), (205, -3), (206, -3), (207, -3), (208, -3), (209, -3), (210, -3), (211, -3), (212, -3), (213, -3), (214, -3), (215, -3), (216, -3), (217, -3), (218, -3), (219, -3), (220, -3), (221, -3), (222, -3), (223, -3), (224, -3), (225, -3), (226, -3), (227, -3), (228, -3), (229, -3), (230, -3), (231, -3), (232, -3), (233, -3), (234, -3), (235, -3), (236, -3), (237, -3), (238, -3), (239, -3), (240, -3), (241, -3), (242, -3), (243, -3), (244, -3), (245, -3), (246, -3), (247, -3), (248, -3), (249, -3), (250, -3), (251, -3), (252, -3), (253, -3), (254, -3), (255, -3)], rhs := -128, weight := 16 },
  { label := "upper_bound(43)", terms := [(43, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(57)", terms := [(57, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(63)", terms := [(63, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(67)", terms := [(67, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(69)", terms := [(69, 1)], rhs := 1, weight := 3 },
  { label := "upper_bound(70)", terms := [(70, 1)], rhs := 1, weight := 18 },
  { label := "upper_bound(73)", terms := [(73, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(76)", terms := [(76, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(79)", terms := [(79, 1)], rhs := 1, weight := 15 },
  { label := "upper_bound(85)", terms := [(85, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(95)", terms := [(95, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(97)", terms := [(97, 1)], rhs := 1, weight := 30 },
  { label := "upper_bound(128)", terms := [(128, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(129)", terms := [(129, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(130)", terms := [(130, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(131)", terms := [(131, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(132)", terms := [(132, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(133)", terms := [(133, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(134)", terms := [(134, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(135)", terms := [(135, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(136)", terms := [(136, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(137)", terms := [(137, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(138)", terms := [(138, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(139)", terms := [(139, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(140)", terms := [(140, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(141)", terms := [(141, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(142)", terms := [(142, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(143)", terms := [(143, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(144)", terms := [(144, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(145)", terms := [(145, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(146)", terms := [(146, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(147)", terms := [(147, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(148)", terms := [(148, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(149)", terms := [(149, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(150)", terms := [(150, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(151)", terms := [(151, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(152)", terms := [(152, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(153)", terms := [(153, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(154)", terms := [(154, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(155)", terms := [(155, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(156)", terms := [(156, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(157)", terms := [(157, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(158)", terms := [(158, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(159)", terms := [(159, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(160)", terms := [(160, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(161)", terms := [(161, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(162)", terms := [(162, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(163)", terms := [(163, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(164)", terms := [(164, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(165)", terms := [(165, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(166)", terms := [(166, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(167)", terms := [(167, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(168)", terms := [(168, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(169)", terms := [(169, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(170)", terms := [(170, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(173)", terms := [(173, 1)], rhs := 1, weight := 36 },
  { label := "upper_bound(175)", terms := [(175, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(177)", terms := [(177, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(179)", terms := [(179, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(180)", terms := [(180, 1)], rhs := 1, weight := 3 },
  { label := "upper_bound(181)", terms := [(181, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(182)", terms := [(182, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(183)", terms := [(183, 1)], rhs := 1, weight := 36 },
  { label := "upper_bound(184)", terms := [(184, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(185)", terms := [(185, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(186)", terms := [(186, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(187)", terms := [(187, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(188)", terms := [(188, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(189)", terms := [(189, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(190)", terms := [(190, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(191)", terms := [(191, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(192)", terms := [(192, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(193)", terms := [(193, 1)], rhs := 1, weight := 6 },
  { label := "upper_bound(195)", terms := [(195, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(196)", terms := [(196, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(197)", terms := [(197, 1)], rhs := 1, weight := 18 },
  { label := "upper_bound(198)", terms := [(198, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(199)", terms := [(199, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(200)", terms := [(200, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(202)", terms := [(202, 1)], rhs := 1, weight := 21 },
  { label := "upper_bound(204)", terms := [(204, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(206)", terms := [(206, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(207)", terms := [(207, 1)], rhs := 1, weight := 36 },
  { label := "upper_bound(208)", terms := [(208, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(209)", terms := [(209, 1)], rhs := 1, weight := 18 },
  { label := "upper_bound(210)", terms := [(210, 1)], rhs := 1, weight := 48 },
  { label := "upper_bound(213)", terms := [(213, 1)], rhs := 1, weight := 24 },
  { label := "upper_bound(214)", terms := [(214, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(215)", terms := [(215, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(216)", terms := [(216, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(217)", terms := [(217, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(218)", terms := [(218, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(219)", terms := [(219, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(220)", terms := [(220, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(221)", terms := [(221, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(222)", terms := [(222, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(223)", terms := [(223, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(224)", terms := [(224, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(225)", terms := [(225, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(226)", terms := [(226, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(227)", terms := [(227, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(228)", terms := [(228, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(229)", terms := [(229, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(230)", terms := [(230, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(231)", terms := [(231, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(232)", terms := [(232, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(233)", terms := [(233, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(234)", terms := [(234, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(235)", terms := [(235, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(236)", terms := [(236, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(237)", terms := [(237, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(238)", terms := [(238, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(239)", terms := [(239, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(240)", terms := [(240, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(241)", terms := [(241, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(242)", terms := [(242, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(243)", terms := [(243, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(244)", terms := [(244, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(245)", terms := [(245, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(246)", terms := [(246, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(247)", terms := [(247, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(248)", terms := [(248, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(249)", terms := [(249, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(250)", terms := [(250, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(251)", terms := [(251, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(252)", terms := [(252, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(253)", terms := [(253, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(254)", terms := [(254, 1)], rhs := 0, weight := 48 },
  { label := "upper_bound(255)", terms := [(255, 1)], rhs := 0, weight := 48 }
]








def q128_v13Rules : List Rule := [
  .outside 2,
  .outside 8,
  .outside 21,
  .single 22,
  .single 24,
  .outside 30,
  .outside 31,
  .outside 33,
  .outside 34,
  .outside 36,
  .outside 37,
  .outside 38,
  .outside 39,
  .outside 40,
  .outside 42,
  .source 43 false,
  .source 44 false,
  .source 45 true,
  .source 46 false,
  .source 47 false,
  .source 48 false,
  .source 49 false,
  .source 50 false,
  .source 52 false,
  .source 53 false,
  .source 54 false,
  .source 55 false,
  .source 56 false,
  .single 57,
  .single 58,
  .single 60,
  .source 65 true,
  .source 66 false,
  .source 69 true,
  .single 70,
  .source 73 true,
  .single 73,
  .source 74 true,
  .source 75 true,
  .source 76 true,
  .source 77 true,
  .source 78 true,
  .source 79 true,
  .source 80 true,
  .source 81 true,
  .source 83 true,
  .source 84 true,
  .source 85 true,
  .outside 86,
  .outside 87,
  .single 87,
  .outside 88,
  .outside 89,
  .single 90,
  .outside 91,
  .outside 93,
  .single 94,
  .outside 97,
  .single 97,
  .single 101,
  .single 103,
  .single 108,
  .outside 115,
  .outside 117,
  .outside 118,
  .outside 119,
  .outside 121,
  .outside 124,
  .outside 127,
  .paired 5,
  .paired 23,
  .paired 24,
  .paired 25,
  .paired 26,
  .paired 27,
  .paired 28,
  .paired 29,
  .paired 31,
  .paired 32,
  .paired 39,
  .paired 41,
  .paired 43,
  .paired 44,
  .paired 45,
  .paired 46,
  .paired 47,
  .paired 48,
  .paired 49,
  .paired 61,
  .paired 63,
  .largeLink,
  .upper 43,
  .upper 57,
  .upper 63,
  .upper 67,
  .upper 69,
  .upper 70,
  .upper 73,
  .upper 76,
  .upper 79,
  .upper 85,
  .upper 95,
  .upper 97,
  .upper 128,
  .upper 129,
  .upper 130,
  .upper 131,
  .upper 132,
  .upper 133,
  .upper 134,
  .upper 135,
  .upper 136,
  .upper 137,
  .upper 138,
  .upper 139,
  .upper 140,
  .upper 141,
  .upper 142,
  .upper 143,
  .upper 144,
  .upper 145,
  .upper 146,
  .upper 147,
  .upper 148,
  .upper 149,
  .upper 150,
  .upper 151,
  .upper 152,
  .upper 153,
  .upper 154,
  .upper 155,
  .upper 156,
  .upper 157,
  .upper 158,
  .upper 159,
  .upper 160,
  .upper 161,
  .upper 162,
  .upper 163,
  .upper 164,
  .upper 165,
  .upper 166,
  .upper 167,
  .upper 168,
  .upper 169,
  .upper 170,
  .upper 173,
  .upper 175,
  .upper 177,
  .upper 179,
  .upper 180,
  .upper 181,
  .upper 182,
  .upper 183,
  .upper 184,
  .upper 185,
  .upper 186,
  .upper 187,
  .upper 188,
  .upper 189,
  .upper 190,
  .upper 191,
  .upper 192,
  .upper 193,
  .upper 195,
  .upper 196,
  .upper 197,
  .upper 198,
  .upper 199,
  .upper 200,
  .upper 202,
  .upper 204,
  .upper 206,
  .upper 207,
  .upper 208,
  .upper 209,
  .upper 210,
  .upper 213,
  .upper 214,
  .upper 215,
  .upper 216,
  .upper 217,
  .upper 218,
  .upper 219,
  .upper 220,
  .upper 221,
  .upper 222,
  .upper 223,
  .upper 224,
  .upper 225,
  .upper 226,
  .upper 227,
  .upper 228,
  .upper 229,
  .upper 230,
  .upper 231,
  .upper 232,
  .upper 233,
  .upper 234,
  .upper 235,
  .upper 236,
  .upper 237,
  .upper 238,
  .upper 239,
  .upper 240,
  .upper 241,
  .upper 242,
  .upper 243,
  .upper 244,
  .upper 245,
  .upper 246,
  .upper 247,
  .upper 248,
  .upper 249,
  .upper 250,
  .upper 251,
  .upper 252,
  .upper 253,
  .upper 254,
  .upper 255
]







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

 def scaleIntHom (p k : ℕ) : ℤ →+ Ambient p k where
  toFun x := (2 : Ambient p k) ^ p * (x : Ambient p k)
  map_zero' := by simp
  map_add' x y := by simp [mul_add]

/-- The actual embedding onto the subgroup generated by2^p. -/
def powerEmbed (p k : ℕ) : ZMod (2 ^ (k + 1)) →+ Ambient p k :=
  ZMod.lift (2 ^ (k + 1)) ⟨scaleIntHom p k, by
    dsimp [scaleIntHom]
    push_cast
    rw [← pow_add, ← Nat.add_assoc]
    simpa only [Nat.cast_pow, Nat.cast_ofNat] using ZMod.natCast_self (2 ^ ((p + k) + 1))⟩

























def innerSet (p k : ℕ) (A : Finset (Ambient p k)) : Finset (ZMod (2 ^ (k + 1))) :=
  homPreimage (powerEmbed p k) A























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

abbrev quotientOrder (p : ℕ) : ℕ := 2^(p+1)
theorem quotientOrder_pos (p : ℕ) : 0 < quotientOrder p := by positivity

def actualVector (p k : ℕ) (A : Finset (Ambient p k)) (z : Ambient p k)
    (j : Fin (2*quotientOrder p)) : ℝ :=
  if j.val < quotientOrder p then (fibreMass p k A (j.val : Quotient p) : ℝ)
  else (linkMass p k A z (j.val-quotientOrder p : Quotient p) : ℝ)

def actualContainer (p : ℕ) (C : Finset ℕ) : Finset (Quotient p) :=
  C.image (fun j : ℕ => (j : Quotient p))

def quotientEquiv (p : ℕ) : Fin (quotientOrder p) ≃ Quotient p where
  toFun := fun i => (i.val : Quotient p)
  invFun := fun i => ⟨i.val, ZMod.val_lt i⟩
  left_inv := by
    intro i
    apply Fin.ext
    change (i.val : Quotient p).val = i.val
    exact ZMod.val_natCast_of_lt i.isLt
  right_inv := by
    intro i
    exact ZMod.natCast_zmod_val i





















-- 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

def middleInterval (q c : ℕ) : Finset (ZMod q) :=
  (Finset.Ico c (2 * c)).image (fun j : ℕ => (j : ZMod q))













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

/-- Exact capacity of an ordinary step-v path interval. -/
def g (v L : ℕ) : ℕ :=
  v * (L / (2 * v)) + min (L % (2 * v)) v

/-- The three-interval expression after deleting near-empty fibres.
For positive v, (v+1)/2 is ceil(v/2). -/
def packing (q v : ℕ) : ℕ :=
  let k := (q + 1) / 3
  k - v + g v (k / 3) + g v (k - (v + 1) / 2) + g v ((k + 2 * v) / 3)



































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

/-- The real piecewise-linear path-capacity envelope. -/
noncomputable def GReal (s : ℝ) : ℝ :=
  (⌊s / 2⌋ : ℤ) + min (s - 2 * (⌊s / 2⌋ : ℤ)) 1

noncomputable def FReal (t : ℝ) : ℝ :=
  t - 1 + GReal (t / 3) + GReal (t - 1 / 2) + GReal ((t + 2) / 3)









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

def quotient (k : ℕ) : ℕ := 3 * k - 1
def enlargedU (k v : ℕ) : Finset ℕ := Finset.Ico k (2 * k + v)
def lowF (k v : ℕ) : Finset ℕ :=
  Finset.Ico ((k + 1) / 2) ((2 * k + v - 1) / 3 + 1)
def highF (k v : ℕ) : Finset ℕ :=
  Finset.Ico (7 * k / 3) ((5 * k + v - 2) / 2 + 1)
def nearEmptyF (k v : ℕ) : Finset ℕ :=
  (Finset.range (quotient k)).filter fun x =>
    2 * x % quotient k ∈ enlargedU k v ∧ 3 * x % quotient k ∈ enlargedU k v




























def liftedRange (k v : ℕ) : Finset ℕ :=
  Finset.Ico (2 * k) (quotient k + k + v)
def liftedLowF (k v : ℕ) : Finset ℕ :=
  Finset.Ico (quotient k + (k + 1) / 2)
    (quotient k + (2 * k + v - 1) / 3 + 1)
def firstBlock (k : ℕ) : Finset ℕ := Finset.Ico (2 * k) (7 * k / 3)
def middleBlock (k v : ℕ) : Finset ℕ :=
  Finset.Ico ((5 * k + v - 2) / 2 + 1) (quotient k + (k + 1) / 2)
def lastBlock (k v : ℕ) : Finset ℕ :=
  Finset.Ico (quotient k + (2 * k + v - 1) / 3 + 1) (quotient k + k + v)















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]

/-- Choose the direct link source when possible, otherwise the predecessor source. -/
def source (C : Finset G) (v y : G) : G := if y ∈ C then y else y - v

def enlarged (C : Finset G) (v : G) : Finset G := C ∪ C.image (fun j => j + v)















end LongWagnerRelaxedSourceMass
end LongWagnerStandaloneBody42

/- Source: LongWagnerFibreSourceMass; SHA256 4c4bef63468708f40faed369ade0cf7bdcff68c0ab82ee64d4ccfe41eb986994. -/
section LongWagnerStandaloneBody43
open scoped BigOperators Pointwise

namespace LongWagnerFibreSourceMass

open Z2nFiveEighths LongWagnerTools LongWagnerHighOdd
open LongWagnerFibreBounds LongWagnerFibreAnalytic LongWagnerRelaxedSourceMass



/-- The quotient's ordinary parity reduction. -/
def parityHom (p : ℕ) : Quotient p →+ ZMod 2 :=
  (ZMod.castHom (Nat.pow_dvd_pow 2 (by omega : 1 ≤ p + 1)) (ZMod 2)).toAddMonoidHom

















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

/-- The normalized critical interval, cast into the actual dyadic quotient. -/
def middleContainer (p c : ℕ) : Finset (Quotient p) :=
  actualContainer p (Finset.Ico c (2*c))

/-- The actual quotient residues whose doubled and tripled targets are critical. -/
def sparseFibres (p c : ℕ) : Finset (Quotient p) :=
  actualContainer p (nearEmptyF c 0)




































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

def template : Finset (Quotient 2) := {3, 4, 5}













end LongWagnerQ8Zero
end LongWagnerStandaloneBody46

/- Source: LongWagnerQ2Container; SHA256 341a4c3d632db185d38f4fa8e1014df9f69a5b2cb61591baf8bf23a8802241b2. -/
section LongWagnerStandaloneBody47
open Z2nFiveEighths LongWagnerTools LongWagnerFibreBounds LongWagnerFibreAnalytic
open LongWagnerFibreInnerHighOdd

namespace LongWagnerQ2Container

def template : Finset (Quotient 0) := {1}





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

def q8C : Finset ℕ := {3,4,5}
abbrev q8Container : Finset (Quotient 2) := actualContainer 2 q8C

















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


/-- Exact certificate for q32_v3: normalized bound 53/3; all analytic rows follow. -/
def q32_v3Rows : Array FibreRow := #[
  { label := "['outside_link', 0]", terms := [(0, 1), (3, 1)], rhs := 1, weight := 3 },
  { label := "['outside_link', 3]", terms := [(3, 1), (6, 1)], rhs := 1, weight := 3 },
  { label := "['outside_link', 8]", terms := [(8, 1), (11, 1)], rhs := 1, weight := 6 },
  { label := "['outside_link', 9]", terms := [(9, 1), (12, 1)], rhs := 1, weight := 6 },
  { label := "['outside_link', 10]", terms := [(10, 1), (13, 1)], rhs := 1, weight := 6 },
  { label := "['link_source', 11, 11]", terms := [(11, -1), (43, 1)], rhs := 0, weight := 9 },
  { label := "['link_source', 12, 12]", terms := [(12, -1), (44, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 13, 13]", terms := [(13, -1), (45, 1)], rhs := 0, weight := 3 },
  { label := "['link_source', 14, 14]", terms := [(14, -1), (46, 1)], rhs := 0, weight := 6 },
  { label := "['link_source', 15, 18]", terms := [(18, -1), (47, 1)], rhs := 0, weight := 3 },
  { label := "['link_source', 17, 17]", terms := [(17, -1), (49, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 19, 22]", terms := [(22, -1), (51, 1)], rhs := 0, weight := 12 },
  { label := "['link_source', 20, 23]", terms := [(23, -1), (52, 1)], rhs := 0, weight := 6 },
  { label := "['link_source', 21, 24]", terms := [(24, -1), (53, 1)], rhs := 0, weight := 6 },
  { label := "['outside_link', 22]", terms := [(22, 1), (25, 1)], rhs := 1, weight := 3 },
  { label := "['outside_link', 23]", terms := [(23, 1), (26, 1)], rhs := 1, weight := 6 },
  { label := "['single_diagonal', 25]", terms := [(11, 1), (18, 2), (25, 1)], rhs := 3, weight := 3 },
  { label := "['outside_link', 29]", terms := [(0, 1), (29, 1)], rhs := 1, weight := 3 },
  { label := "['outside_link', 31]", terms := [(2, 1), (31, 1)], rhs := 1, weight := 3 },
  { label := "['paired_diagonal', 6]", terms := [(2, 1), (6, 1), (12, 2), (18, 1), (22, 1)], rhs := 4, weight := 3 },
  { label := "['paired_diagonal', 7]", terms := [(5, 1), (7, 1), (14, 2), (21, 1), (23, 1)], rhs := 4, weight := 6 },
  { label := "['paired_diagonal', 11]", terms := [(1, 1), (11, 1), (17, 1), (22, 2), (27, 1)], rhs := 4, weight := 6 },
  { label := "['paired_diagonal', 12]", terms := [(4, 1), (12, 1), (20, 1), (24, 2), (28, 1)], rhs := 4, weight := 6 },
  { label := "['paired_diagonal', 15]", terms := [(13, 1), (15, 1), (29, 1), (30, 2), (31, 1)], rhs := 4, weight := 3 },
  { label := "['large_link']", terms := [(32, -3), (33, -3), (34, -3), (35, -3), (36, -3), (37, -3), (38, -3), (39, -3), (40, -3), (41, -3), (42, -3), (43, -3), (44, -3), (45, -3), (46, -3), (47, -3), (48, -3), (49, -3), (50, -3), (51, -3), (52, -3), (53, -3), (54, -3), (55, -3), (56, -3), (57, -3), (58, -3), (59, -3), (60, -3), (61, -3), (62, -3), (63, -3)], rhs := -32, weight := 4 },
  { label := "upper_bound(15)", terms := [(15, 1)], rhs := 1, weight := 3 },
  { label := "upper_bound(16)", terms := [(16, 1)], rhs := 1, weight := 6 },
  { label := "upper_bound(17)", terms := [(17, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(19)", terms := [(19, 1)], rhs := 1, weight := 6 },
  { label := "upper_bound(32)", terms := [(32, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(33)", terms := [(33, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(34)", terms := [(34, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(35)", terms := [(35, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(36)", terms := [(36, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(37)", terms := [(37, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(38)", terms := [(38, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(39)", terms := [(39, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(40)", terms := [(40, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(41)", terms := [(41, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(42)", terms := [(42, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(43)", terms := [(43, 1)], rhs := 1, weight := 3 },
  { label := "upper_bound(45)", terms := [(45, 1)], rhs := 1, weight := 9 },
  { label := "upper_bound(46)", terms := [(46, 1)], rhs := 1, weight := 6 },
  { label := "upper_bound(47)", terms := [(47, 1)], rhs := 1, weight := 9 },
  { label := "upper_bound(48)", terms := [(48, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(50)", terms := [(50, 1)], rhs := 1, weight := 12 },
  { label := "upper_bound(52)", terms := [(52, 1)], rhs := 1, weight := 6 },
  { label := "upper_bound(53)", terms := [(53, 1)], rhs := 1, weight := 6 },
  { label := "upper_bound(54)", terms := [(54, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(55)", terms := [(55, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(56)", terms := [(56, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(57)", terms := [(57, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(58)", terms := [(58, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(59)", terms := [(59, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(60)", terms := [(60, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(61)", terms := [(61, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(62)", terms := [(62, 1)], rhs := 0, weight := 12 },
  { label := "upper_bound(63)", terms := [(63, 1)], rhs := 0, weight := 12 }
]








def q32_v3Rules : List Rule := [
  .outside 0,
  .outside 3,
  .outside 8,
  .outside 9,
  .outside 10,
  .source 11 false,
  .source 12 false,
  .source 13 false,
  .source 14 false,
  .source 15 true,
  .source 17 false,
  .source 19 true,
  .source 20 true,
  .source 21 true,
  .outside 22,
  .outside 23,
  .single 25,
  .outside 29,
  .outside 31,
  .paired 6,
  .paired 7,
  .paired 11,
  .paired 12,
  .paired 15,
  .largeLink,
  .upper 15,
  .upper 16,
  .upper 17,
  .upper 19,
  .upper 32,
  .upper 33,
  .upper 34,
  .upper 35,
  .upper 36,
  .upper 37,
  .upper 38,
  .upper 39,
  .upper 40,
  .upper 41,
  .upper 42,
  .upper 43,
  .upper 45,
  .upper 46,
  .upper 47,
  .upper 48,
  .upper 50,
  .upper 52,
  .upper 53,
  .upper 54,
  .upper 55,
  .upper 56,
  .upper 57,
  .upper 58,
  .upper 59,
  .upper 60,
  .upper 61,
  .upper 62,
  .upper 63
]







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

def progression512 : Finset ℕ := Finset.Ico 171 342














/-- The exact geometric packing decomposition and source-map facts supplied
by the separate quotient-interval/actual-packing adapter. -/
structure ActualPackingData (p k v : ℕ) (A : Finset (Ambient p k)) (z : Ambient p k)
    (C F : Finset (Quotient p)) : Prop where
  double_injective : Set.InjOn (fun i => i+i) (F : Set (Quotient p))
  double_image : ∀ i ∈ F, i+i ∈ enlarged C (quotientHom p k z)
  triple_image : ∀ i ∈ F, i+i+i ∈ enlarged C (quotientHom p k z)
  packing : (A.card : ℝ) ≤ ((2^k : ℕ) : ℝ)*(LongWagnerPacking.packing (quotientOrder p) v : ℝ)+
    ∑ i ∈ F, (fibreMass p k A i : ℝ)













end LongWagnerSmallQuotientDispatch
end LongWagnerStandaloneBody51

/- Source: LongWagnerSourcePacking; SHA256 efc3b97d9d3a698a054c2b6d37b36e1588d3dca92a91e8e3854b38b830f761d7. -/
section LongWagnerStandaloneBody52
open scoped BigOperators

set_option autoImplicit false
set_option maxHeartbeats 0

namespace LongWagnerQuotientIntervals

def isolated (k v : ℕ) : Finset ℕ := Finset.Ico (k + v) (2 * k)
def baseC (k : ℕ) : Finset ℕ := Finset.Ico k (2 * k)



















end LongWagnerQuotientIntervals
end LongWagnerStandaloneBody52

/- Source: LongWagnerQuotientIntervalZMod; SHA256 fa347496764b4db7ff19f37cea226ca5fc5442299e9447d1d298c6c0d54b201c. -/
section LongWagnerStandaloneBody53
set_option autoImplicit false
set_option maxHeartbeats 0

namespace LongWagnerQuotientIntervals

def zNearEmpty (k v : ℕ) : Finset (ZMod (quotient k)) :=
  (nearEmptyF k v).image (fun x : ℕ => (x : ZMod (quotient k)))

def zEnlargedU (k v : ℕ) : Finset (ZMod (quotient k)) :=
  (enlargedU k v).image (fun x : ℕ => (x : ZMod (quotient k)))























end LongWagnerQuotientIntervals
end LongWagnerStandaloneBody53

/- Source: LongWagnerQuotientIntervalAdapters; SHA256 04fe5778b22f6add2e44d637a846e362911b71dad4487f58ef8aabbf148934aa. -/
section LongWagnerStandaloneBody54
open scoped BigOperators

set_option autoImplicit false
set_option maxHeartbeats 0

namespace LongWagnerQuotientIntervals

/-- Free target modulus avoids dependent transport in actual dyadic fibres. -/
def zNearEmptyAt (q k v : ℕ) : Finset (ZMod q) :=
  (nearEmptyF k v).image (fun x : ℕ => (x : ZMod q))
def zEnlargedAt (q k v : ℕ) : Finset (ZMod q) :=
  (enlargedU k v).image (fun x : ℕ => (x : ZMod q))
def zBaseCAt (q k : ℕ) : Finset (ZMod q) :=
  (Finset.Ico k (2 * k)).image (fun x : ℕ => (x : ZMod q))

















def natQuotientEquiv (q : ℕ) [NeZero q] : Fin q ≃ ZMod q where
  toFun := fun i => (i.val : ZMod q)
  invFun := fun i => ⟨i.val, ZMod.val_lt i⟩
  left_inv := by
    intro i
    apply Fin.ext
    exact ZMod.val_natCast_of_lt i.isLt
  right_inv := fun i => ZMod.natCast_zmod_val i



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



/-- The normalized middle-third container in an arbitrary quotient modulus. -/
def middleContainer (q K : ℕ) : Finset (ZMod q) :=
  (Finset.Ico K (2 * K)).image (fun x : ℕ => (x : ZMod q))



























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





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. -/