§A The weak-base difference torsor (the liftHom_equiv_Z1 #
construction at weak bases: no surjectivity onto the quotient is imposed on the basepoint, so the fibres feed clause (d))
The weak framed-lift set at a basepoint hom: continuous framed
homs agreeing with h0 modulo the elementary kernel (the fibre of the
mod-E.N reduction through h0's coset; surjectivity NOT imposed —
lem:affinelifting's weak coordinates).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The weak-base difference torsor (liftHom_equiv_Z1 re-run at a
weak framed basepoint): weak framed lifts biject with the clause-(d)
twisted-cocycle carrier weakZ1 — the counting bridge to
q2_localduality_weakZ1_card (N5) and the N6 corank engine.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Card transport of the torsor.
§B Carriers at the child: one-spelling bridges (banked #
mixed-defeq-carrier fix-class — every downstream statement consumes THESE spellings)
The λ-liftable W2a total space, abbreviated (the Zcount carrier,
RadicalEdgeCount.lean:160).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The base of the W2a fibration, ASCRIBED at the cChild-spelling
(the one-spelling bridge: coverLiftBase produces the
(mChildKernel).N-spelled child type, defeq to (cChild chief K).1/.2;
this abbrev pins the cChild spelling every ρ-sum below uses).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The framed M-lift fibre over a lower map (all framed lifts, weak
in the ambient target — liftHom at the child M-kernel, ρ taken in
the cChild spelling).
Equations
- One or more equations did not get rendered due to their size.
Instances For
An M-lift, repackaged as a W2a total-space point (the
coverLiftFibreEquiv.invFun packaging; .val is UNCHANGED — rfl).
Equations
- Q2Presentation.Induction.mTotal chief K B ρ l = ⟨↑l, ⋯⟩
Instances For
λ-liftability read on the M-lift carrier (the coverLiftableWeak
predicate of the total point; reads only l.val).
Equations
- Q2Presentation.Induction.liftableML chief K lam hinv B ρ l = Q2Presentation.Induction.coverLiftableWeak chief K lam hinv B (Q2Presentation.Induction.mTotal chief K B ρ l)
Instances For
coverLiftableWeak is .val-determined (Prop-subtype
extensionality; the transport across repackagings).
The mod-T' reduction of an M-lift: the induced V⋊C-lift of ρ
(composition with the tChild-projection; the T′-stage map of
lem:affinelifting).
Equations
- One or more equations did not get rendered due to their size.
Instances For
§C The |W_ρ| = 2^{2·dimV} numerics: `edgeZ1 ≃ btLiftHom ≃ #
weakZ1(vLayerKernel) at the pinned-section basepoint, closed per source by N5/N6 (weakZ1_vLayer_card, weakZ1_vLayer_card_gammaA`)
Two elements of B/T' agree modulo the V-layer iff their
btProj-images agree (ker btProj = vLayer in coset form).
The pinned-section basepoint hom γ ↦ s(ρ̄γ) (the trivialization of
z = 0, as a framed continuous hom into B/T').
Equations
- One or more equations did not get rendered due to their size.
Instances For
The basepoint is framed.
The basepoint, packaged as a V-stage total-space point (the
carrier N5/N6's weakZ1_vLayer_card* counts read).
Equations
- Q2Presentation.Induction.sBaseTotal chief K lam hinv B ρ Z P = ⟨Q2Presentation.Induction.sBaseHom chief K lam hinv B ρ Z P, ⋯⟩
Instances For
V⋊C-lifts of ρ are exactly the weak framed lifts at the pinned
basepoint (the projection clause read modulo the V-layer).
Equations
- Q2Presentation.Induction.btLiftHom_equiv_weakLift chief K lam hinv B ρ Z P = Equiv.subtypeEquivRight ⋯
Instances For
|Z¹_ρ(V)| = |weakZ1(vLayer)| — the carrier chain
edgeZ1 ≃ btLiftHom ≃ weakLift ≃ weakZ1 at the pinned basepoint.
The per-source |W_ρ|-numerics (N5/N6 closed). Stated at the #
CONCRETE packages boundaryPackage_GammaA/boundaryPackage_GQ2 — the
N5 cards ride clause (d) of the GQ2-pinned q2_localduality_general
and the N6 cards ride the GammaA ledger, so neither is
package-generic; the §C constructions above ARE generic and are simply
instantiated here.
|W_ρ| = 2^{2·dimV}, candidate source (N6's
weakZ1_vLayer_card_gammaA at the pinned basepoint).
|W_ρ| = 2^{2·dimV}, local source (N5's weakZ1_vLayer_card
at the pinned basepoint).
The per-source T'-fibre numerics (N5/N6 closed; concrete #
packages for the same reason as the |W_ρ|-cards)
|weakLift(T')| = 2^{2·dimT+rT} at every candidate M-lift
(N6's weakZ1_tChild_card_gammaA through the difference torsor).
|weakLift(T')| = 2^{2·dimT+rT} at every local M-lift (N5's
weakZ1_tChild_card through the difference torsor).
§D The honest floors (named Props, consumed as HYPOTHESES — #
never axioms; the N7 EdgeDelSurj discipline)
The T'-fibre condition of a framed M-lift over the z-twisted
V⋊C-lift: l mod T' = γ ↦ vInG(zγ)·s(ρ̄γ) pointwise (the graph of
the trivialized coordinate; modT l = edgeTrivial … z in value form).
Equations
- One or more equations did not get rendered due to their size.
Instances For
F-affine floor Prop (design §4-N9's honest residue of S2/S3;
lem:affinelifting l.4048–4083, eq:affineequation l.4060 +
lem:elementarystage l.4171–4205): a twisted cocycle z ∈ Z¹_ρ(V)
supports a framed M-lift over ρ through the pinned trivialization
IFF its per-χ constraint readings (edgeLRead, the Γ_{γ_χ}-graph
ι-values) hit the χ_*e-targets (edgeKappaRead) — the affine
equation ∂z = ρ*e in per-cocycle, token-FREE spelling. PROVENANCE +
dissolution: (⟸, existence) is the H²_{Γ,ρ}(M_χ-complement) = 0
counting dévissage — in-tree route: clause (d) of
q2_localduality_general at ker χ̃-kernels (local) resp. the N6
corank engine (candidate), the SAME ladder as EdgeDelSurj's
dissolution (the concurrent ∂-glue lane); (⟹, admissibility) is the
tau_eT-deck calculus of the pinning (eq:basekappacochain l.2131 read
along the lift; dischargeable from P.tau/P.tau_eT +
edgeLRead_eq_chiDefect, budgeted as the first dissolution rung).
Falsifiable per (ρ, z): both sides are decidable-in-principle finite
statements at a concrete bundle. Strictly below keeps 3/4 (it carries
no count, no sign, no Gauss content).
Equations
- One or more equations did not get rendered due to their size.
Instances For
F-sgn-C1 floor Prop, VALUE spelling (design §5, candidate
Gauss-type constancy; prop:candidatezero l.2731 = lem:wall +
lem:unitaryline + lem:ramifiedhermitian, P6-OWNED — consumed, not
created, by this lane): the descended base-problem Gauss sum takes the
single value baseGaussSign s · 2^{dimV/2} at EVERY candidate lower
map. The value spelling absorbs the nonsingularity/positivity of the
descended form (the "radical ⊆ B¹" converse of the N7 landing note) —
each is implied by keep 5 + P6.4–P6.8 and each is falsifiable here as a
single ℤ-equation per ρ. Bound to the CONCRETE package
boundaryPackage_GammaA (the over-strength guard: never quantify a
floor over arbitrary packages). F1/audit-§A guard: NO
gaussType (edgeHeadForm …)-tie is stated or implied.
Equations
- One or more equations did not get rendered due to their size.
Instances For
F-sgn-L1 floor Prop, VALUE spelling (design §5, local
Gauss-type constancy; prop:localzero l.3349 weak half — strictly below
keep 5, dissolved BY keep 5 at P8-S2). Audit-§A guard: the nearest
literature form (Poonen–Rains JAMS 2012 Prop 4.11) has the OPPOSITE
sign and is NEVER cited for this value. Bound to the CONCRETE package
boundaryPackage_GQ2 (over-strength guard).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The one-common-sign package (S6 + F-sgn-X1: "the common Gauss
sum is supplied by prop:candidatezero, prop:localzero — one sign",
joint sentence l.3358–3360): ONE bit serves both sources' value floors.
The keeps-file residue sec7_zeroEdge_sign_agree : zeroEdgeSign … Z = s_cand mentions zeroEdgeSign and therefore belongs to the
coordinator's swap in BlockRecursionKeeps.lean; THIS Prop is its
keeps-free content.
Equations
- One or more equations did not get rendered due to their size.
Instances For
§E The T′-stage absorption (the f-level Zcount fibre #
absorption recorded as N9 scope by the N7 landing note)
Value readout of the pinned trivialization (rfl through
Equiv.ofBijective and edgeTrivial_apply).
The trivialized-coordinate fibre condition, as an equality of
V⋊C-lifts: modT l = trivialization(z) iff the pointwise T'-fibre
condition FibHom holds.
Stage-1 transport at a fibre point: an M-lift over the z-twisted
V⋊C-lift is λ-liftable iff z is desc-liftable (N1's
coverLiftableWeak_iff_descLiftableWeak + the fibre-condition
rewiring).
The per-coordinate fibre dichotomy: over a twisted cocycle z,
the λ-liftable M-lift fibre count is 2^{2·dimT+rT} when z is
constrained (L z = κ₀, via the affine floor) and desc-liftable, and
0 otherwise.
The T′-stage absorption (design §4-N9 / N7-landing-note scope):
per lower map, the λ-liftable framed M-lift count equals
2^{2·dimT+rT} times N7's constrained desc-liftable cocycle count.
The torsor and stage-1 descent are theorems; the image characterization
enters through the EdgeAffineLifting floor; the T′-numeric enters
through the per-source hT-slot (card_weakLift_tChild_gammaA/gq2).
§F The Zcount partition over the lower maps #
(coverLiftTotal_equiv_sigma_liftHom restricted to the liftable
subtype, through coverLiftFibreEquiv)
The per-ρ fibre of the liftable total space is the liftable
M-lift set (coverLiftFibreEquiv conjugated through the subtype
reassociations).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Zcount partition over the lower maps.
§G The per-χ regroup: Σ_ρ ι±(ρ*Δ_χ) = 2·n_{Γ,0}(Δ_χ) − e_Γ(C) #
(N2's reading lemmas + the proven sGammaZ_eq)
The ±1-indicator of the pulled phase class, in sGammaZ's
summand form (N2's iotaSign_pullCochain_eq_one_iff both ways).
The per-χ regroup (eq:recursionR5a consumed): the ρ-sum of
the ±1-indicators is 2·phaseCount − eC.
§H The generic assembly (source-generic over the token and the #
per-source numeric/floor slots)
The R4b realization, generic assembly (design §4-N9): the
ZeroEdgeCount*-shaped ℤ-identity at a free sign s, from N7's
pointwise engine summed over the lower maps. Slots: hdel (the F-∂
floor, per ρ), haff (the affine floor, per ρ), hW/hT (the
per-source |Z¹(V)|/|Z¹(T')| numerics — theorems at both sources,
§C), hg (the F-sgn value floor at s).
§I The tie-break instrument and the per-source sign-parametric #
exits
The both-signs tie-break (design §3.1(ii)/§4-N9: "both signs ⟹
the phase-sum term vanishes ⟹ every consumer identity is
sign-insensitive"): if the R4b identity holds at BOTH signs then it
holds at every sign — the instrument the keeps-file swap uses to resolve
zeroEdgeSign's definite description against the delivered sign.
The per-source exits (sign-parametric; the keeps-file swap #
connects them to zeroEdgeSign)
The R4b count, candidate source, at a delivered sign — keep 3's
count content, sign-parametric (design §4-N9 output
ZeroEdgeCount* Z s_source): all four floor slots explicit.
The R4b count, local source, at a delivered sign — keep 4's count content, sign-parametric.
Keep 3's count content in the ∃-sign form, at a merely-pinned
bundle (the mission's ∃ s-exit shape; P recovered by choice from
ZeroEdgeDescentDataPinned, so the affine floor is quantified over the
pinning).
Keep 4's count content in the ∃-sign form (the mission's
zeroEdgeCount_gq2_of_delSurj shape).
The joint one-sign package (keeps 3+4's count content at ONE
common sign, from the S6/X1 common-Gauss floor): both source counts hold
at the same s. The keeps swap resolves zeroEdgeSign Z against this
s by the §3.1(ii) case split (zeroEdgeCountGQ2_sign_free supplies
the both-signs branch).
The per-source both-signs instruments (def-Prop wrappers of #
zeroEdgeIdentity_sign_free; the keeps swap's §3.1(ii) branch)
Both signs ⟹ every sign, candidate source.
Both signs ⟹ every sign, local source.