A verified negation of PositiveRateETH

Reading points

Each original reading point has a separate role: source theorem, formal specification, and proved result. The A/B/C labels are historical identifiers for this page; the ETH registry now records the cross-formalization implication as RPI-ETH-010.

The checked proof chain

1. Encoding correspondence. Convert ParityLifts' normalized 3-CNF inputs to OpenAI's exact canonical CNF bit encoding, preserving satisfiability, keeping the variable count bounded, and proving bit-for-bit equality with OpenAI’s encodeCNF (canonicalWord_eq). Conversion time is polynomial in the variable bound N (canonicalWordProgram_time_poly).
2. Machine translation. Represent OpenAI's primitive multitape machine in ParityLifts' finite-alphabet machine model with step-level correspondence.
3. Executable simulation. Construct a fixed ParityLifts FCode runner and prove polynomial resource overhead, yielding simulationHypothesis_proved.
4. Rate comparison. Bound OpenAI’s subexponential factor 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.

From OpenAI’s ETH predicate to Anthropic’s

A second, independent Lean bridge proves an unconditional implication between the two projects’ formal ETH statements. Its proof uses explicit encoding conversion and machine simulation; it does not depend on OpenAI’s SAT proof or Anthropic’s existing proof of ETHIsFalse.

theorem OAI.Bridges.AnthropicETH.not_positiveRateETH_implies_ethIsFalse :
  ¬ OAI.ParityWL.Complexity.PositiveRateETH → MainResults.ETHIsFalse

1. FinTM2 simulation (H1). Simulate a ParityLifts multitape machine in Mathlib’s stack-machine model, with the required halting configuration and time bound 4 * (x.length + s + 1).
2. Encoding converter (H2). A verified polynomial-time PolyProgram converts Anthropic’s encClauses 3 φ exactly to ParityLifts’ encodeFormula (toFormula φ), with a uniform degree.
3. Quantifier and rate transfer. Clause-count and encoding-length bounds absorb polynomial overhead into arbitrarily small positive exponential rates, yielding MainResults.ETHIsFalse.

The dependency guard excludes forbidden proof constants and out-of-scope OpenAI modules. The final theorem’s only reported axioms are [propext, Classical.choice, Quot.sound]. VPS Comparator reported “Lean default kernel accepts the solution” and “Your solution is okay!” with nanoda disabled. A separate standalone nanoda replay was accepted in the local harness, not on the VPS.

Independent VPS verification

Final axiom audit: [propext, Classical.choice, Quot.sound]. Verified proof snapshot: 81ec97cd23d21675cee4ee76768fffba33a61e17. Documentation commit: 81708f93f.

What the results establish

The first 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.

The additional RPI-ETH-010 theorem proves that this negation implies Anthropic’s formal predicate MainResults.ETHIsFalse. Together they provide a checked route to that Anthropic statement, while the cross-formalization proof itself does not import either project’s existing SAT/ETH proof.

These results connect formal definitions; they do not yet establish a two-way equivalence with standard textbook ETH. The converse remains open in this project. OpenAI’s original paper and its precise Lean theorem have distinct complexity bounds; the first 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 checks.