Dominance Precision Interval

Abstract

Complete dominance occupies exactly the half-open band between the two pairwise reveal thresholds.

Theorem 1.1 (Complete dominance is an interval of precision levels).

$$\begin{array}{r}\forall X:\mathrm{Type},O:\mathbb{N}\to \mathrm{Type},\\ q:\forall k:\mathbb{N},X\to O_k,\\ rho:\forall k:\mathbb{N},O_{k+1}\to O_k,\\ x_{AA},x_{AB},x_{BB}:X,\\ (\forall k:\mathbb{N},q_k=rh{o}_k\circ q_{k+1})\Rightarrow \\ \mathrm{let}{r}_1:=\mathrm{revealThreshold}\left(O,q,x_{AA},x_{AB}\right),\\ r_2:=\mathrm{revealThreshold}\left(O,q,x_{AB},x_{BB}\right),\\ d(k):=(q_k(x_{AA})=q_k(x_{AB})\wedge q_k(x_{AB})\ne q_k(x_{BB})),\\ D:=\{v\in \mathrm{WithTop}\left(\mathbb{N}\right)\mid \exists k\in \mathbb{N},v=k\wedge d(k)\},\\ D_{fin}:=\{k\in \mathbb{N}\mid d(k)\},\\ W_{dom}:=\mathrm{ncard}\left(D_{fin}\right)\mathrm{in}\\ (\forall k\in \mathbb{N},d(k)\iff r_2\le k\wedge k<r_1)\wedge \\ D=\mathrm{Ico}\left(r_2,r_1\right)\wedge \\ ((\exists k\in \mathbb{N},d(k))\iff r_2<r_1)\wedge \\ (\forall n_1,n_2\in \mathbb{N},r_1=n_1\wedge r_2=n_2\Rightarrow W_{dom}=n_1-n_2).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/RefinementGeometry/DominancePrecisionInterval.dominance_precision_interval (✓ std3). ∎

Source. Repository-derived.

Commentary.

The reveal threshold of a pair is constructed as its least separating precision, with infinity used exactly when no precision separates the pair. Compatibility of the lowering maps makes separation persistent above that threshold.

Complete dominance at level k is the simultaneous agreement of AA with AB and separation of AB from BB. Consequently its extended-natural levels are precisely the half-open interval from r2 to r1, and such a level exists exactly when r2 is strictly below r1.

The finite dominance width is constructed as the cardinality of the finite-level dominance band. When both reveal thresholds are finite, the natural interval cardinality theorem identifies it with n1 - n2.

References

• Truth anchor: D5/S3/ConceptDynamics/RefinementGeometry/DominancePrecisionInterval.dominance_precision_interval
• Dependency: D5/S3/ConceptDynamics/RefinementGeometry/PrecisionSeparationPersistence