Testing Tower Membership

Abstract

Finite tables and program codes admit a primary height with finite sublevels.

Definition 1.1 (Names are finite tables or program codes).

$$\forall O:\mathrm{Type},\mathrm{TestingName}\left(O\right)=\mathrm{Sum}\left({\sigma }_{S:\mathrm{Finset}\left(\mathbb{N}\right)}(S\to O),\mathbb{N}\right).$$

Formalization. D5/S0/Naming/Conservation/TestingTowerMembership.TestingName (✓ std3).

Source. Repository-derived.

Commentary.

A name is either a function on a self-selected finite support or a natural-number code for a program-based test.

Lemma 1.2 (Binary description length supplies the primary filtration).

$$\begin{array}{c}\forall O:\mathrm{Type},\\ \forall code:\mathrm{TestingName}\left(O\right)\to \mathrm{List}\left(Bool\right),\forall hC:\mathrm{TestingName}\left(O\right)\to \mathbb{N},\\ \mathrm{Injective}\left(code\right)\Rightarrow \exists i:Bool,\forall Q:\mathbb{N},\\ \mathrm{Finite}\left(\left\{\mathrm{ite}\left(i,\mathrm{hC}\left(a\right),\mathrm{length}\left(\mathrm{code}\left(a\right)\right)\right)\le Q\mid a\in \mathrm{TestingName}\left(O\right)\right\}\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

TestingName O is the disjoint sum of finite functional tables on self-selected finite supports and natural-number program codes. The theorem keeps this source carrier public rather than replacing it with a prepackaged naming-system witness.

An injective self-delimiting Boolean code is the algorithmic height, while execution cost is an arbitrary secondary height. Choosing the code coordinate reduces every bounded sublevel to the injective preimage of the finite set of Boolean lists of bounded length.

Repository body-shape searches found only the raw-program special case. Pinned Mathlib supplies List.finite_length_le, which is applied directly to establish the finite-level-set clause.

References

• Truth anchor: D5/S0/Naming/Conservation/TestingTowerMembership.TestingName
• Truth anchor: D5/S0/Naming/Conservation/TestingTowerMembership.testing_tower_is_multi_filtration