Hashed construction as a level-3 stage and a level-2 continuation

This is the hashed construction at a chosen reference, in the form of a level-3 stage followed by a level-2 continuation, with the rate budget split between them.

Fix the released global data, with $D=10^{12}$ and $\mathrm{blocks}(K)=D^5K$; write $n=6\,\mathrm{blocks}(k^2)$. For a scale $K$ and a family $a=(a_o)_{o\in\mathrm{Fin}\,6}$ of released global references at scale $K$, let $N_K(a)$ be the number of hashed (positive) positions, and let $\mathcal Q_K(a,e)$ be the hashed source predicate QPos with tolerance $e$ for all six owners.

Claim. For every $e$ with $0<e\le1$ there is $C\in\mathbb N$ such that for every $k_0$ there is $k\ge k_0$ with the following property. If $k>0$, then there are a reference family $a$ at scale $K=k^2$ and

• a partition of the $N_K(a)$ positions into six parts $j\in\mathrm{Fin}\,6$ of sizes $s_j$,
• part predicates $S_j,T_j$ on words of length $s_j$ and a predicate $Q$ on words of length $N_K(a)$, such that the six sources $S_j$ jointly imply $\mathcal Q_K(a,e)$ and $Q$ implies every target $T_j$ (each on its part's positions),
• graded part stages $D_j$ from $S_j$ to $T_j$ with lower level $2$,
• a graded logarithmic joint recipe $R'$ of level $2$ with source $Q$,

satisfying

1. $1\le\mathrm{types}(D_j)\le(k+1)^C$ for each $j$;
2. $n\cdot 0.7363871\le\sum_j \mathrm{rate}(D_j)$;
3. $1\le\mathrm{inputs}(R')\le(k+1)^C$ and $1\le R'.a\,R'.b\,R'.c$;
4. $n\cdot 0.5859676\le\mathrm{logOutputs}(R')$;
5. $n\cdot 5.83785872051\le\log(R'.a\,R'.b\,R'.c)$.

Role. This is the level-3/level-2 split of refthe hashed construction with an explicit dimension target, following the plan in the mission comments: part $j$ is the band-part stage (or the square-scale tolerance stage) for orientation/region $j$, and $R'$ is the level-2 continuation (zero-half boundary, the single-type level-2 step, level-1 boundary). The stage's rate share $0.7363871$ is below $\sum_\rho c_\rho=0.73638718416$ per $n$, the sum of the six proved region rate margins $c_\rho\cdot 6\cdot10^{48}<\mathrm{regionalRate}_\rho$ (with $c_\rho\cdot10^{-12}$ per $n$). The continuation's share $0.5859676$ is below the level-2 margin $0.585967670317$ per $n$. The two shares add to exactly the required $1.3223547$. All dimensions come from the continuation, since a stage does not change dimensions.

Formalization Note. The parts are given by positions : ((j : Fin 6) × Fin (size j)) ≃ Fin (partSize (k^2) a 1), the stages are LogPartStageG (size j) 2 (S j) (T j), and the continuation is LogJointRecipeG (partSize (k^2) a 1) 2 Q. The degree $C$ is chosen after $e$ and before $k_0$; the reference family and all stage data are chosen after $k$.