The abstract two-way count #
The per-fibre halving clauses (keep-shaped HYPOTHESES, not axioms) #
The R4a per-fibre halving, candidate source — THE sharply-scoped
R4a residual (manuscript lem:radicaledge step 6, l.4006–4019: exact
variation formula + perfect degree-one duality; candidate half =
prop:chainmap l.1687 + prop:defduality-grade degree-one content):
over each g_C, exactly half of the weak M-lifts are λ-liftable,
stated division-free per fibre. Deliberately does NOT assert the fibre
size 2^{2·dim M} (that is the separate, PROVEN lem:elementarystage
obligation — design §6.3), and is deliberately NOT conditioned here on
¬ ZeroEdge — the conditioning belongs to its (future, coordinated)
keep sec7_edgeHalving_gammaA (hne) (hedge) : EdgeHalvingGammaA …,
whose dissolution program is recorded in the design §4.6: (i) the ledger
variation formula from U3's edgeDefect calculus + the weak-base defect
engine; (ii) edgeShadow ≠ 0 on the T-cocycle space by the
trivial-chain dévissage over the PROVEN Sec7TrivialChainData;
(iii) the free-orbit torsor bookkeeping.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The R4a per-fibre halving, local source (manuscript
lem:radicaledge step 6, l.4006–4019, with prop:localduality — NSW
VII.2, perfectness of the degree-one local pairing — the
citable-with-derivation trust class of localObstruction_scalar,
BLOCKR_P1_DESIGN §5.3). Same statement shape as the candidate clause;
its (future, coordinated) keep is
q2_edgeHalving (hne) (hedge) : EdgeHalvingGQ2 ….
Equations
- One or more equations did not get rendered due to their size.
Instances For
The R4a exits (eq:recursionR4a, division-free) #
R4a, candidate source (prop:nonzeroedge, eq:recursionR4a
l.4299–4303, division-free): on the nonzero-edge branch,
2·Z_{Γ_A,λ}(B/C) = 2^{2·dim M}·e_{Γ_A}(C'). The branch hypotheses
_hne/_hedge pin the R4a case (design §4.6's exit signature; they are
consumed by P8's Classical.byCases split and by the keeps discharging
hhalf, not by this counting proof). The halving clause enters as an
explicit HYPOTHESIS (EdgeHalvingGammaA); the fibre size is the PROVEN
candidate lem:elementarystage count (P3-U6).
R4a, local source (prop:nonzeroedge, mirror): on the
nonzero-edge branch, 2·Z_{G_{ℚ₂},λ}(B/C) = 2^{2·dim M}·e_{G_{ℚ₂}}(C').
The fibre size is the local lem:elementarystage count (P3-U5, THEOREM
from the citable q2_localduality_general); the halving clause enters
as an explicit HYPOTHESIS (EdgeHalvingGQ2).