Endpoint-preserving primitive lattice assembly #
The endpoint values in paper (5.5) are fixed. They must therefore remain
visible until Proposition 5.6 supplies the factor
⟨x₀-x₁⟩⁻⁴. This file provides the endpoint-preserving summation layer
which is deliberately absent from primitiveAcrossLatticeSum.
The first theorem below closes one complete paired-incidence fibre. Unlike
primitive_lattice_estimate, its denominator remains inside the genuine
tuple sum; no constancy of the incidence denominator across supports or
multiplicity profiles is assumed.
First and last slots of the paper's even tuple.
Equations
- Anderson4D.primitiveEndpointLeft n hn = ⟨0, ⋯⟩
Instances For
Tuples in a finite family with prescribed endpoint lattice labels.
Equations
- Anderson4D.primitiveTuplesAtEndpoints hn Y x₀ x₁ = {y ∈ Y | y (Anderson4D.primitiveEndpointLeft n hn) = x₀ ∧ y (Anderson4D.primitiveEndpointRight n hn) = x₁}
Instances For
The actual fixed-datum endpoint contribution after finite incidence reindexing. Both the primitive-pairing multiplicity and the symmetry denominator are evaluated on each tuple.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A realized tuple with the displayed endpoints has support in the two-anchor carrier used by Proposition 5.6.
Pointwise denominator estimate with the full realized-support cardinality kept on the left. The primitive-pairing cardinality may be zero; in the nonzero case one compatible pairing supplies positivity of the incidence denominator.
Every induced word in a fixed paired fibre inherits the root-cluster diameter bound from its underlying realized tuple.
Numerator of the fixed-datum endpoint contribution, before the incidence denominator.
Equations
- One or more equations did not get rendered due to their size.
Instances For
One realized support contributes at most the root-diameter factor times the complete Proposition 5.7 scale expression.
Summing one fixed datum over all endpoint-valid supports costs exactly the cardinality of the two-anchor realized-set carrier. This is the factor which Proposition 5.6 cancels against the incidence denominator.
Complete fixed-datum endpoint assembly.
This is the denominator-correct version of the one-datum lattice estimate. The actual tuple-dependent incidence denominator remains under the sum. The cardinality of the two-anchor support carrier is introduced pointwise, cancelled by Proposition 5.6, and then cancelled again after summing the same carrier.
Reindexing active paired data #
Halving the positive even leaf multiplicities of paired data gives a
positive assignment of total mass n. This is the exact 2^n carrier
for the paper's choice of (m_l).
Equations
- Anderson4D.pairedLeafHalfAssignment d = ⟨fun (l : Anderson4D.HeppLeaf t) => ⟨↑((↑d).2 l) / 2, ⋯⟩, ⋯⟩
Instances For
Paired incidence data which actually contribute to a prescribed endpoint family. The nonempty primitive-pairing fibre excludes all zero-contribution denominator data before the logarithmic reindexing.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Anderson4D.instFintypePrimitiveActiveEndpointData t M n hn Y A x₀ x₁ = Fintype.ofFinite (Anderson4D.PrimitiveActiveEndpointData t M n hn Y A x₀ x₁)
The active datum's marking restricted to the genuine logarithmic scale window.
Equations
Instances For
Active paired data inject into the product of the logarithmic marking carrier and the positive half-multiplicity carrier.
Equations
Instances For
Summing active paired data separates into a logarithmic marking sum and
at most 2^n positive half-multiplicity assignments.
Summing the paired-incidence carrier #
The endpoint contribution attached to every paired realization datum. The tuple family is restricted to the actual incidence fiber before the fixed-datum estimate is applied.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A datum outside the active endpoint subtype contributes zero. This is the precise justification for discarding the enormous ambient realization data carrier before the logarithmic marking sum.
Exact removal of the zero paired-incidence data.
Summation of the denominator-correct fixed-datum estimate over all active incidence data. This is the common branch before the extremal and non-extremal marking arguments diverge.
Non-extremal branch of the paper's (5.16)--(5.17) summation. The
strict branch-cardinality inequality leaves enough room for the unrestricted
logarithmic marking carrier.
Endpoint-preserving tree cover of the lattice sum #
The primitive (5.5) statistic after summing all compatible primitive
across pairings, while retaining the two fixed endpoint labels.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The finite endpoint-preserving version of the lattice sum (5.5).
Equations
- Anderson4D.primitiveEndpointLatticeSum M n hn A x₀ x₁ = Anderson4D.latticeChainSum M (2 * n) (Anderson4D.primitiveEndpointLatticeStatistic hn A x₀ x₁)
Instances For
A nonzero primitive endpoint statistic lies in the repeated-value locus required by the weak Hepp-tree cover.
If a valid tree realizes a word carrying an across pairing, its
restricted realization data can be promoted to the even paired carrier.
This is the arithmetic-carrier version of the fixed-slice construction in
PrimitiveAssembly.
On a valid tree, the endpoint statistic is exactly the denominator-correct paired-incidence sum over the active tuple family.
Endpoint-preserving master bridge from the finite lattice sum to valid trees and their exact even-multiplicity incidence denominators.
The bare-leaf slice #
The bare leaf contributes at most one constant endpoint tuple, and its
primitive across-pairing multiplicity is at most n!.
Non-extremal bound without requiring a multiplicity witness from the caller. If the active carrier is nonempty, any one active datum supplies the total-multiplicity witness; otherwise the incidence sum is exactly zero.