# GameTheoryComplexity

This separate Lake package connects selected ComplexityLib machine definitions
to GameTheory probability and sample-test semantics. The base GameTheory package
does not depend on this package, ComplexityLib, or CSLib. Clients needing only
ordinary game theory do not resolve or download these dependencies.

The first integration provides finite fair-coin random tapes, their exact
counting interpretation, canonically encoded Boolean sample tests with certified
polynomial input length and machine execution, and equivalence
between the two libraries' negligibility predicates. It does not establish
efficient sampling of arbitrary real-valued utilities, efficient game deviations,
cryptographic primitives, or complexity bounds for arbitrary Lean definitions.
The canonical serializer also has a deterministic polynomial-time machine
certificate, with exact output correctness and tuple decoding included in the
cost. Its encoded input length and runtime are polynomial in the unary security
parameter. A composed probabilistic machine implements serialization plus
testing with exactly the same verdict law, one fixed machine, and a polynomial
clock independent of the samples. FP preprocessing is certified rather than
inferred from output length. A user-supplied encoder is never
classified as efficient merely because its result has polynomial length.

The payoff-constrained Nash slice certifies SAT reduction to explicit symmetric
integer payoff tables and proves NP-completeness of mixed Nash existence with both
payoffs at least one. The writer has an actual fixed polynomial-time machine
certificate and exact agreement with the table decoder. Base game semantics,
the satisfiability characterization and serialization remain dependency-free.
Membership uses bounded rational witnesses and a polynomial-time binary verifier
for the same total decoder and canonical Nash predicate. Import
`GameTheoryComplexity.Backend.NashNPComplete` for the headline theorem,
`Backend.NashNP` for membership alone, or `Backend.SATReduction` for hardness
alone. General Nash search and fixed-point results use separate relations and
imports described below; FIXP results remain separate work.

Import `GameTheoryComplexity.BimatrixNash` for general rectangular games with
two independently signed integer payoff matrices. The binary certificate
verifier has an actual polynomial-time machine and proves FNP membership.
Unary dimension and coefficient-width headers bound the scans; payoff and
certificate magnitudes are binary. Accepted certificates give ordinary PMF
mixed Nash equilibria, and equilibrium existence is equivalent to existence
of an exactly serialized bounded certificate. Malformed instances accept only the empty
answer, and malformed outer pairs are rejected. Bit-recursive multiplication
and canonical paired-verifier composition are separate game-free modules.
Serialized totality, TFNP and general Nash PPAD membership are proved through
finite complementary paths and actual polynomial-time pointer and answer
machines. Analytic existence remains confined to the base `Analysis` root.

Import `GameTheoryComplexity.Backend.EndOfLineVerifier` for a total circuit-encoded
End-of-Line
endpoint relation in TFNP and its actual polynomial-time verifier.
`Backend.SearchReduction` provides certified instance maps and decoders preserving
every target solution. The generic finite endpoint theorem lives independently in
the base `GameTheory.Math.EndOfLine` module. This slice uses mutually consistent
edges. Import `GameTheoryComplexity.PPAD` for the standard asymmetric raw
End-of-Line relation, PPAD membership and closure, and a certified reduction
showing consistent-edge endpoint search is PPAD-complete. Raw End-of-Line is complete
by definition of the class. Uniformly generated normalized circuit instances
give the reverse reduction with an actual FP instance map and every-answer decoder;
Signed rectangular Nash PPAD-completeness is supplied by `GameTheoryComplexity.BimatrixNash`.

`Backend.CircuitPrefixCompiler` provides an actual polynomial-time serialized
prefix restriction component. It preserves exact optional evaluation on all
source codes at positive live width, rejects malformed syntax and guards empty
outputs. `Backend.UniformCircuitSpecialization` joins this compiler to actual
uniform generation; `Backend.CircuitVectorEmission` serializes the output coordinates
in polynomial time. `Backend.EndOfLineCircuitGeneration` specializes normalized
pointer computations and preserves the invalid-source fallback.

