A kernel-checked Lean bridge connects OpenAI's subexponential bounded-width SAT theorem, applied at width 3 to the negation of ParityLifts' PositiveRateETH predicate. The bridge formalizes the SAT encoding conversion, machine simulation, polynomial overhead, and exponential-rate comparison.
theorem OAI.Bridges.ETH.not_positiveRateETH :
¬ OAI.ParityWL.Complexity.PositiveRateETHVerified on the VPS at proof commit 81ec97cd2. The final theorem has no additional premises. Its axiom audit reports propext, Classical.choice, and Quot.sound.
Each reading point has a separate role: source theorem, formal specification, and proved result. Identifiers below are provisional pending registration in the RPI catalog.
SqrtLogSpace.original_sat_main : SqrtLog.Statement.MainTheorem
For every width k ≥ 3, a fixed deterministic machine and width-dependent constants decide bounded-width CNF with a subexponential variable-count factor and polynomial encoding-length factor. OpenAI's Comparator checks exact_count_and_sat; original_sat_main is derived from it and kernel-checked in the final build.
OAI.ParityWL.Complexity.PositiveRateETH
A formal assertion that some positive exponential rate excludes all deterministic multitape 3-SAT deciders within the specified polynomial-times-exponential bound.
Inspect definitionOAI.Bridges.ETH.not_positiveRateETH
A verified implication applies OpenAI's SAT result to the ParityLifts formalization, constructing the required decider through a polynomial-overhead conversion and simulation.
Inspect final proofencodeCNF (canonicalWord_eq). Conversion time is polynomial in the variable bound N (canonicalWordProgram_time_poly).FCode runner and prove polynomial resource overhead, yielding simulationHypothesis_proved.2^(A · runtimeScale N) by an arbitrarily small positive exponential rate (runtimeFactor_expBound); incorporate polynomial converter and simulator costs using sat_code_rate, and refute PositiveRateETH with original_sat_main.original_sat_main → not_positiveRateETH_of_mainTheorem → ¬ PositiveRateETHLEAN_NUM_THREADS=2 lake build OAI.Bridges.ETH.FinalImplicationFinal axiom audit: [propext, Classical.choice, Quot.sound]. Verified proof snapshot: 81ec97cd23d21675cee4ee76768fffba33a61e17. Documentation commit: 81708f93f.
The kernel-checked conclusion is the negation of the specifically defined ParityLifts predicate PositiveRateETH. That predicate quantifies over deterministic finite-alphabet multitape machines deciding 3-SAT on ParityLifts' binary formula encoding, with a polynomial input-length factor and a positive exponential variable-count rate.
Comparison with standard textbook ETH is a separate semantic-fidelity review of the machine model, encoding, and quantifiers. The final statement’s meaning is fixed by the ParityLifts definitions; OpenAI’s MainTheorem enters as a kernel-checked proof term. OpenAI’s original paper and its precise Lean theorem have distinct complexity bounds; the bridge uses the Lean theorem.
Review focus: exact definition unfolding; machine and encoding faithfulness; quantifier order; rate preservation; and independent reproduction of the final kernel check.