ProofOfTheInsulatorLemmas

The full context of ProofOfTheInsulatorLemmas is explained in [Homotopy Hyperbolic 3-Manifolds are Hyperbolic], as ProofOfTheInsulatorLemmas is actually the proof of two crucial computer-verified results used there. People equipped with the specialized knowledge of GeometricTopology to fully understand this context are likely already familiar with the result; what follows is an explanation for other readers.

The problem is to prove that a particular property applies to most points within a compact region of a space with six real dimensions. The basic technique used a RegularBinarySpacePartition to divide this region into about 500,000,000 sub-regions, and to prove that this property applied to each of those sub-regions.

The property could be stated:

There exists a WordOfSymbols $w$ for which the inequality associated with $w$ is satisfied for each point in the sub-region.

The proof consists of the pre-order traversal of the WikiPedia:Binary_tree associated with RegularBinarySpacePartition, and each leaf node of this tree consists of the WordOfSymbols required to prove the property, or an indication that the property hasn't been proved for this sub-region. Verification of this proof is done by the process of simultaneously traversing the binary tree and the RegularBinarySpacePartition, checking at each leaf node of the binary tree that the inequality is in fact satisfied.

The entire proof can itself be thought of as a very long WordOfSymbols, in a language whose symbols include:

• The original symbols
• INTERNAL_NODE
• LEAF_NODE
• [Hospedagem de Sites]
• [Hospedagem]
• [Servidor Dedicado]

ComputerAssistedProofFindingAlgorithm contains a description of the algorithmic procedure used to find ProofOfTheInsulatorLemmas.