Keyboard shortcuts

Press or to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Golden Tower Clause Two Erratum Package

Abstract

The golden tower clause carries its sixteen proved sentences together with explicit refutations of the three that are false as stated.

Sixteen source sentences are discharged by their frozen theorems. Three further source sentences are false: the unrestricted supremum claim, its corollary for arbitrary x, and the assertion that the closed permanent set is the four point ring. Those three appear in the package as explicit refutations rather than silent replacements, and the strict-side emptiness that stands in place of the third is conjoined beside them.

Theorem 1.1 (The golden clause with its errata).

Proof. Machine-checked in Lean as D5/S0/Tower/GoldenClauseTwo/ErrataPackage.golden_clause_two_errata_package (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed identity is the champion value the ring attains. The package itself is the conjunction of that identity with the remaining fifteen proved sentences and the three refutations.

References