`Backend.GridRoutingWords` encodes the endpoint-preserving planar routed graph
using two coordinate fields, totaling `4*b+6` bits for `2^b` original vertices.
Reciprocal pointers, known sources and every-endpoint recovery are proved;
malformed words remain isolated. `Backend.GridRoutingCodecMachine` certifies
acceptance and field extraction in FP, and `Backend.GridRoutingDivision` supplies
actual bitwise FP division by 3 and 6 and remainder modulo 3.
`Backend.GridRoutingEndpointMachine` gives a uniform FP decoder returning the
canonical original vertex label.
`Backend.GridRoutingGeometryMachine`, `GridRoutingGuards`, `GridRoutingQueries`,
`GridRoutingCrossingMachine` and `GridRoutingWireMachine` supply certified local
components for that pointer: exact route geometry, rectangle rejection,
guarded seeded original queries, proper-crossing validation and both individual
wire steps. Oversized candidate labels retain their value and remain isolated.
`Backend.GridRoutingDecoderMachine` certifies the six-candidate mathematical
decoder, using an explicit found flag to distinguish failure from vertex zero.
`Backend.GridRoutingNodeStepMachine` certifies guarded vertex/interior steps.
`Backend.GridRoutingPointerMachine` composes these with crossing switches and
coordinate encoding into complete uniform FP predecessor/successor machines.
Their agreement with the mathematical word pointers holds on every input word,
including malformed and background inputs.

Import `GameTheoryComplexity.Sperner` for
`spernerRelation_PPADComplete`: succinct canonical square-grid Sperner search is
complete for standard PPAD. The reverse reduction uses an actual uniform FP
coloring machine and circuit instance generator; its FPn decoder divides the
triangle row by 36 and recovers every non-source original endpoint, including
endpoints on disconnected components. Source entrance tiles and inactive
two-color padding exclude the known source and spurious outer-boundary answers.
Invalid source promises decode to the required empty witness. Continuous Brouwer
search completeness is described below; signed rectangular Nash search completeness is described below.

## Use as a dependency

In a downstream `lakefile.lean`, select a published commit containing this
extension (the placeholder below must be replaced with that commit):

```lean
require GameTheoryComplexity from git
  "https://github.com/elazarg/GameTheory" @ "<extension-commit>" / "extensions/complexity"
```

Import only the modules needed by the client:

```lean
import GameTheoryComplexity.SampleTest
-- The umbrella contains the random-sample integration surface.
-- Import this leaf separately for payoff-constrained Nash NP-completeness:
import GameTheoryComplexity.Backend.NashNPComplete
```

The default dependency configuration fetches the base GameTheory commit
`c7cd6bed7498b9a16edb22262e9522ceff90648c`; it does not assume a sibling checkout.
The resolved packages share Lean/Mathlib 4.35.0. ComplexityLib is pinned directly
to upstream `SamuelSchlesinger/complexitylib@257ad90ec5f547894cc20f27bd828839b1bf7bbf`,
and CSLib to `94ea80f41a5678fce997a004f0d8d12dbe47cc4b`. Their declared upstream
toolchains are 4.35.0 release candidates. Compatibility claims cover only the
dependency closure of this extension's selected imports. They do not cover
upstream umbrella modules,
unrelated theorem families, or CSLib interoperability.
The earlier fork's Cook–Levin proof repair is unnecessary on Lean 4.35.0;
the upstream proof compiles unchanged. The original integration is recorded in
EXP-159 in the repository's experiment log. Third-party diagnostics are allowed;
first-party diagnostics and transitive nonstandard axioms remain audit failures.

