Green-Class Mass and Naming Conservation

Abstract

Uniform Green mass and countable-name conservation share one product carrier.

Theorem 1.1 (Finite certificates retain mass while countable names remain null).

$$\begin{array}{c}\forall O:\mathrm{Type},\\ [\mathrm{Fintype}(O)],[\mathrm{Nonempty}(O)],[\mathrm{Nontrivial}(O)],\\ [\mathrm{MeasurableSpace}(O)],[\mathrm{MeasurableSingletonClass}(O)],\\ [\mathrm{TopologicalSpace}(O)],[\mathrm{DiscreteTopology}(O)],\\ \forall S:\mathrm{Finset}\left(\mathbb{N}\right),t:\mathbb{N}\to O,\\ \mu :=\mathrm{stringMeasure}\left(O\right),\\ \forall J:\mathrm{Type},[\mathrm{Countable}(J)],\\ \forall systems:J\to \mathrm{NamingSystem}\left(\mathbb{N}\to O\right),\\ \mu (\mathrm{greenClass}\left(S,t\right))=\mathrm{inv}{\left(\mathrm{card}\left(O\right)\right)}^{\mathrm{card}\left(S\right)}\wedge \\ 0<\mu (\mathrm{greenClass}\left(S,t\right))\wedge \\ \mathrm{Countable}\left(\mathrm{iUnion}\left(\Lambda j\mapsto \mathrm{named}\left(\mathrm{systems}\left(j\right)\right)\right)\right)\wedge \\ \mu (\mathrm{iUnion}\left(\Lambda j\mapsto \mathrm{named}\left(\mathrm{systems}\left(j\right)\right)\right))=0\wedge \\ \mu (\mathrm{iUnion}{\left(\Lambda j\mapsto \mathrm{named}\left(\mathrm{systems}\left(j\right)\right)\right)}^c)=1\wedge \\ \forall j:J,Q:\mathbb{N},\mu ({\left\{\exists a:\mathrm{Name}\left(\mathrm{systems}\left(j\right)\right),a\in \mathrm{layer}\left(\mathrm{systems}\left(j\right),Q\right)\wedge \mathrm{assignment}\left(\mathrm{systems}\left(j\right),a\right)=\mathrm{some}\left(x\right)\mid x\in \mathbb{N}\to O\right\}}^c)=1.\end{array}$$

Proof. Machine-checked in Lean as D5/S0/Naming/Conservation/GreenClassNamingConservation.green_class_naming_conservation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let O be a finite nontrivial discrete measurable alphabet and equip the sequence space N -> O with the canonical uniform product probability measure stringMeasure O. A finite support S and target t determine the canonical greenClass S t.

The green class has mass exactly (card O)^(-1) raised to card S and that mass is positive. Thus the value depends on the certificate budget and not on the pinned content.

For every countably indexed family of canonical NamingSystem values, the union of named images is countable and null, while its complement has measure one. For every system and every height budget, the complement of the corresponding finite layer image also has measure one.

The exact cylinder calculation and positivity are supplied by the frozen GreenClassMeasure declarations. The frozen NamingTowerConservation declaration supplies countability, nullity, and full-measure complement. Atomlessness of the same product measure follows from the imported critical-diameter estimate; probability normalization then also proves the sequence carrier uncountable.

References

• Truth anchor: D5/S0/Naming/Conservation/GreenClassNamingConservation.green_class_naming_conservation
• Dependency: D5/S0/Asymptotics/MetricGeometry/GreenClassHausdorffDimension
• Dependency: D5/S0/Naming/Conservation/NamingTowerConservation
• Dependency: D5/S0/Naming/GreenClassMeasure