ℕ/sum support (design §3.4/§4.4) #
1 ≤ dim M (mChild_ne_bot through the child card): the R4a
exponent rewrite 2^{2·dimM}/2 = 2^{2·dimM − 1} is sound.
|𝒳_T| = 2^r (Module.natCard_eq_pow_finrank at the global
instFintypeXTEdge carrier).
XT-sum collapse (design §3.4): Σ_{χ'∈𝒳_T}(2·f(χ') − e) = 2·Σf − 2^r·e in ℤ.
The generic R4b ℕ-evaluation (design §3.4, the ℤ→ℕ bridge and THE
numeric refutation instrument of keeps 3–4): the negative product moves
across = in ℤ BEFORE any Nat.sub (never Int.toNat), and the /2^{r+1}
is exact by the identity itself.
R2's erase-sum in the children enumeration (design §4.4): the V3
isolation sum over J ≠ ⊤ equals the sum over V5's fixed properIdx
positions.
The R4a keeps (1–2) and the recovered halving theorem #
R4a flip-cocycle existence, candidate source — DISSOLVED (P8-W).
Former keep 1 (design §10-P8D, the strictly smaller residue of §5.2's
sec7_edgeHalving_gammaA), now a THEOREM: the manuscript's degree-one
duality clause (lem:radicaledge step 6, prop:chainmap +
prop:defduality-grade) is replaced by the in-tree marked-augmentation
diamond dévissage of EdgeTwistWitness.lean (design §12-P8W): at hedge
the deck generator falls inside the separating-dual window
(zeroEdge_of_separating_dual contrapositive), diamondAtW_all +
hfaithNT_of_frame produce a relator-row witness, and deck-valued
shadows yield a TwistCocycle of edgePairing exactly 1. Guards stay
load-bearing: at zero edge the flip provably cannot exist, so the
unconditional statement remains FALSE — the hypotheses are not vestigial.
The R4a per-fibre halving, candidate source — now a THEOREM in the
design §5.2 statement (same name/statement as the pre-P8-D keep shape, zero
downstream rewiring): recovered from keep 1 through the PROVEN flip
involution edgeHalvingGammaA_of_twistFlip (lem:radicaledge steps 1–6
minus the duality clause, in-tree).
KEEP 2′ — R4a local twist-reach, the S8 floor — INTERIM KEEP.
Strictly below the audit-7 keep q2_edgeHalving (per-fibre halving) and
below the §13-P8WL candidate q2_edgeTwistFlip: asserts only that every
fibre point REACHES some λ-liftable T'-twist (per-g, per-f bare ∃
— no half-count, no flip biconditional). THREE-PART provenance
(audit/CITABILITY_AUDIT_20260708.md §B/§G2): (i) variation-onto =
NSW (7.2.6) at i = 1, citable perfectness; (ii) quadraticity of the
obstruction in the twist with commutator polar form = Poonen–Rains,
MRL 18 (2011) Prop 2.9, citable; (iii) the ANCHOR clause — some
liftable twist at every point — is the manuscript residue
(lem:radicaledge l.3916–4019, local instance; S8.2 gate finding:
counting from citable clause (d) cannot rule out anchor-less points,
per-orbit liftable count is 0-or-|Im|). Everything above the floor is
PROVEN: edgeHalvingGQ2_of_twistReach (EdgeHalvingLocal.lean, the
Im-index counting over the G1 clause) recovers the halving below.
Guards hne/hedge load-bearing: at zero edge Reach forces
all-or-nothing liftability (§14-S8 guard analysis). Refutation
instrument: edgeHalvingGQ2_iff_half_card through the derived theorem.
Dissolution program: an explicit anchor from the constrained-Gauss
section (P6 engine) or a citable direction-2 variation identity (W2).
The R4a per-fibre halving, local source — now a THEOREM (S8.2:
the audit-7 keep statement, recovered from the Reach floor through the
Im-index counting of EdgeHalvingLocal.lean — clause-(d) weak-base
counts + the twist-orbit torsor structure; direction-2/W2 content never
consumed).
Keep-1/keep-2 refutation target, candidate side (design §5.2): the
halving clause in closed numeric form — half of the PROVEN fibre size
2^{2·dimM} per fibre (coverLiftFibreEquiv + mChild_liftHom_card_gammaA,
the lem:elementarystage count). A concrete per-g counterexample
refutes the recovered halving, hence keep 1.
Keep-2 refutation target, local mirror (mChild_liftHom_card_gq2).
The zero-edge sign, the R4b keeps (3–4), and the definite bundle #
The zero-edge block sign (design §3.1, architecture D: ∃-free
definite description, LOCALLY anchored): true iff the local R4b identity
holds at the plus sign for the given bundle. The formula and BOTH
zero-edge keeps use this single flag; its arithmetic value (= ram(V),
prop:localzero) is deliberately NOT computed here — that is
q2_local_base_gaussType's content (P8-S2, design §5.5). Tie-break note
(§3.1 (ii)): if both signs satisfy the local identity the phase-sum term
vanishes and every consumer identity is sign-insensitive.
Equations
- Q2Presentation.Induction.zeroEdgeSign chief K lam hinv Z = if Q2Presentation.Induction.ZeroEdgeCountGQ2 chief K lam hinv Z true then true else false
Instances For
Definitional form of zeroEdgeSign (the sGammaZ_def fix-class:
cite this, never re-haveI a decidability instance — the S9 derivations
resolve the definite description through this lemma).
The S9 floor axioms (the R4b trusted residue after the N1–N10 #
wave; design audit/BLOCKR_R4B_DESIGN.md §5 — each strictly below the
former keeps 3/4, each with recorded provenance, refutation instrument
and dissolution program)
S11 FLOOR (F-ram residual) — the base class at high-dimensional
genuinely-ramified blocks — INTERIM KEEP. BaseModelExists
(TransgressionUnit.lean:321) under the residual gates 4 < dimV and
¬Odd |HeadIm| — STRICTLY BELOW the former q2_baseModel keep: the
dimV ≤ 4 stratum is discharged by the CITABLE
griess_baseModel_dim_le_four (BaseModelGriess.lean: Griess,
Pac. J. Math. 48 (1973) Thm 1 SPLIT half + Winter, Rocky Mountain
J. Math. 2 (1972), class (c)), and the odd-faithful-image stratum
is a THEOREM (baseModelExists_of_oddHeadAction; the manuscript's
ENTIRE unramified clause is in-tree via headIm_odd_of_unramified —
BaseModelHeadStructure.lean F-H5). heven certifies genuine
ramification: headTau_ne_one_of_not_odd pins this keep to ramified
blocks (headTau ≠ 1), matching lem:faithfulprojective's hypotheses
exactly. MANUSCRIPT-ONLY per audit/CITABILITY_AUDIT_20260708.md §F
- §I: the residue is
lem:faithfulprojective(l.2829, Clifford theory - Sylow-2 free weight action + projectivity descent) feeding
lem:basedetclass's ramified clause (l.2286–2360); the literature provably lacks the positive criterion — Griess: "our methods do not indicate how big these nonzero cohomology groups are"; Glasby, J. Austral. Math. Soc. Ser. A 58 (1995) 232–247 (§I, source verified) gives the explicit ±1-cocycle projective realization of the AMBIENT covers but "contains NO positive subgroup-splitting criterion" (§I verdict 3) — the Glasby anchor does NOT upgrade this keep. REFUTATION GUARDS: Griess Thm 0 manufactures nonlifting 2-local configurations atn ≥ 3— this statement binds the SPECIFIC in-tree tower and faithful image (never a free subgroup quantifier), and BOTH gates are load-bearing (droppinghdcollides with the citable Griess split half'sn ≤ 2boundary; droppinghevencollides with the F-H5 theorem). Refutation instrument: per(chief, K, lam)at4 < dimV, even|HeadIm|— theBaseModelDatam-laws are finite checks overC × V × V(design §6.2). Dissolution program: F-M2 (audit/BLOCKR_FRAM_DESIGN.md§3 —lem:faithfulprojectiveformalization: Clifford theory + the Sylow projectivity criterion + flat descent; XL, blocked on genuine mathlib gaps, DEFERRED), optionally staged through theHeadSplitPairkeep-shrink (F-M1).hneorientsedgeBaseFactorinside them_quadraticlaw; noZeroEdgeguard — the model is cover-free.
The former F-ram keep is a THEOREM (S11) — byte-identical
statement, derived by the F-G3 three-way case split
(q2_baseModel_cases, BaseModelGriess.lean): odd faithful image ⟹
baseModelExists_of_oddHeadAction (in-tree averaging); dimV ≤ 4 ⟹
the citable Griess split half (baseModelExists_of_lowDim over
griess_baseModel_dim_le_four); otherwise the strictly smaller
residual keep q2_baseModel_highdim_even above. Zero downstream
rewiring — theZeroEdgeBundle rides the theorem.
F-affine, candidate source — DISSOLVED (A-wave,
audit/BLOCKR_FAFFINE_DESIGN.md §6): a THEOREM since S11.
EdgeAffineLifting (ZeroEdgeRealization.lean §D): at every pinning
P of every bundle Z and every candidate lower map ρ, a twisted
cocycle z ∈ Z¹_ρ(V) supports a framed M-lift through the pinned
trivialization IFF its per-χ constraint readings (edgeLRead) hit
the χ_*e-targets (edgeKappaRead) — eq:affineequation
(lem:affinelifting l.4048–4083, l.4060) with the existence half
lem:elementarystage (l.4171–4205, the H²_{Γ,ρ}(M_χ) = 0
dévissage). The eq:affineequation characterization is now the A1–A7
chain (EdgeAffineDischarge.lean, edgeAffineLifting_gammaA_proven):
the token THEOREM sec7_candidate_iotaToken + the PROVEN
edgeDelSurj_gammaA + the N6-ledger cards — ZERO floors, no new
trust, no Gauss content. The ∀-P pinning guard (a ZeroEdgePinning
term is actual deck-reading data — the design-§8.3 over-strength
refutation) and the per-(ρ, z) refutation instrument are inherited
unchanged by the theorem.
F-affine, local source — DISSOLVED (A-wave,
audit/BLOCKR_FAFFINE_DESIGN.md §6): a THEOREM since S11. The
G_{ℚ₂}-mirror of q2_edgeAffineLifting_gammaA (same
eq:affineequation/lem:elementarystage provenance, same ∀-P
pinning guard, same per-(ρ, z) refutation instrument), derived by
the A1–A7 chain (EdgeAffineDischarge.lean,
edgeAffineLifting_gq2_proven): the citable local token
q2_trivialCoeff_h2_line (existing citable axiom — no new trust) +
the PROVEN edgeDelSurj_gq2 + the clause-(d)-backed cards
(mChild_liftHom_card_gq2, card_edgeZ1_gq2,
card_weakLift_tChild_gq2). ZERO floors — the predicted "(⟸) clause
(d) at the ker χ̃-kernels" dissolution landed exactly as recorded.
S10 FLOOR (F-sgn: C1 + L1 + X1) — the one-common-sign Gauss value
line at a canonical-gauge WITNESS bundle — INTERIM KEEP (W1 form).
ZeroEdgeCommonGauss (ZeroEdgeRealization.lean §D): ONE s : Bool
with G(Q̄_ρ) = baseGaussSign s · 2^{dimV/2} at every lower map of
BOTH sources — asserted for SOME pinned bundle of the zero-edge cover
(the manuscript's canonical-κ_q⁰ gauge), NEVER for every pinned
bundle. W1 WEAKENING (consistency repair, 2026-07-09,
audit/BLOCKR_FSGN_DESIGN.md §3.3-RESOLUTION): the S9 ∀-pinned-Z
form was UNSOUND-SHAPED — conj_read pins only the sum
mC c v + γ_κ c (c·v) (TransgressionUnit.lean:547), so the pinned
bundles of one cover form a torsor under the coherence-cocycle gauge
with effective group H¹(C,V); a shift by the class dual to
A ∈ Z¹(C,V) moves the descended form by a linear functional with
polar representative [ρ*A] and flips the per-ρ Gauss sign by the
pulled-back phase read ι_Γ(ρ*Θ_A) (completed square) — a per-ρ bit
with NO uniformity mechanism, so at a shifted bundle no single s
serves all ρ; conditional refutation recipe at §3.3-RESOLUTION R.3.
STRICTLY WEAKER: the S9 axiom + N10's zeroEdgePinnedExistence
implies this statement; the converse fails off the witness gauge.
MANUSCRIPT-IMPLIED: the canonical bundle exists (N10's construction
pattern with the canonical model in the mC-slot) and
prop:candidatezero + prop:localzero + the joint sentence
l.3358–3360 give its one-sign line. THREE-PART provenance UNCHANGED
(design §5 rows F-sgn-C1/L1/X1): (C1) prop:candidatezero l.2731 =
lem:wall + lem:unitaryline + lem:ramifiedhermitian, P6-OWNED
(P6.4–P6.8); (L1) prop:localzero l.3349 weak half; (X1) the ONE-BIT
agreement, joint sentence l.3358–3360 — all stated by the manuscript
AT the canonical base model of lem:basedetclass, exactly the witness
this form carries. The value spelling also absorbs the descended-form
nonsingularity (the "radical ⊆ B¹" converse, per-source
duality-grade). CITABILITY GUARD (audit CITABILITY_AUDIT_20260708.md
§A): the nearest literature form — Poonen–Rains, J. AMS 25 (2012),
Prop 4.11 — computes the OPPOSITE sign for its self-cup pairing; NEVER
cite that cluster for this value. F1 GUARD: NEVER a
gaussType (edgeHeadForm …) = ram tie — refuted in general
(eq:ramifiedarfq vs eq:relativeArf); the Gauss type stays opaque
inside a Bool. Refutation instrument: per (chief, K, lam) — the ∃
ranges over the pinned bundles of the given cover, each candidate
checked by one ℤ-equation per ρ (Dickson.gaussSum of a finite
form). Dissolution (W2, BLOCKR_FSGN_DESIGN.md §4 + §3.3-RESOLUTION
R.5): the P6 §1.1 canonical base-model construction builds the aligned
witness and the U-L3/U-CVAL value program pins its sign — this axiom
then becomes a THEOREM.
THE definite zero-edge bundle (design §3.1's theZeroEdgeBundle,
chosen ONCE by Classical.choose — since S10 from the W1 witness of
q2_zeroEdge_commonGauss over the q2_baseModel floor, so the definite
bundle CARRIES the common-sign value line
(theZeroEdgeBundle_commonGauss) — P7 §8.2's discipline). Both the
children list and the counting formula read THIS bundle, and both count
theorems below are derived at it, so no choice-coherence obligation
arises (design §6.2). Signature unchanged from S9 (zero downstream
rewiring).
Equations
- Q2Presentation.Induction.theZeroEdgeBundle chief K lam hinv hne hedge = ⟨⋯.choose, ⋯⟩
Instances For
The definite bundle carries the one-common-sign value line (the W1 witness clause; the S10 count derivations read their sign from here).
S10 FLOOR (the §3.1(ii) tie-break corner, AT the definite
bundle) — sign-insensitivity transfers from the local to the candidate
identity — INTERIM KEEP. If the LOCAL R4b identity holds at BOTH
signs at the definite bundle (so its phase term vanishes,
zeroEdgeIdentity_sign_free) and the CANDIDATE identity holds at
false, then the candidate identity holds at true as well — exactly
the corner where the locally-anchored definite description
zeroEdgeSign can disagree with the common-Gauss sign s = false; the
old keep 3 carried this transfer implicitly, and it stays the honest
one-implication residue (the design §4-N9 record). Provenance
UNCHANGED from S9: the prop:candidatezero + prop:localzero joint
sentence (l.3358–3360) + the §3.1(ii) tie-break note (both-signs ⟹
phase-term vanishes ⟹ sign-insensitive, transported across the sources
by the one common sign). S10 RESTATEMENT (gauge note,
audit/BLOCKR_FSGN_DESIGN.md §3.3-RESOLUTION): the former ∀-Z form
ranged over the full H¹(C,V)-gauge torsor of pinned bundles, where
the single-sign count identities are gauge-unknowable; the corner is
asserted ONLY at the definite (witness-gauge) bundle — the one place
the derivations consume it. hpin dropped: the bundle carries its
pinning. Refutation instrument: numeric per-instance — compute the
candidate phase sum Σ_χ (2·n_{Γ_A,0}(Δ_χ) − e_{Γ_A}) at the definite
bundle when the local phase sum vanishes
(zeroEdgeCount_nat_gammaA/gq2 evaluate both sides). Guards
load-bearing: the count hypotheses keep the axiom conditional — it
asserts nothing off the both-signs corner. Dissolution: the
§3.3-RESOLUTION §5 endgame — under the W2 value program either the
zeroEdgeSign re-anchoring retires this axiom as dead code (option 1)
or it survives as the recorded one-implication residue (option 2).
The candidate Gauss-value line at the definite bundle, projected
from the W1 witness (the F-sgn-C1 row individually; theorem-shaped so
the S10 census carries no redundant axiom). S10: the S9 ∀-pinned-Z
projection is retired with the ∀-Z floor (§3.3-RESOLUTION).
The local Gauss-value line at the definite bundle (the F-sgn-L1 row individually; its arithmetic sign is the W2/U-L3 value program).
Keep 3's count clause at the definite bundle — since S10 the REAL
derivation site (the shape the assembly consumes; mirror of
theZeroEdgeBundle_countQ). Derivation: the bundle-carried common
sign (theZeroEdgeBundle_commonGauss) through N9's
zeroEdgeCount_gammaA_of_floors (N7 engine + N5/N6 numerics inside)
with hdel := edgeDelSurj_gammaA (PROVEN), haff := q2_edgeAffineLifting_gammaA; the definite description resolves by
cases on its own if-condition (zeroEdgeSign_def), with the genuine
corner (local identity at both signs, common sign false) supplied by
sec7_zeroEdge_sign_agree at the bundle.
Former KEEP 3 — R4b zero-edge count, candidate source — a THEOREM
(S9; re-derived at S10) with the byte-identical statement (zero
downstream rewiring). Since S10 the ∃-witness is the definite bundle
itself (the W1 witness of q2_zeroEdge_commonGauss over the
q2_baseModel floor) and the count clause is
theZeroEdgeBundle_countA — N10's zeroEdgePinnedExistence no longer
carries the ∃-load (it remains the value-free existence instrument).
Former KEEP 4 — R4b zero-edge count, local source — now a THEOREM
AT THE DEFINITE BUNDLE (S10). The S9 ∀-bundle form is RETIRED as
gauge-unknowable (audit/BLOCKR_FSGN_DESIGN.md §3.3-RESOLUTION R.2/R.5:
over the H¹(C,V)-gauge torsor of pinned bundles the single-sign count
identity has no uniform derivation, and its truth off the canonical
gauge is not manuscript-backed); the assembly consumes ONLY the
definite-bundle shape (theZeroEdgeBundle_countQ — grep-verified: no
generic-(Z, hpin) consumer anywhere in the tree). Derivation: N9's
zeroEdgeCount_gq2_of_floors at the bundle-carried common sign
(hdel := edgeDelSurj_gq2, PROVEN; haff := q2_edgeAffineLifting_gq2;
hgauss from theZeroEdgeBundle_commonGauss), then the definite
description resolves by Classical.byCases on its own if-condition
(zeroEdgeSign_def): if the local identity holds at true the flag is
true and the case-condition itself is the count; otherwise the flag
is false and the delivered sign must be false (a true delivery
would contradict the case). The arithmetic sign value (Serre LF XIV
§2–3 + NSW VII.2–3 + lem:shapirodet) remains DEFERRED to the W2
value program inside the q2_zeroEdge_commonGauss floor.
Keep 4 at the definite bundle (statement byte-identical to S9's;
alias of the S10 q2_zeroEdgeCount).
The R4b ℕ closed form, candidate source: any bundle/sign instance
of ZeroEdgeCountGammaA evaluates Zcount through zeroEdge_toNat_eval
(XT-sum collapsed, casts folded).
The R4b ℕ closed form, local source (mirror).