Import modules use the disjoint prefix `GameTheoryComplexity` because the base
package owns every `GameTheory.*` module through its default Lake globs.
Declarations keep the public namespace `GameTheory.Complexity`. Ordinary clients
use the small `SampleTest` facade; machine-specific builders live under
`GameTheoryComplexity.Backend.Complexitylib`, and the negligibility equivalence
under `GameTheoryComplexity.Backend.Negligible`. The serializer machine
certificate lives in `GameTheoryComplexity.Backend.Serializer`. Composition and
its canonical sample-test specialization live in `Backend.Composition` and
`Backend.CompiledSampleTest`, respectively. This separates backend details
without introducing a general machine-interface framework. Swapping a backend
still requires proofs that its implementation satisfies the facade contract.

## Work in this repository

Run these commands from `extensions/complexity`. Quote the configuration option
in PowerShell so `../..` is passed to Lake intact:

```text
lake -R '-KgameTheoryPath=../..' update
lake '-KgameTheoryPath=../..' env lean --version
lake '-KgameTheoryPath=../..' exe cache get
python ../../scripts/audit.py --complexity
```

The extension's generated manifest is ignored because local development replaces
the released base pin with a path. Run `lake -R update` after switching between
local and released modes. Source dependencies remain explicitly pinned; never
edit either package's manifest by hand.

The audit rejects warnings and info in every extension module's stored build
diagnostics, including cached results. Dependency warnings also fail; upstream
proof suggestions are allowed. CI runs the same audit against both the local
checkout and the released base pin.

The extension has its own CI workflow. Its default build targets only its own
library and fixtures, together with their imported dependencies. It never builds
the broad ComplexityLib umbrella target. The boundary audit checks that base
modules cannot import the optional surface and that resolved Mathlib revisions
are identical. The axiom audit checks every extension declaration's transitive
axioms, rejecting placeholders and all axioms except `propext`,
`Classical.choice`, and `Quot.sound`.


Import `GameTheoryComplexity.Backend.SpernerGridWords` for binary encoding of
the local Sperner graph, source promises and every-endpoint decoding. Import
`Backend.SpernerGridCodecMachine` and `Backend.SpernerBinarySteps` for actual
FP certificates for codec fields, exact acceptance and fixed-width arithmetic.
Import `Backend.SpernerPointerMachine` for the composed pointer, its actual
uniform FP certificate, source promises and endpoint decoding. Import
`GameTheoryComplexity.Sperner` for succinct Sperner PPAD-completeness, TFNP
totality and the independently verified trichromatic-triangle relation.
`Backend.SpernerReduction` and `Backend.EndOfLineSpernerReduction` supply both
actual FP circuit-instance maps and FPn every-answer decoders.

Import `GameTheoryComplexity.Brouwer` for continuous approximate fixed-point
search PPAD-completeness. A serialized color circuit specifies a piecewise
affine continuous self-map of the real unit square. With grid side `n = 2^b`,
an answer is any bounded point `(X/(6n), Y/(6n))` whose actual coordinate
residuals are at most `1/(6n)`; answers need not be triangle barycenters.
`Backend.BrouwerVerifier` provides independent FNP membership and an actual
polynomial-time verifier. `Backend.BrouwerReduction` supplies the certified
reductions to and from succinct Sperner. The map continuity, square
preservation and exact rational residual semantics are base mathematics and
require no ComplexityLib. The theorem concerns this circuit-induced map
family and output precision, rather than arbitrary continuous-map encodings,
distance to an exact fixed point or FIXP.

Import `GameTheoryComplexity.BimatrixNash` for exact signed rectangular Nash
search PPAD-completeness (`bimatrixNashRelation_PPADComplete`). The existing binary relation
has an actual FP instance map to End-of-Line and an FPn decoder preserving
every target answer. Full lexicographic perturbations handle degenerate games;
malformed inputs retain the empty answer. The decoder computes the supplied
endpoint's certificate and undoes payoff shifts. Hardness uses an actual FP
Brouwer-to-game instance map and FPn decoder. The canonical sampled program's
coefficient/kind machines agree at every output, and its emitted reward proves
that every accepted Nash certificate yields an accepted Brouwer answer.
`bimatrixNashRelation_PPADHard` and the existing membership theorem classify the
same binary relation. Ordinary base clients continue to require no ComplexityLib.