Section 12.2: Decreasing colors and historical masks #
This file was automatically generated by Claude.
Formalization of blueprint Section 12, "Curvature localization" (sec:localization), subsection 2,
"Decreasing colors and historical masks" (lines 1712-1795) of
blueprint/formalization_blueprint.tex.
The data of the coloring (blueprint lines 1714-1728): graph distances, the parameters
d₀, b₁, b₂ and the primary and high delay arrays (one per round), with values in [0, d₀].
- dist : DepthDistance V
Depth-dependent distance used to compare chart labels.
- d0 : ℕ
Number of coloring rounds and bound for each delay value.
- b1 : ℕ
Distance scale dividing graph distances in the primary score.
- b2 : ℕ
Distance scale dividing graph distances in the high score.
Primary delay assigned to each label in each round.
High delay assigned to each label in each round.
Instances For
The primary score D_z - ⌊d_s(z,v)/b₁⌋ of z at the center v (distance quotients capped
at d₀ + 6, which does not affect top scores or gaps).
Instances For
The signature of a family of rounds: the winner predicates and the top scores.
Equations
- TrilinearHT.Auto.ColorSetup.roundSig X sc ρ = (TrilinearHT.Auto.RoundWinner X (sc ρ), TrilinearHT.Auto.roundTop X (sc ρ))
Instances For
The primary data (round, winner z, top score g) of the center v at a state.
Equations
- K.prim A v = TrilinearHT.Auto.ColorSetup.sigData (TrilinearHT.Auto.ColorSetup.roundSig A.X fun (ρ : Fin K.d0) => K.psc A.s ρ v)
Instances For
The rival profile f_a(s') = max_{w ∈ W∖{z}} (b₁ D_w - d_{s'}(w,a)) (-∞ when empty or at
infinite distance).
Equations
Instances For
The fixed pseudometric d^{(l)}(a,b) = sup_{s'} |C_l(f_a(s')) - C_l(f_b(s'))| of a context.
Equations
Instances For
The floor logarithms of the sizes of the balls B_{d^{(l)}}(v, R_l) on the present list.
Equations
Instances For
The least 1 ≤ l < d₀ whose two consecutive balls have the same floor logarithm, and that
common value n (placeholder (0,0) on failure).
Equations
Instances For
The high score E_a - ⌊d^{(l+1)}(a,v)/b₂⌋ (capped at d₀ + 6).
Equations
Instances For
The complete color data at a state: primary data, cohort level, ball selection and high data (winners included).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The first potential: the sum over primary rounds of the round potentials.
Instances For
The third potential: the total floor-logarithm of the ball sizes.
Equations
Instances For
The fourth potential: the sum over high rounds of the round potentials.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The lexicographic potential of the color data, with bounds B₂, B₃, B₄ on the last three
coordinates.
Equations
Instances For
One step along a path: the potential does not decrease, and if it stays constant then the complete color data (including both winners) are unchanged.
A dyadic tree of cells with admission lists (blueprint §12.1-12.2): parents, heights above a virtual top level (where lists are empty), depths and present lists with admission positions; lists extend along every path.
- Cell : Type u_2
Cell type of the abstract tree of admissible states.
Parent cell in the admissible-state tree.
Natural-number height above the top of the tree.
Integer depth associated with each tree cell.
Finite set of labels present at each tree cell.
Position of each label in the finite list at a tree cell.
Instances For
The number of changes of the color data of v along the last n ancestors of I.
Equations
Instances For
The number of changes of the color data of v along the whole ancestor path of I.
Instances For
The number of changes is bounded by the potential.
The color metadata (blueprint line 1728): the primary round and g, the cohort level, l
and n, and the high round and g₂; winners are not part of the metadata.
Equations
Instances For
The color of v at I (blueprint line 1728): a change counter, decremented at every change
of the color data along the path, followed by the encoded metadata.
Equations
Instances For
Colors do not increase along a path (blueprint line 1730).
Equal colors have equal metadata (blueprint line 1728).
Profiles and the context pseudometrics #
Profiles increase with depth.
Profiles are 1-Lipschitz in the vertex for the graph distance at the same depth.
The clipped profile difference whose supremum defines the context pseudometric.
Equations
Instances For
The pseudometrics decrease in l (blueprint line 1738).
Historical masks (blueprint lines 1748-1771) #
The numerical relations of blueprint lines 1714-1717 used by the masks:
b₂ = 100 (H_max + 1), b₁ = d₀^{10} b₂ (H_max + 1) and d₀ ≥ 8 (the blueprint has d₀ ≥ 1000 log 2).
Instances For
Rival terms at a successful center are at most (g - 5) b₁ at all earlier depths.
Blueprint lem:masks, first assertion (pseudometric part): at a successful center, every
present vertex within graph distance h ≤ 2 b₁ has context distance at most h for every
l ≤ 2 d₀.
Unfolding the color data of a successful primary round.
The mask predicate eq:ball-mask for a vertex b at depth s with pad h, relative to a
historical central vertex whose (successful) color data are c and whose frozen prefix is W.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The group of a central vertex: its color and complete color data (winners, levels and rounds; the frozen prefix and cohort block are determined by these along a path).
Instances For
The mask M_{G,h} at a cell (blueprint eq:ball-mask): present vertices satisfying the mask
predicate for some historical central vertex of the group at or above the cell.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Blueprint lem:masks, first assertion: at an actual use centered at v, every present vertex
within h graph edges of v lies in M_{G,h}.
Blueprint lem:masks, third assertion: an admitted mask vertex is within graph distance
(d₀ + 1) b₁ + H_max of the primary winner (which lemma graph turns into a short path).
Masks persist to finer cells (blueprint line 1755: the mask increases inside its cohort).
The high winner is within (d₀ + 1) b₂ of the center in d^{(l+1)}.
The ball comparison of blueprint lines 1762-1763: a historical central vertex v₀ of the
group and the current center v are within 2 R_l in d^{(l)}.
The numerical inequalities of blueprint lines 1763-1765:
A_h + 1 ≤ T_{l+1} - T_l with A_h = 10 R_l h + 2 R_l.
The data of a use: the center's successful color data and the common frozen prefix.
Unpacking a mask membership for the group of a successful center.
eq:rival-bound (blueprint lines 1763-1766): at an actual use centered at v, every vertex
of the pad-h mask has rival profile at most T_l + A_h, A_h = 10 R_l h + 2 R_l, at all
depths up to the use.
Blueprint lem:masks, second assertion (neighbor closure): at an actual use, every present
neighbor of a vertex of M_{G,h} belongs to M_{G,h+1} when h < H_max.
Two adjacent vertices, one of which has small rival profile up to depth s, are within
their graph distance in the high pseudometric d^{(l+1)}.
Distinct high winners of one high round and top score at two comparable historical centers
force the centers far apart in d^{(l+1)} (blueprint lines 1770-1771).
Blueprint lem:masks, fourth assertion (separation): for distinct groups of one color, vertices
of their pad masks on overlapping usable endpoints I ⊇ J (each with an actual use below it) are at
graph distance greater than one at the finer endpoint.
Choice of the delays (blueprint lines 1732-1733) #
Delays are truncated geometric: P(D = n) = 2^{-(n+1)} for n < d₀ and P(D = d₀) = 2^{-d₀}.
A single round is marked with probability at least 1/66 once |X| ≤ 2^{d₀ - 5}: raising the
delay of a top scorer by five marks the round, injectively, at a weight cost at most 2^{-5}.
The product weight of a delay array.
Equations
- TrilinearHT.Auto.cfgW d0 D = ∏ z : V, TrilinearHT.Auto.geomW d0 (D z)
Instances For
A top scorer of a round.
Equations
- TrilinearHT.Auto.topScorer X hX c D = Classical.choose ⋯
Instances For
Blueprint lines 1732-1733: a single round is marked with probability at least 1/66 when
|X| 2^{4 - d₀} ≤ 1/2.
The weight of an array of d₀ independent delay arrays.
Equations
- TrilinearHT.Auto.roundsW d0 D = ∏ ρ : Fin d0, TrilinearHT.Auto.cfgW d0 (D ρ)
Instances For
A finite chain: on a finset totally preordered by r, a function determined by a monotone
potential takes at most as many values as the potential.
The coloring setup of given primary and high delay arrays.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ball selection succeeds deterministically once d₀ exceeds the floor-log range
(blueprint line 1739).
The potential is monotone along ancestor chains, and constant potential means constant color data.
The primary situation of a center at a cell: the present list and the capped distance quotients, which determine whether all primary rounds fail.
Equations
Instances For
The capped high offsets min(⌊d^{(l+1)}(a,v)/b₂⌋, d₀ + 6) of the selected context.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The high situation of a center at a cell: the present list and the high offsets.
Instances For
The potential of the high situation.
Equations
Instances For
Primary failure is the failure of all primary rounds at the primary situation.
High failure is the failure of all high rounds at the high situation.
High situations do not depend on the high arrays.
Some vertex at the cell has unsuccessful color data.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Counting the situations of the centers along a chain.
The failure probability along one path (blueprint lines 1732-1733): the union bound over the primary situations and, conditionally on the primary arrays, over the high situations.
Blueprint lines 1732-1734: the delays can be fixed so that the cells carrying a failed
marking have total length at most the path failure bound times |R|.
The coloring parameters (blueprint lines 1714-1717) #
The explicit failure bound of delays_exist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The failure bound tends to zero: with d₀ = ⌈1000 log 2D⌉ and at most D vertices it is at
most 100 · 2001⁷ / D (blueprint line 1732: the union bound tends to zero as D grows).
Blueprint §12.2 (Declaration coloring, THT.Localization.monotoneColoring): with
d₀ = ⌈1000 log 2D⌉ and at most D original vertices, the delays can be fixed so that the
cells with a failed marking have total length at most 100 · 2001⁷ |R| / D; the colors lie in
[1, L] with L ≤ d₀^{30}, do not increase along paths (the change counter decreases at every
change of the color data), and equal colors carry equal metadata.
Blueprint lem:masks (Declaration masks, THT.Localization.historicalMaskSeparation): for
the pad masks M_{G,h} of eq:ball-mask with h ≤ H_max,
(1) at an actual use centered at v every present vertex within h graph edges of v lies in
M_{G,h}; (2) at an actual use every present neighbor of a vertex of M_{G,h} lies in
M_{G,h+1} when h < H_max; (3) every mask vertex is within graph distance
(d₀ + 1) b₁ + h of the primary winner (so lemma graph gives a short path); (4) for distinct
groups of one color, vertices of their pad masks on overlapping usable endpoints are at graph
distance greater than one at the finer endpoint.
Whole endpoint ranges (blueprint lem:whole-ranges, lines 1777-1791) #
A group output Z_G(y) = Σ_v a_{v,G}(y) Φ_v(y) with combined coefficients.
Equations
- TrilinearHT.Auto.groupOutput φ ε a y = ∑ v : V, a v y • TrilinearHT.Auto.privateColumnValue φ ε v y
Instances For
|Σ z_G|² = Σ_G |z_G|² + Σ_{G ≠ G'} Re(conj z_G z_{G'}).
Blueprint lem:whole-ranges, analytic core: group outputs Z_G = Σ_v a_{v,G} Φ_v with private
coordinates that never coincide on overlaps, cross physical pairings at most τ ∫ |a_{v,G}| |a_{w,G'}|, at most N nonzero coefficients at each point and inverse private weights at most
W₀² satisfy ‖Σ_G Z_G‖² ≤ (1 + τ N W₀²) Σ_G ‖Z_G‖².
Only finitely many cells of one depth meet a bounded interval.
A function constant on the cells of one depth, supported in finitely many of them, pairs
against ψ with the per-cell bound (the grid argument of blueprint line 1785).
The combined coefficient a_{v,G} = Σ_I a_{v,G,I} 1_I of the occurrences of v in G.
Equations
- TrilinearHT.Auto.occCoef Gd occ c G v y = ∑ I ∈ occ G v, (TrilinearHT.Auto.dyadicGridCell Gd I.1 I.2).indicator (fun (x : ℝ) => c G v I) y
Instances For
Blueprint lem:whole-ranges (Declaration whole-ranges, THT.Localization.usableRangeBessel):
group outputs Z_G = Σ_v a_{v,G} Φ_v whose combined coefficients are constant on entire endpoint
cells satisfy ‖Σ_G Z_G‖² ≤ (1 + τ N W₀²) Σ_G ‖Z_G‖² provided
(i) overlapping endpoint cells of labels in different groups have depth at most the last
separating depth s_*(v, w) of the two labels (lemma masks),
(ii) at that depth the physical pairing of the two pure columns is at most τ on every cell
(lemma graph), for labels with overlapping occurrences in different groups,
(iii) private labels never coincide on an overlap, and
(iv) at most N group-label pairs are present at each point and inverse private weights are
at most W₀².
One attempt: the admission tree (blueprint lines 1677-1681) #
The cells of the finite tree below R.
Equations
- TrilinearHT.Auto.AdmCell G R N = ↥(TrilinearHT.Auto.dyadicFiniteTree G R N)
Instances For
Two ancestors of one cell at the same depth coincide.
The parent of a non-root cell lies in the tree.
Ancestors-or-self of a cell in the tree at which a label is available.
Equations
- TrilinearHT.Auto.admAnc av I v = {J : TrilinearHT.Auto.AdmCell G R N | TrilinearHT.Auto.dyadicGridCell G (↑I).1 (↑I).2 ⊆ TrilinearHT.Auto.dyadicGridCell G (↑J).1 (↑J).2 ∧ av (↑J) v}
Instances For
The admission cell of a label along the path of I: its shallowest available ancestor.
Equations
- TrilinearHT.Auto.admCellOf av I v = if h : (TrilinearHT.Auto.admAnc av I v).Nonempty then Classical.choose ⋯ else I
Instances For
The vertices: a label with its admission cell.
Equations
- TrilinearHT.Auto.AdmVertex = (Λ × TrilinearHT.Auto.AdmCell G R N)
Instances For
The present vertices at a cell.
Equations
- TrilinearHT.Auto.admPresent av I = Finset.image (fun (v : Λ) => (v, TrilinearHT.Auto.admCellOf av I v)) {v : Λ | (TrilinearHT.Auto.admAnc av I v).Nonempty}
Instances For
The present vertices of the parent are present at the child.
The admission key: admission depth first, then the label order.
Equations
- TrilinearHT.Auto.admKey x = ((↑x.2).1 - R.1).toNat * Fintype.card Λ + ↑((Fintype.equivFin Λ) x.1)
Instances For
The admission position of a present vertex.
Equations
- TrilinearHT.Auto.admPos av I x = {y ∈ TrilinearHT.Auto.admPresent av I | TrilinearHT.Auto.admKey y < TrilinearHT.Auto.admKey x}.card
Instances For
Positions of the parent's vertices are unchanged at the child.
The parent map of the admission tree (the top above the root is its own parent).
Equations
- TrilinearHT.Auto.admPar none = none
- TrilinearHT.Auto.admPar (some I) = if h : ↑I = R then none else some ⟨TrilinearHT.Auto.dyadicParent G ↑I, ⋯⟩
Instances For
Blueprint lines 1677-1681: the admission tree of the finite tree below R: the present
vertices along a path increase, with admission positions ordered by admission depth and then by
label.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The vertex bound D of the attempt: at most 4|L| vertices are present at any cell.
Instances For
One attempt: color parameters and historical masks (blueprint lines 1712-1760) #
The primary depth d₀ = ⌈1000 log 2D⌉ of the attempt.
Equations
Instances For
The high scale b₂ = 100 (H_max + 1) (blueprint line 1716).
Equations
- TrilinearHT.Auto.ActiveSetup.cb2 Hmax = 100 * (Hmax + 1)
Instances For
A vertex of the ball mask of a group lies within the winner bound of the group's center
(blueprint eq:ball-mask, first clause): with the group's primary winner (ρ, z, g), its graph
distance k from z obeys (g - 1) b₁ - h ≤ b₁ D_ρ(z) - k.
Whole endpoint ranges for the attempt (lem:whole-ranges, blueprint lines 1777-1789) #
Masks increase with the pad (blueprint eq:ball-mask).