Finite Actual Root Menu Minimax

Abstract

Executable attained chart and exact unit-call optimum on the actual three-reply menu.

The actual menu consists only of the classes occurring in the complete current row. The three replies are some true, some false, and none. The fourth native absent reply has no table row.

This natural-number executable optimizer supplies the effective part of Native Birth Provenance Corollary 10.9. It adds no physical-cost or performance claim. Finite normalization and Bellman methods are existing suppliers; the particular row-count-fueled construction and its attaining-tree theorem are the mathematical content here.

In the formula, rowType and rowTarget denote the TableRow projections; chart elements coerce to their assignments. The two Boolean implications express the exact constant versus nonconstant recurrence.

Definition 1.1 (Attained Type Checker).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.admissibleCode

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.admissibleCode (✓ std3).

Source. Repository-derived.

Commentary.

The Boolean image grammar and distinct-class leaf bounds decide precisely Admissible. The branch obligation remains in the retained native image-chart supplier.

Theorem 1.2 (Exact Boolean Admissibility).

$$\forall C:LiteralRow,(\forall theta:(\mathrm{Classes}\left(C\right))\to (\mathrm{Option}\left(Bool\right)),((\mathrm{admissibleCode}\left(C,theta\right)=true)⟺(\mathrm{Admissible}\left(C,theta\right))))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.admissibleCode_spec (✓ std3). ∎

Source. Repository-derived.

Commentary.

The public equivalence connects the executable checker to the original admissibility predicate for every literal row and every class-root assignment. It is reused by the actual repeated-partner controllers.

Definition 1.3 (Finite Chart Enumeration).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.chartList

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.chartList (✓ std3).

Source. Repository-derived.

Commentary.

List.pi enumerates the three replies at every appearing class and filters by admissibleCode. Completeness includes zero classes. No actual origin, source-size bound, or native-word bound is a data argument.

Definition 1.4 (Entire Predecessor Target).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.computedTarget

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.computedTarget (✓ std3).

Source. Repository-derived.

Commentary.

The computable mask tests each occurrence parent for the visible alpha sibling and calls NativePredecessorRowRecovery.back. Shared old and new occurrences are repaired individually, including the root and blocked cuts.

Definition 1.5 (Executable Unit-Call Value).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.minimaxValue

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.minimaxValue (✓ std3).

Source. Repository-derived.

Commentary.

Row-count fuel suffices: every nonempty reply fiber of a splitting coordinate is strictly smaller. A constant target costs zero. Otherwise List.argmin selects the actual class coordinate with one plus the maximum child value. Empty reply cells contribute zero.

Definition 1.6 (Particular Attaining Tree).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.minimaxTree

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.minimaxTree (✓ std3).

Source. Repository-derived.

Commentary.

The tree follows the same argmin and three reply cells as minimaxValue. Constant tables stop at their common complete target. Empty and impossible branches stop at the supplied fallback.

Theorem 1.7 (Exact Recurrence and Finite Chart Bound).

$$\forall C:LiteralRow,(\forall W:\mathrm{List}\left(\mathrm{TableRow}\left(C\right)\right),((((\mathrm{constantTarget}\left(W\right)=true)⟹(\mathrm{minimaxValue}\left(C,W\right)=0))\wedge ((\mathrm{constantTarget}\left(W\right)=false)⟹(\mathrm{minimaxValue}\left(C,W\right)=\mathrm{scoreMinimum}\left(C,W,\mathrm{minimaxValue}\left(C\right)\right))))\wedge (\forall fallback:LiteralRow,((\forall a:\mathrm{TableRow}\left(C\right),((\mathrm{member}\left(a,W\right))⟹(\mathrm{fst}\left(\mathrm{rootRun}\left(\mathrm{rowType}\left(a\right),\mathrm{minimaxTree}\left(C,fallback,W\right)\right)\right)=\mathrm{rowTarget}\left(a\right))))\wedge (\mathrm{rootDepth}\left(\mathrm{minimaxTree}\left(C,fallback,W\right)\right)=\mathrm{minimaxValue}\left(C,W\right))))\wedge (\forall T:\mathrm{RootTree}\left(C,LiteralRow\right),((\forall a:\mathrm{TableRow}\left(C\right),((\mathrm{member}\left(a,W\right))⟹(\mathrm{fst}\left(\mathrm{rootRun}\left(\mathrm{rowType}\left(a\right),T\right)\right)=\mathrm{rowTarget}\left(a\right))))⟹(\mathrm{minimaxValue}\left(C,W\right)\le \mathrm{rootDepth}\left(T\right))))\wedge (\mathrm{length}\left(\mathrm{chartList}\left(C\right)\right)\le \mathrm{pow}\left(3,\mathrm{card}\left(\mathrm{Classes}\left(C\right)\right)\right))\wedge (\forall theta:\mathrm{Chart}\left(C\right),(\mathrm{member}\left(theta,\mathrm{chartList}\left(C\right)\right)))\wedge (\forall theta:(\mathrm{Classes}\left(C\right))\to (\mathrm{Option}\left(Bool\right)),(\mathrm{computedTarget}\left(C,theta\right)=\mathrm{target}\left(C,theta\right)))))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.finite_root_minimax (✓ std3). ∎

Source. Repository-derived.

Commentary.

The retained result combines the constant-target or splitting-menu recurrence, attaining tree, all-competitor lower bound, chart length at most 3 raised to the number of occurring classes, exact semantic chart completeness, and computed-target agreement.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.admissibleCode
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.admissibleCode_spec
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.chartList
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.computedTarget
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.finite_root_minimax
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.minimaxTree
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteRootMinimax.minimaxValue
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/NativeFullRootFeasibility