Section 13.5: Representatives, component sizes, and first tops #
This file was automatically generated by Claude.
Formalization of blueprint Section 13, "Fixed modes, the linear side, and hereditary
representatives" (sec:modes), subsection 5, "Representatives, component sizes, and first tops"
(lines 2171-2235) of blueprint/formalization_blueprint.tex.
Representatives, component sizes, and first tops (blueprint lines 2171-2231) #
Blueprint lines 2176-2180: with F = π(F_late), the later predecessor labels B carrying
nine tenths of F, the earlier ones A more than half of B, and good primaries G nine tenths
of F, the three label sets share a primary (more than 7|F|/20 of A ∩ B, minus the bad ones).
Blueprint lines 2180-2181: by stabilization, the joined witnesses of a common later nonexceptional height-good primary nest the earlier PRE predecessor inside the later one.
Blueprint eq:representative-separation (lines 2184-2190): if the affine frequency
difference 2λx + γ exceeds θ at one point of a cell of length r and 2|λ| r ≤ θ/2, it
exceeds θ/2 everywhere on the cell.
Blueprint eq:size-comparison (lines 2196-2209): with
σ² = Σ_D (‖A_D‖ + y_D)², Σ_D ‖A_D‖² ≤ c ‖T_F - V_F‖², coefficient floors Σ_D y_D² ≤ η,
and ‖P_F ZTilde - T_F‖ ≤ ε, one has σ² ≤ 6c (‖P_F ZTilde‖² + ε² + ‖V_F‖²) + 2η.
Hereditary representatives (blueprint lines 2172-2191) #
Blueprint lines 2181-2182 ("process pre-cells chronologically: inherit an earlier
representative when its predecessor is contained, otherwise pick any mode"): the representative
of c' is that of some earlier c with E c ⊆ E c', if there is one, and otherwise a fixed
element of E c'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint lines 2176-2181 (nesting of predecessors along a link): let f transport an earlier
component system C into a later one C' on a descendant pre-cell, preserving primaries, PRE
components and CURRENT components. If m is good at h in C, m' is good at h in C',
f m lies in the later CURRENT component of m', the later system stabilizes good primaries,
and the later predecessor has fewer than twice the primaries of the earlier one (equal first type
coordinates), then the earlier PRE predecessor is transported into the later one.
Separation of representative frequencies (eq:representative-separation, 2184-2192) #
Blueprint line 2192: without a gap edge at height h, every allowed shift leaves the affine
frequency difference above θ at some point, hence above θ/2 on the whole cell when its
variation over the cell is at most θ/2 (eq:slope-variation).
Blueprint eq:representative-separation (lines 2184-2192): two modes alive on the pre-cell
J' of block b' that lie in different CURRENT components at height h have, for every allowed
shift n, frequency difference above Ξ / (2 r_{t_{b'}}) on the whole pre-cell, when the
curvature difference obeys eq:slope-variation; on actual cells I, I' of length at least
r_{t_{b'}} this is at least (Ξ/2) max(|I|⁻¹, |I'|⁻¹).
Component sizes (blueprint lines 2193-2209, eq:size-comparison) #
The lower half of almost_orthogonal_synthesis (blueprint line 2201, "two-sided almost
orthogonality"): (1 - η D³) Σ ‖v_e‖² ≤ ‖Σ v_e‖².
The lower half of subtotals_almost_orthogonal: subtotals over disjoint components with
small mutual pairings satisfy (1 - η D³) Σ_j ‖T_j‖² ≤ ‖Σ_j T_j‖².
Blueprint eq:size-comparison (lines 2196-2209), first assertion, at one actual cell: the core
subtotals A_D = Σ_{m core in D} α_m Ψ_m of the minimal CURRENT components D ⊆ F (pairwise
almost orthogonal, η D³ ≤ 1/2) with coefficient floors y_D (Σ y_D² ≤ η_f) satisfy
σ_F² = Σ_D (‖A_D‖ + y_D)² ≤ 12 (‖P_F ZTilde‖² + ε² + ‖V_F‖²) + 2 η_f, when the full subtotal is
T_F = V_F + Σ_D A_D and ‖P_F ZTilde - T_F‖ ≤ ε.
Blueprint eq:size-comparison, second assertion: the side subtotals V_F of distinct CURRENT
components of a linear side V = Σ_F V_F satisfy Σ_F ‖V_F‖² ≤ 2 ‖V‖² (η D³ ≤ 1/2).
First tops and their count (prop:tops, blueprint lines 2211-2231) #
Blueprint lines 2227-2229 (eq:top-count, second bound): if every used representative
a ∈ A at a point y has a retained first top containing y, distinct representatives having
distinct tops, then |A| is at most the number of retained tops containing y.
Blueprint lines 2226-2227 ("Markov's inequality and first crossings of their partial top
counts"): tops t ∈ T on cells cell t ∈ S with total length Σ_t |cell t| ≤ M |R| are cut at the
first crossings of M/ρ, at cost ρ|R|, after which every point lies in at most M/ρ retained
tops.
Blueprint line 2192 (eq:slope-variation on the later pre-cell): two modes alive at the
decision cell of a pre-cell J' of block b' have curvature difference with
2 |λ' - λ| r_{J'} ≤ Ξ / (2 r_{t_{b'}}) once 8 Λ ≤ Ξ.
Blueprint eq:representative-separation (lines 2184-2192) for modes alive at a decision
cell: two modes in different later CURRENT components are separated by
(Ξ/2) max(|I|⁻¹, |I'|⁻¹) on the whole pre-cell, for every allowed shift.
The private lower bound of a synthesis of cell modes: ε |J| Σ |α|² ≤ ‖Σ α_m Ψ_{J,m}‖².
The goodness at height h of a component of the block b on the pre-cell J: the goodness of
a mode whose minimal PRE component it is.
Equations
- One or more equations did not get rendered due to their size.
Instances For
hereditaryRep_inherit when only earlier cells with meeting predecessors need to be
comparable (several components per pre-cell, blueprint lines 2181-2183: "two earlier
predecessors contained in the current one ... intersect and, lying on one path, are linked").
Stabilization of the frozen mode graphs at the schedule (blueprint lines 2179-2181) #
Blueprint lem:stabilize (lines 2002-2028) for the frozen mode graphs at the chosen schedule, as
used at lines 2179-2181 ("stabilization joins its two witnessing modes in later PRE"): on a
pre-cell J of depth v_b = b - 2K, two alive modes of one key that is good at a height
h ≤ J_* (goodP with the side parameters of the schedule) and lie in one CURRENT component at
h are PRE-joined at h - Δ, Δ = 10. The alive modes number at most D_*, the dimensions are
at most d_max, and D_* covers the heights of the mode differences
(2 (Q₀ (3 B_σ²)²)² ≤ ⌊D_*⌋, line 1934).
The PRE predecessor at h - Δ of the component of the mode c.2.2 at the node
(c.1, c.2.1) (the singleton of the mode if it is not alive there).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Comparability of mode nodes: a later block on a descendant pre-cell.
Equations
- Ms.nodeLt3 Nd c c' = (c ∈ Nd ∧ c' ∈ Nd ∧ TrilinearHT.Auto.dyadicGridCell Gd c'.2.1.1 c'.2.1.2 ⊆ TrilinearHT.Auto.dyadicGridCell Gd c.2.1.1 c.2.1.2 ∧ c.1 < c'.1)
Instances For
Blueprint lines 2172-2191 (THT.Modes.hereditaryRepresentatives) for all successful
components at once: the nodes are triples (b, J, m) with one good mode m per CURRENT component
at each pre-cell. The chronological representatives lie in their predecessors, are inherited under
predecessor inclusion, and different representatives on comparable nodes have disjoint
predecessors in different later CURRENT components.
The first role type of a mode node: the dyadic size class of the number of primaries of its PRE predecessor (blueprint line 2708, "fix ... all role types").
Equations
- One or more equations did not get rendered due to their size.
Instances For
The second role type of a mode node: the dyadic size class of its predecessor.
Equations
- Ms.nodeType2 S hA Δ h c = Nat.log 2 (Ms.predOfMode S hA Δ h c).card
Instances For
Blueprint lines 2172-2191 with the role types fixed (attempt_representatives3 on each type
class of nodes): there are representatives rep k₁ k₂ for every type class, in the predecessors of
the nodes, inherited and separated along comparable nodes of the class.
Blueprint lines 2172-2185 (THT.Modes.hereditaryRepresentatives) at the chosen schedule: with
the side parameters of the schedule (Δ = 10) at a height h ≤ J_* (the upper end of
H_up, line 2041), the stabilization step ("stabilization joins its two witnessing modes in later
PRE") is lem:stabilize for the frozen mode graphs (blockComps_stab). Hence, for fixed height
and types, representatives in the PRE predecessors exist, are inherited under predecessor
inclusion along comparable nodes, and different representatives on comparable nodes have disjoint
predecessors with no shared or CURRENT-adjacent modes in the later graph. The alive modes at each
decision cell number at most D_* and D_* covers the heights of the mode differences (the
choices of D_*, lines 1932-1934).
Elements of the predecessor of a mode node are alive at its decision cell.
Blueprint eq:representative-separation at a path point for the representatives of
attempt_representatives3: different representatives on mode nodes whose pre-cells contain x*
have labels ω_a(x*) separated by (Ξ/2) max(r_I⁻¹, r_{I'}⁻¹) against every shift
n·θ/(Q₀ L_h), |n| ≤ E_h.
Component sizes at an actual cell (blueprint lines 2196-2209, eq:size-comparison) #
Blueprint line 2055 at threshold Ξ/2: the pairing constant is at most 2 D_*^{-200}.
cellMode_inner_le with the height-zero separation given directly at threshold Ξ'/|J| on the
cell (the form of lem:mode-rows on the smaller cell).
A cell mode restricts on a subcell to the cell mode of the subcell.
Blueprint lines 2202-2203 ("two-sided almost orthogonality for arbitrary subtotals in distinct
minimal CURRENT components"), one pair: two modes alive at the decision cell of the pre-cell J
of the block b that lie in different minimal CURRENT components pair on an actual cell I ⊆ J
of length at least r_{t_b} by at most η |I|, with η the pairing constant at threshold
Ξ/2 (eq:slope-variation halves the CURRENT threshold on the whole pre-cell).
The modes of the CURRENT component F_h(x) of the block b on the pre-cell J.
Equations
- Ms.compModes S hA b J h x = Finset.map { toFun := Subtype.val, inj' := ⋯ } ((Ms.blockComps S hA b J).F h x)
Instances For
The minimal (height zero) CURRENT components inside F_h(x), as mode sets.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Two CURRENT components at one height are equal or disjoint.
Modes of different CURRENT components at a height are not CURRENT-joined there.
The minimal CURRENT components inside F_h(x) cover its modes.
Sums over the filtered members of pairwise disjoint finite sets are sums over the filtered union.
A core mode of the block b on the pre-cell J: alive at the decision cell and with at most
δ_* (J_* + 1) bad heights (line 2037).
Equations
Instances For
Blueprint eq:component-size (lines 2196-2201) on the actual cell I:
σ_F² = Σ_{D ⊆ F} (‖A_D‖_{2,I} + D_*^{-30} Σ_{m core in D} |α_m|)² over the minimal CURRENT
components D of F = F_h(x), with the full core subtotals A_D = Σ_{m core in D} α_m Ψ_{I,m} and
the normalized norm ‖f‖_{2,I} = |I|^{-1/2} ‖1_I f‖₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
At the schedule, Ξ = D_*^{1000} dominates 16 Λ when Λ ≤ D_*.
Blueprint eq:size-comparison (lines 2202-2209), first assertion, at an actual cell I of
length at least r_{t_b} inside the pre-cell J of the block b, for the CURRENT component
F = F_h(x): with the frozen coefficients c of ZTilde_{l,G,b} on J (square sum at most
B_c over
the alive modes; B_c = 4 D_*² C_F by frozen_coeffs),
σ_F² ≤ 12 (‖P_{F,I} ZTilde‖²_{2,I} + ‖V_F‖²_{2,I}) + 3 B_c D_*^{-59}, where P_{F,I} projects
onto
the modes of F on I and V_F is the exact linear-side subtotal of F on I.
Proof as in the blueprint: the core subtotals of distinct minimal CURRENT components are almost
orthogonal (actualCell_inner_le, cross pairings ≤ 2 D_*^{-200} |I|), so
Σ_D ‖A_D‖² ≤ 2 ‖T_F - V_F‖²; the coefficient floors cost at most D_*^{-59} B_c; and pairing the
complementary modes against the range of P_{F,I} gives
‖P_{F,I} ZTilde - T_F‖² ≤ 4 D_*^{-397} B_c |I|
(projection_subtotal_close). The schedule enters through Ξ = D_*^{1000}, Λ ≤ D_*, the Fourier
norm and tail of the squared gauge, the inverse private weights at most D_* and at most D_*
alive modes (line 2055).
The CURRENT components at height h of the block b on the pre-cell J, as mode sets.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint eq:size-comparison (lines 2202-2209), second assertion ("decomposing V into all
height-h CURRENT components and discarding unsuccessful ones"): on an actual cell I of length
at least r_{t_b} inside the pre-cell J of the block b, for any family Fs of CURRENT
components at height h, the exact side subtotals satisfy Σ_{F ∈ Fs} ‖V_F‖² ≤ 2 ‖V‖², where
V = Σ_{m alive, side} α_m Ψ_{I,m} is the linear side on I.
The side events of a pre-cell partition its side modes (blueprint line 2084, "it is entirely
side by the predicate coherence", core_iff_of_minimal_pre).
The block side subtotal V_{l,G,b} restricted to an actual cell I inside one of its pre-cells
J is the side synthesis on I with the frozen coefficients of J.
Blueprint eq:size-comparison (lines 2202-2209), second assertion, with V = V_{l,G,b}: on an
actual cell I of length at least r_{t_b} inside a pre-cell J of the block, for any family
Fs of CURRENT components at height h, Σ_{F ∈ Fs} ‖V_F‖²_{2,I} ≤ 2 ‖V_{l,G,b}‖²_{2,I}.
Cross-mode separation of components with different representatives (lines 2183-2185) #
The linking step of attempt_representatives3 (blueprint lines 2176-2181): if the mode of an
earlier node is CURRENT-joined at height h in the later graph to the mode of a later comparable
node of the same first type, the earlier predecessor is contained in the later one.
Blueprint lines 2183-2185 ("different representatives on comparable actual-use cells have no
shared or adjacent cross modes in the later CURRENT graph"), at the level of whole components:
for representatives inherited under predecessor inclusion, if two comparable nodes of one type
class have different representatives, no mode of the earlier CURRENT component is equal or
CURRENT-adjacent (in one later CURRENT component at h) to a mode of the later component.
Rows on the first tops with path counts (prop:tops, lines 2221-2222) #
Blueprint prop:tops, lines 2221-2222 (lem:mode-rows on the rows P_{F,I} of the tops), with
the path counts of the blueprint: rows on cells with nonempty mode sets alive on their cells, such
that overlapping distinct rows meet in one of their cells, have disjoint mode sets and are
separated there at threshold Ξ' for every allowed shift, are Bessel with constant 1 + η D³ when
at most D modes (and at most ε D²) are alive at every point.
First tops of the representatives (prop:tops, lines 2221-2222) #
The modes of the CURRENT component at height h of a node (b, J, m) (the mode alone if it is
not alive at the decision cell).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The predecessor of a node lies in its CURRENT component.
Blueprint line 2221 ("take the first actual-use cells on each branch where a given
representative has σ_F ≥ σ"): among the instances (I, c) (a use cell I and the node c of
a component used there) with size at least σ₀, those whose cell is maximal among the instances
of the same representative with size at least σ₀.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The row of a top: its block, its cell and the modes of its component.
Instances For
eq:representative-separation at the left endpoint of an actual cell I ⊆ J of length at least
r_{t_b}, at height zero.
Blueprint lines 2221-2222 ("tops for that representative do not overlap; different
representatives on overlapping tops have component-mode nonadjacency ... their sets are disjoint on
a path"): for two first tops with nested cells I ⊆ I' and different rows, the component modes are
disjoint and every pair (inner, outer) is separated at threshold (Ξ/2)/|I| at the left endpoint
of I, for every allowed shift at height zero. Hypotheses: the nodes, representatives and
type-class conclusions of typed_representatives, blocks K-spaced, and instances (I, c) with
I inside the pre-cell of c at a depth of its block.
Hereditary representatives of one type class at height h (blueprint lines 2172-2185): the
nodes (b, J, m) (one good mode per successful CURRENT component of a pre-cell) with the
hypotheses and conclusions of typed_representatives, the blocks being K-spaced.
Finite family of nodes in the representative class at the fixed height.
- hstab (c : ℤ × (ℤ × ℤ) × Ms.Md) : c ∈ self.Nd → ∀ (z z' : ↥(Ms.alive (ancAt Gd c.2.1 (c.1 - 4 * ↑S.K)))), Ms.goodP S SP c.1 h ((Ms.blockComps S hA c.1 c.2.1).π z) → (Ms.blockComps S hA c.1 c.2.1).π z' = (Ms.blockComps S hA c.1 c.2.1).π z → z' ∈ (Ms.blockComps S hA c.1 c.2.1).F h z → z' ∈ (Ms.blockComps S hA c.1 c.2.1).E (h - Δ) z
- k1 : ℕ
Common binary logarithm of the predecessor-component primary-label count.
Chosen predecessor mode representing each node in the class.
Instances For
The instances of a type class: use cells I inside the pre-cell of a node c, at a depth of
its block.
Equations
Instances For
Distinct first tops have distinct rows.
Blueprint prop:tops, lines 2221-2222 (lem:mode-rows on the rows P_{F,I} of the first tops of
one type class at height h and threshold σ₀), at the schedule: the rows of the first tops are
Bessel with constant 2, when Λ ≤ D_*, D_* covers the Fourier norm and tail of the squared
gauge, the inverse private weights are at most D_* and at most D_* modes are alive at every
point.
Grouping a sum over a finite set of pairs (b, d) by the first coordinate, when at most K
second coordinates occur with each first coordinate (they lie in [b, b + K)).
Blueprint prop:tops, lines 2224-2225 (the side part of eq:size-comparison on the tops):
"sum first at a fixed depth of a block: cells are disjoint and component subtotals sum in square to
C ‖V_{l,G,b}‖²; summing the at most K depths" gives
Σ_tops ‖V_F‖²_{2,I} ≤ 2 K Σ_b ‖V_{l,G,b}‖² for the first tops of one type class, with V_F the
exact side subtotal of the top's component on its cell (frozen coefficients c b J).
The component size σ_F² (eq:component-size) of the node of an instance (I, c) on its
cell, with the frozen coefficients c b J of its block and pre-cell (zero off the alive modes).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint prop:tops, lines 2226-2229 (before the cut): on the first tops of one type class at
threshold σ₀ (sizes σ_F² ≥ σ₀), eq:size-comparison and the absorption of its error
(6 B_c D_*^{-59} ≤ σ₀, from σ² ≥ D_*^{-2}) give
σ₀ Σ_tops |I| ≤ 24 (Σ_tops ‖P_{F,I} ZTilde‖² + Σ_tops ‖V_F‖²), with ZTilde the frozen
evaluation on the
top's pre-cell.
The ancestor at a depth above a containing cell is the ancestor of that cell.
The row projection of an event is local to every set containing its cell.
Blueprint prop:tops, lines 2221-2227, for one height, one type class (representatives R G of
each group) and one threshold σ₀: on the first tops of the actual uses,
σ₀ Σ_G Σ_tops |I| ≤ 24 (2 G₀ |R| + 2 K V_E).
lem:mode-rowson the rowsP_{F,I}of the tops (RepClass.firstTops_rows, Bessel constant2); their decision cells are the containingu_b-cells, active and certified by the tops (retained_decision), solem:lift-composition(lift_composition_dep,liftConst_le_G0) givesΣ_tops ‖P_{F,I} ZTilde_{l,G,b}‖² ≤ 2 G₀ |R|;- the side part:
Σ_tops ‖V_F‖² ≤ 2 K Σ_{G,b} ‖V_{l,G,b}‖² ≤ 2 K V_E(RepClass.tops_side, withV_Ethe linear-side energy ofeq:linear-energy); eq:size-comparisonand absorption on each top (RepClass.tops_absorb,6 B_c D_*^{-59} ≤ σ₀).
The frozen coefficients c represent ZTilde_{l,G,b} = R_{l,G} Z_{l,G,u_b} on the retained
pre-cells
with square sums at most B_c (frozen_coeffs, linear_energy); the instances are use cells
inside retained pre-cells of blocks in Bs.
Counting the used representatives by first tops (prop:tops, line 2229) #
Blueprint line 2229 ("each representative used in the bin has a ... first σ-top above that
use"): an instance of size at least σ₀ lies below a first top of its representative.
card_reps_le_firstTops restricted to the cells of an upward closed family (for instance the
cells not inside any cut cell): the distinct representatives of the instances of size at least
σ₀ used at y on such cells are at most the first tops containing y on such cells.
Blueprint line 2229 ("there are polynomially many choices ... Markov's inequality and first
crossings of their partial top counts give simultaneously Σ_tops 1_I(y) ≤ P^C σ^{-2} outside a
small root fraction, after increasing the fixed power for their number"): for finitely many
choices ch with tops of total length Σ_t |I_t| ≤ M_ch |R|, the first crossings of the partial
top counts at the thresholds M_ch N/ρ (N choices) remove root length at most ρ |R|, and
every point lies in at most M_ch N/ρ tops of every choice on cells not inside a removed cell
(the retained paths).
Blueprint prop:tops, eq:top-count (lines 2212-2229), for given type classes of hereditary
representatives: after first-crossing cuts of total root length at most ρ |R|, at every point y
outside the cuts, for every height h ∈ Hs, type τ ∈ Ts and threshold σ ∈ Thr
(σ ≥ D_*^{-1}), the distinct representatives A_G of the components used at y with size
σ_F ≥ σ satisfy Σ_G |A_G| ≤ min(D_*, M N / (ρ σ²)), with M = 24 (2 G₀ + 2 K V₀) and N the
number of choices (V₀ |R| bounds the linear-side energy eq:linear-energy). The first bound is
the full mode budget along the path; the second comes from tops_energy for each choice and the
first crossings of the partial top counts (tops_cut_many), each used representative having a
retained first top above its use (card_reps_le_firstTops).
The empty representative class (no nodes; every mode represents itself).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint lines 2172-2185 at the schedule, for one height h ≤ J_* and one type (k₁, k₂):
nodes (b, J, m) (one good mode per successful CURRENT component of a pre-cell of depth v_b,
nodes on one pre-cell lying in different components) of this type, with their hereditary
representatives (typed_representatives_sched), form a RepClass (Δ = 10, the side parameters
of the schedule). The blocks are K-spaced (K ∣ b - R₀), at most D_* modes are alive at each
decision cell and D_* covers the heights of mode differences.
A fixed enumeration of the modes.
Equations
- Ms.modeIdx m = ↑((Fintype.equivFin Ms.Md) m)
Instances For
Blueprint lines 2172-2174 (successful components and their good modes): the modes alive at the
decision cell of the pre-cell J of the block b that are good at height h, lie in a CURRENT
component containing a core mode good at h (a successful component), and have the least index
among the good modes of their component: one good mode for each successful component.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The nodes (b, J, m) of the successful components over a set P of pairs (block, pre-cell).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The successful nodes are alive, of depth v_b, good, and distinct nodes on one pre-cell lie in
different CURRENT components (the node hypotheses of exists_repClass).
The used instances of a group (blueprint line 2214, "used representatives"): an actual-use cell
I of the group inside the pre-cell of a node (b, J, m), at a depth of its block [b, b + K).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The retained pairs (b, J) of a group: blocks b ∈ Bs and retained v_b-cells J.
Equations
Instances For
Blueprint line 2229 ("the full mode budget proves the first [bound]; for σ < D_*^{-1} the full
budget already implies the minimum"): at every point and for every threshold, the distinct
representatives used at y over all groups number at most D_*, since they are modes alive at
y and at most D_* modes are alive along a path across groups.
Blueprint prop:tops (eq:top-count, lines 2212-2229) for one basic role l, color k and
ball level j, with the hypotheses of eq:linear-energy (linear_energy): there are frozen
coefficients c of ZTilde_{l,G,b} on the retained pre-cells (with the linear-side energy
bound), and
for every height h ≤ J_* and type τ the hereditary representatives of the successful components
(RepClass on the successful nodes succNodes of the retained pre-cells, of type τ), such that
after first-crossing cuts of total root length at most ρ |R|, at every point y outside the cuts,
for every height h ≤ J_*, type τ ∈ Ts and threshold σ ∈ Thr (σ ≥ D_*^{-1}), the distinct
representatives A_G of the successful components used at actual-use cells of G containing y
with size σ_F ≥ σ satisfy Σ_G |A_G| ≤ min(D_*, M N / (ρ σ²)), where
M = 24 (2 G₀ + 2 K V₀) (V₀ |R| the linear-side energy bound) and N is the number of choices
of height, type and threshold. The schedule hypotheses are those of linear_energy and of
typed_representatives_sched, and D_* covers the normalization constant (24 C_F ≤ D_*^{55}).