ComplexityPair
plain-language theorem explainer
ComplexityPair introduces a record type pairing two functions Tc and Tr, each from natural numbers to natural numbers, to represent time costs for covering and reduction steps on vertex-cover instances. Researchers formalizing NP-completeness or approximation algorithms would reference this structure when typing concrete instances or proving cover properties. The declaration is a direct structure definition with no proof obligations or additional constraints.
Claim. A complexity pair consists of two functions $T_c : ℕ → ℕ$ and $T_r : ℕ → ℕ$ that assign natural-number time costs to input sizes.
background
The VertexCover module models vertex-cover decision problems over natural-number vertices and imports only Mathlib for basic types. ComplexityPair supplies the minimal record needed to attach time functions to an instance size n. No upstream lemmas are referenced; the structure stands alone as the entry point for later definitions such as trivialInstance and HasCover.
proof idea
The declaration is a bare structure definition that directly introduces the two fields Tc and Tr with no tactics, lemmas, or reduction steps required.
why it matters
This definition supplies the basic type for attaching time measures to vertex-cover instances inside the module. It enables the sibling constructions of trivial instances and cover predicates that appear later in the same file. Within the broader Recognition Science monolith it provides a discrete-complexity interface, though it remains disconnected from the forcing chain or phi-ladder machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.