Testing Tower Structure Membership

Abstract

The testing tower satisfies its carrier, valuation, and two-height classification clauses.

Lemma 1.1 (The testing tower is a multi-filtration naming system).

$$\begin{gathered} \begin{array}{c}\forall O:\mathrm{Type},\\ [\mathrm{Finite}\left(O\right)],[\mathrm{Nontrivial}\left(O\right)],\\ [\mathrm{TopologicalSpace}\left(\mathbb{N}\to O\right)],[\mathrm{PolishSpace}\left(\mathbb{N}\to O\right)],\\ [\mathrm{MeasurableSpace}\left(\mathbb{N}\to O\right)],[\mathrm{BorelSpace}\left(\mathbb{N}\to O\right)],\\ [\mathrm{Uncountable}\left(\mathbb{N}\to O\right)],\\ \forall o0:O,decode:\mathbb{N}\to \left(\mathbb{N}\to O\right),\\ input:\mathbb{N},\\ code:\mathrm{TestingName}\left(O\right)\to \mathrm{List}\left(Bool\right),programCost:\mathbb{N}\to \mathbb{N},\\ \mu :\mathrm{Measure}\left(\mathbb{N}\to O\right),\\ [\mathrm{NullSingletonClass}\left(\mu \right)],[\mathrm{SigmaFinite}\left(\mu \right)],\\ \mathrm{Injective}\left(code\right)\Rightarrow \mathrm{withMeasureSpace}\left(\mu ,(\mathrm{Countable}\left(\mathrm{TestingName}\left(O\right)\right)\wedge \\ (\forall p:\mathbb{N},\mathrm{isSome}\left(\mathrm{testingAssignment}\left(o0,decode,input,\mathrm{inr}\left(p\right)\right)\right)⟺\mathrm{Dom}\left(\mathrm{eval}\left(\mathrm{ofNatCode}\left(p\right),input\right)\right))\wedge \\ \neg \mathrm{ComputablePred}\left((c:PartrecCode\mapsto \mathrm{isSome}\left(\mathrm{testingAssignment}\left(o0,decode,input,\mathrm{inr}\left(\mathrm{encodeCode}\left(c\right)\right)\right)\right))\right)\wedge \\ (\forall Q:\mathbb{N},\mathrm{Finite}\left(\left\{\mathrm{length}\left(\mathrm{code}\left(a\right)\right)\le Q\mid a\in \mathrm{TestingName}\left(O\right)\right\}\right))\wedge \\ \mathrm{Infinite}\left(\left\{\mathrm{testingExecutionCost}\left(programCost,a\right)\le 1\mid a\in \mathrm{TestingName}\left(O\right)\right\}\right)\wedge \\ (\forall Q:\mathbb{N},\mathrm{Finite}\left(\left\{\mathrm{length}\left(\mathrm{code}\left(a\right)\right)+\mathrm{natLog}\left(2,\mathrm{testingExecutionCost}\left(programCost,a\right)\right)\le Q\mid a\in \mathrm{TestingName}\left(O\right)\right\}\right))\wedge \\ \mu \left(\mathrm{named}\left(\mathrm{primary}\left(\mathrm{testingTower}\left(o0,decode,input,code,programCost,\mu \right)\right)\right)\right)=0)\right).\end{array} \end{gathered}$$

Proof. Machine-checked in Lean as D5/S0/Naming/TestingTowerStructureMembership.testing_tower_has_multi_filtration_membership (✓ std3). ∎

Source. Repository-derived.

Commentary.

The carrier is the sequence space over a finite nontrivial output type, with its Polish and Borel structures and an explicitly supplied atomless sigma-finite measure.

The constructed assignment retains the default table extension. The public clauses expose countability of the exact TestingName carrier, the noncomputable halting domain of program names, finite description-length sublevels, an infinite execution-cost sublevel, finite mixed-cost sublevels, and the null named image.

The constructed tower wraps NamingSystem as its primary coordinate and uses the execution-cost model as its secondary coordinate. The proof applies the three standalone prerequisites and the frozen dark-side conservation owner.

References

• Truth anchor: D5/S0/Naming/TestingTowerStructureMembership.testing_tower_has_multi_filtration_membership
• Dependency: D5/S0/Naming/MultiFiltrationNamingSystem
• Dependency: D5/S0/Naming/TestingCostClassification
• Dependency: D5/S0/Naming/TestingTowerValuation