The R4b count clauses (keep-shaped HYPOTHESES, not axioms) #
The R4b count, candidate source — THE zero-edge interim keep
(manuscript prop:zeroedge l.4314–4369, eq:recursionR4b l.4342–4353
with the candidate functional ι_A of prop:chainmap; division-free):
2^{r+1}·Z_{Γ_A,λ}(B/C) = μ·(2^d·e_{Γ_A}(C) + G⁰·Σ_{χ∈𝒳_T} (2·n_{Γ_A,0}(Δ_{χ,κ}) − e_{Γ_A}(C)))
with μ = muT (the eq:mumultiplicity value), G⁰ = baseGaussSign ram · 2^{d/2} (the base Gauss sum of q̄_λ, gaussSum_eq_sign_two_pow-shaped),
and Δ_{χ,κ} = Delta Z χ the U8 phase classes of ONE fixed bundle Z.
s_Γ enters pre-absorbed as 2·n − e (eq:recursionR5a = the proven
sGammaZ_eq; the ι_Γ-sign is BY DEFINITION the splitting indicator).
Deliberately NOT conditioned here on anything beyond the bundle — the
hne/ZeroEdge/ram-pinning conditioning lives on the exits and on the
(future, coordinated) keep
axiom … (hne) (Z) (ram) (hram) (hpin) : ZeroEdgeCountGammaA …, which
must also carry the base-identity pinning of Z until the transgression
unit lands (U8 bundle note). Dissolution program (design §4.7): (i) P8
realization over the P6 engine (constrainedGauss_count +
prop:phaseidentity via completedSquare/addLinear at the descended
class, eq:pointwiseconstrained per lower map, then μ-multiplication
and summation); (ii) ∂-surjectivity = the H²(M) = 0 content (U6-grade
dévissage at the child); (iii) lem:affinelifting per source (candidate:
ledger dévissage at V/T; local: citable numerics at tChildKernel);
(iv) the signChar ↔ splitting-indicator identification (P8, per P6 §3's
contract, δ_κ-absorption per P6 §7.6 — Delta includes δ_κ exactly
once); (v) the sign pinnings P6.4–P6.8 discharging ram.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The R4b count, local source (manuscript prop:zeroedge mirror,
with the local functional ι_F = inv_{ℚ₂}; same fixed bundle Z as the
candidate clause — design §6.5). Same statement shape, provenance and
dissolution program as ZeroEdgeCountGammaA.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The R4b exits (eq:recursionR4b, division-free, in ℤ) #
R4b, candidate source (prop:zeroedge, division-free ℤ-spelling):
on the zero-edge branch, 2^{r+1}·Z_{Γ_A,λ}(B/C) equals the
μ·(2^d·e_C + G⁰·Σ_χ(2·n − e_C)) closed form. The branch hypotheses pin
the R4b case (design §4.7 exit signature): _hne mirrors U7's spelling
(the bundle already carries Z.hne; consumed by P8's Classical.byCases
split via Z.zeroEdge), and _hram is the P6 pinning slot tying the
ram-flag to the target-side head form (gaussType q̄_λ = ram,
discharged by P6.4–P6.8 through candidate_numZeros_eq_gaussType-grade
theorems at [Nontrivial V] — supplied by edgeHead_nontrivial). The
count clause enters as an explicit HYPOTHESIS (ZeroEdgeCountGammaA).
R4b, local source (prop:zeroedge mirror): same shape, same
bundle Z, same ram-pinning slot; the count clause enters as an
explicit HYPOTHESIS (ZeroEdgeCountGQ2).
ℕ-rearrangement guards for P8 (design §7's phaseCount_le note: #
the 2·n − e factors are bounded by ±e_C, so P8's toNat-forms can
move the negative terms across = — never Int.toNat inside a keep)
2·n_{Γ,0}(ζ) − e_Γ(C) ≤ e_Γ(C) (from the proven n ≤ e).
−e_Γ(C) ≤ 2·n_{Γ,0}(ζ) − e_Γ(C) (nonnegativity of the count).