Budget and First-Gap Geometry of Green Classes

Abstract

Uniform Green-class volume depends only on budget, while exact drift depends on the first gap.

Theorem 1.1 (Budget controls volume while the first hole controls drift).

$$\begin{array}{c}\forall O:\mathrm{Type},\\ \mathrm{Fintype}(O)\wedge \mathrm{Nonempty}(O)\wedge \mathrm{MeasurableSpace}(O)\wedge \mathrm{MeasurableSingletonClass}(O)\wedge \\ \mathrm{TopologicalSpace}(O)\wedge \mathrm{DiscreteTopology}(O)\wedge \mathrm{Nontrivial}(O)\Rightarrow \\ \forall S:\mathrm{Finset}(\mathbb{N}),t:\mathbb{N}\to O,\\ \mathrm{stringMeasure}(O,G(S,t))=(\mathrm{card}(O{)}^{-1}{)}^{\mathrm{card}(S)}\wedge \\ (\forall U:\mathrm{Finset}(\mathbb{N}),\mathrm{card}(U)=\mathrm{card}(S)\Rightarrow \mathrm{stringMeasure}(O,G(U,t))=\mathrm{stringMeasure}(O,G(S,t)))\wedge \\ \mathrm{diam}(G(S,t))={\frac{1}{2}}^{\mathrm{firstHole}(S)}\wedge \\ ({\frac{1}{2}}^{\mathrm{card}(S)}\le \mathrm{diam}(G(S,t))\wedge (\mathrm{diam}(G(S,t))={\frac{1}{2}}^{\mathrm{card}(S)}⟺S=\mathrm{range}(\mathrm{card}(S)))).\end{array}$$

Proof. Machine-checked in Lean as D5/S0/Asymptotics/MetricGeometry/GreenClassBudgetGeometry.green_class_budget_geometry (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let O be a finite nonempty nontrivial alphabet carrying the measurable discrete structure used by the uniform product law and the PiNat prefix metric. For a finite support S and target t, the Green class G(S,t) consists of all infinite strings agreeing with t on S.

Its uniform product measure is (card O)^(-1) raised to card S. Hence replacing S by any support U of the same cardinality leaves the volume unchanged: the regression budget sees how many coordinates were tested, not where they lie.

Its prefix-metric diameter is exactly (1/2)^firstHole(S), so the least untested coordinate fixes the full drift radius regardless of tests placed later. At fixed budget, (1/2)^card(S) is the smallest possible diameter, and equality holds exactly when S is the gapless prefix range(card(S)).

The proof applies the frozen canonical Green-class measure, exact-diameter, and prefix-extremality theorems. It introduces no replacement Green class, measure, metric, or first-hole definition.

References

• Truth anchor: D5/S0/Asymptotics/MetricGeometry/GreenClassBudgetGeometry.green_class_budget_geometry
• Dependency: D5/S0/Asymptotics/MetricGeometry/GreenClassDiameter