orbitStarSize_pos
plain-language theorem explainer
Geometric star size $r_\tau$ is strictly positive on every 4D hinge orbit type under coordinate permutation. Anyone building the distinct-hinge continuum fold weight $1/r_\tau$ cites this positivity. The proof is a pure case split on the six orbit labels, evaluating the fixed table $(1,1)\mapsto 6$, $(1,2)\mapsto 4$, etc.
Claim. For every lattice hinge orbit type $\tau$ under coordinate permutation, the geometric star size $r_\tau$ satisfies $0 < r_\tau$. Explicitly $r_{(1,1)}=6$, $r_{(1,2)}=4$, $r_{(2,1)}=4$, $r_{(1,3)}=6$, $r_{(3,1)}=6$, $r_{(2,2)}=4$.
background
This module builds the continuum-facing multi-orbit 4D Bloch fold: each slot transports its orbit seed area covector and star deficit kernel by the covering permutation of the orbit representative. The six orbit types are the lattice classes of hinges under coordinate permutation, labelled $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, $(2,2)$.
Geometric star size $r_\tau$ is the per-orbit integer weight from the star modules and paper table: six for the $(1,)$ and $(,1)$ classes that hit three spatial axes in the complementary pair, four for the mixed $(1,2)$, $(2,1)$, $(2,2)$ classes. Downstream continuum folds want a distinct-hinge sum with full-star deficit, which inserts the weight $1/r_\tau$ on each orbit contribution rather than a bare all-orbit fold or a fitted $2/r$.
Positivity of $r_\tau$ is the elementary arithmetic gate before one may form that reciprocal weight or assert $r_\tau\neq 0$.
proof idea
One-line wrapper: case-split on the inductive orbit-type label, then norm_num against the definition of star size. Each branch reduces to a concrete positive numeral (4 or 6), so the inequality $0<r_\tau$ holds by arithmetic. No external lemmas beyond the definition table and the inductive type of orbit labels.
why it matters
Feeds the immediate sibling orbitStarSize_ne_zero, which is the non-vanishing form used when writing the distinct-hinge continuum fold weight $1/r_\tau$. Module status lists that weight, together with axis/gauge $m^2$ evaluations, among the closed theorem content of the transported all-orbit fold; the open items (all-orbit $m^2$ Tendsto, continuum EH isotropy via residual $2/N^4$ cell-sum dictionary) sit downstream of having a well-defined positive reciprocal weight. Without positivity one cannot even state the distinct-hinge fold as a real scalar multiple of the orbit Bloch contribution. Does not itself touch gap-action recovery or the EH continuum limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.