WIP: Import Beyond Bethe permanent approximation

[Vilin97]

Imports the permanent-approximation development from nimaanari/formalization-beyond-bethe, pinned at 325cda6d2118870f7f121a9a986b7ea9ffdd7a26, together with the required Complexitylib closure pinned at b6738219a3a3c50967d6bd16cba9487887ca6b66.

The 708 destination Lean files retain the production stable-polynomial inequalities, rational optimization and arithmetic, Turing-machine implementation, and proved wrapper behind BeyondBethe.theoremOne. Five additional layout modules preserve their original declaration bodies and public imports. Original author and license notices remain; the dependency overview records its provenance.

The port is in progress. Please leave this PR unmerged while kernel and linter verification continue. No repository checks, settings, or budgets were weakened.

Validation at 2fe0c16b8:

• The unchanged scoped static checks report zero findings across all 708 files, including headers, forbidden constructs, file limits, and proof limits.
• The original missing-documentation inventory and 45 oversized-proof findings were addressed through documentation and semantic helper lemmas. Public theorem contracts were preserved; a textual signature audit covers the refactored files and explicit layout moves.
• The pre-module-migration project build passed all 4,288 jobs. The module migration and subsequent helper refactors still require a fresh kernel build and scoped declaration/style audits; the earlier successful build does not validate these later edits.
• Current main and concurrent maintainer edits were merged into the branch. Module paths were preserved. Validation will prebuild modules in dependency order under the shared resource limits, followed by the complete cached project target.

Scope exclusions preserve the maintainer edits in 7658458bd and 812cb8239. The upstream duplicate open challenge and these three unused executable test/smoke harnesses are outside the production proof graph. Their declarations are listed explicitly below; no production theorem dependency was removed.

BeyondBethe.MachineArithmeticTests — 31 test/helper declarations

• BeyondBethe.binaryLongDiv_exhaustive_256_by_64
• BeyondBethe.binaryEuclidBounded_exhaustive_128_by_128
• BeyondBethe.machineBinaryMul_exhaustive_64_by_64
• BeyondBethe.machineBinarySub_exhaustive_64_by_64
• BeyondBethe.machineBinaryCompare_exhaustive_64_by_64
• BeyondBethe.machineBinaryDivision_exhaustive_64_by_32
• BeyondBethe.machineBinaryGcd_exhaustive_32_by_32
• BeyondBethe.signedIntegerTest
• BeyondBethe.machineIntegerArithmetic_exhaustive_signed_16
• BeyondBethe.positiveRawRatTest
• BeyondBethe.negativeRawRatTest
• BeyondBethe.signedRawRatTest
• BeyondBethe.machineRationalNormalization_exhaustive_signed_8_by_8
• BeyondBethe.machineRationalArithmetic_exhaustive_signed_3
• BeyondBethe.machineRationalComparison_exhaustive_signed_4
• BeyondBethe.machineRationalUnary_exhaustive_signed_3
• BeyondBethe.machineDyadicFloor_exhaustive_signed_4
• BeyondBethe.machineRationalFloorCeil_exhaustive_signed_8
• BeyondBethe.machineRationalLogSeriesSum_exhaustive_signed_3
• BeyondBethe.machineBoundedUnary_exhaustive_8
• BeyondBethe.machineBoundedRationalExpLower_small_signed
• BeyondBethe.machineLengthBits_exhaustive_16
• BeyondBethe.positiveNonzeroRawRatTest
• BeyondBethe.machineDirectedLog_small_positive
• BeyondBethe.machineMatrixNonnegative_two_by_two
• BeyondBethe.machineMatrixSum_two_by_two_constant
• BeyondBethe.machineRationalMin_exhaustive_positive_3
• BeyondBethe.machineFactorial_exhaustive_8
• BeyondBethe.machineRationalRowAdd_exhaustive_2
• BeyondBethe.machineScheduledLogTermsRuler_three_halves
• BeyondBethe.machineNearbyCoordinate_one_third

BeyondBethe.MachineOptimizerTests — 8 test/helper declarations

• BeyondBethe.optimizerTestAffinePoint
• BeyondBethe.optimizerTestFloor
• BeyondBethe.machineBetheFloorViolation_exhaustive_two_by_two_quarters
• BeyondBethe.machineBetheFloorScan_exhaustive_two_by_two_quarters
• BeyondBethe.machineExecutableMatrixEntry_exhaustive_two_by_two_quarters
• BeyondBethe.machineExecutablePotentialEntries_two_by_two_half
• BeyondBethe.optimizerTestEntry
• BeyondBethe.machineMatchingGain_exhaustive_two_by_two_binary_entries

BeyondBethe.MachineRAMSmoke — 4 test/helper declarations

• BeyondBethe.emptyMachineTarget
• BeyondBethe.outputBitLanguage_emptyMachineTarget
• BeyondBethe.paddedOutputBitLanguage_emptyMachineTarget
• BeyondBethe.emptyMachineTarget_mem_FP_from_paddedRAM

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.

[Vilin97]

Changes requested by automated review

Reviewed exact head 33f57fab1d3bd464e1ac4a74b8cc8e478cb1d932. The exact-head BeyondBethe build emits a large warning set and fails the repository zero-warning gate, including flexible-simp and tactic/style warnings in the Turing-machine and permanent-approximation modules. The PR itself says warning cleanup and proof-size refactoring remain pending. Complete those repairs and full quality/trust validation before merge.

[Vilin97]

/review

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low risk] Adds mathematical proof library files for permanent approximation.

No new blocking issue was established, but the current head should remain unmerged until its stated kernel and linter verification is complete.

Findings

1.  Executable regression checks deleted ▶

Summary

Imports the Beyond Bethe permanent-approximation formalization and its Complexitylib dependencies into Lean Pool.

• The latest change replaces two Boolean-matrix proof tactics without changing their theorem statements.
• Kernel and linter verification of the current head remains pending, as the PR description acknowledges.

_{Reviews (19) · Last reviewed commit: "fix: apply generic Boolean matrix memory..."}

[Vilin97]

🤖 LLM review (gpt-6-astra, 5 rubrics)

Reviewed head: 7b5af6a2bbcdfb1eb9b354b5cf12defc6f14bb07

Verdict: 🤔 needs_discussion — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	BeyondBethe.theoremOne proves the card’s uniform permanent-approximation and deterministic polynomial-time claims without undisclosed assumptions.
Novelty	✅ pass	Direct searches of pinned Mathlib and the base-branch pool found no declaration subsuming BeyondBethe.theoremOne’s deterministic polynomial-time permanent approximation with base below sqrt(2).
Significance	✅ pass	The permanent-approximation theorem and its supporting analytic and computational theory meet the pool’s research-level significance bar.
Sources	✅ pass	The pinned upstream source supports the claimed approximation and polynomial-time result, and the PR credits the imported formalization and Complexitylib.
Code quality (advisory)	🤔 discuss	Substantial duplication in the machine implementations and helper proofs warrants a maintainer’s refactoring review.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	Entrywise nonnegativity is required for the approximation guarantee and disclosed in the card; the certificate routine, source inequalities, and polynomial-time implementation are supplied by proofs rather than assumed.
Matches cited source	✅ matches
Fit	✅ good_fit
Level	research
Branch	approximation algorithms
Mode	theory_building
Code quality	2 / 5

Statement check: It constructs one rational-valued algorithm and an absolute 0 < c < sqrt(2), proving alg(A) ≤ permanent(A) ≤ c^n·alg(A) for every nonnegative rational n-by-n matrix, including dimensions 0 and 1, together with a deterministic Turing-machine implementation polynomial in binary input length.

BeyondBethe.theoremOne establishes deterministic polynomial-time permanent approximation with exponential base strictly below √2, the research contribution of Beyond the Bethe Approximation of the Permanent, supported by stable-polynomial inequalities, rational optimization, and machine complexity proofs.

Code quality findings (2)

• duplicate-definition — LeanPool/BeyondBethe/BeyondBethe/MachineRationalRowDivide.lean:49
  RowDivide and RowAdd independently reproduce the same bounded traversal, state projections, polynomial-time proofs, iteration bounds, and semantic induction; the substantive differences are the scalar operation and output-size constants. The same pattern recurs in MachineMatrixNormalizeEntries versus MachineMatrixAddDelta. Changes to encoding or iteration APIs therefore require parallel repairs across these implementations. Extract a bounded list-mapping machine parameterized by the entry operation and its semantic/size guarantees. Also reuse the existing generic nested-matrix access/update routines in MachineBooleanMemory: machineBoolMatrixEntryAtUnary and machineBoolMatrixUpdateAtUnary duplicate their machineNestedMatrix counterparts exactly.
  Evidence: MachineRationalRowDivide.lean:49–51: def machineRationalRowDividePack (remaining accumulator scale bound : List Bool) : List Bool := pair remaining (pair accumulator (pair scale bound))
  MachineRationalRowAdd.lean:49–51: def machineRationalRowAddPack (remaining accumulator delta bound : List Bool) : List Bool := pair remaining (pair accumulator (pair delta bound))
  Both independently define the same clamp:
  def machineRationalRowDivideNextAccumulator (state : List Bool) : List Bool := (machineRationalRowDivideCandidate state).take (machineRationalRowDivideBound state).length
def machineRationalRowAddNextAccumulator (state : List Bool) : List Bool := (machineRationalRowAddCandidate state).take (machineRationalRowAddBound state).length
  Their respective machineRationalRowDivideStep_semantics and machineRationalRowAddStep_semantics proofs both begin at line 489 and independently establish the same traversal invariant.
• duplicated-proof — LeanPool/BeyondBethe/Complexitylib/Models/RandomAccessMachine/Simulation/RegisterStore/Machine/Instruction/DenseStore.lean:25
  The tape helpers are repeatedly reproved as private declarations: hasBinaryPrefix_parked has 13 identical copies across EntryUpdate and Instruction modules, and phaseTransition_of_parked has 16 across Instruction, Lookup, and Program modules. This spreads direct dependencies on the tape representation across many files. Move these facts into a shared tape/transition module. Related repetitions include binaryAddConstTime_zero_le in Program/DenseBoundsProof and Program/Bounds/Internal, and the identical natural-list sum bound in both rational-row modules and both matrix-transformation modules.
  Evidence: The repeated proof in DenseStore.lean:25–34 is:
  private theorem hasBinaryPrefix_parked {t : Tape} {bits : List Bool} (h : t.HasBinaryPrefix bits) : TM.Parked t := by refine ⟨by rw [h.1]; omega, ?_⟩ intro j hj obtain ⟨i, rfl⟩ : ∃ i, j = i + 1 := ⟨j - 1, by omega⟩ by_cases hi : i < bits.length · rw [h.2.1 i hi] exact Γ.ofBool_ne_start _ · rw [h.2.2 i (Nat.le_of_not_gt hi)] decide
  The same declaration and proof occur, for example, in Instruction/Store.lean:28, Instruction/Load.lean:171, Instruction/Sim/Internal.lean:38, and EntryUpdate/TaggedProof.lean:27. The adjacent repeated phaseTransition_of_parked concludes with exactly TM.phaseTransition_eq_self_of_reads_ne_start hinput.read_ne_start (fun i => (hwork i).read_ne_start) houtput.read_ne_start.

---

Tokens: 4,408,002 in / 32,133 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $90.5700 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

CI was not green for this commit at review time; this review does not replace CI.

[Vilin97]

Changes requested by automated review

Reviewed exact current head 3e42dee6d7f9ab09caa26681d461ef0d8bcf5e50. The Beyond Bethe import still fails the zero-warning gate with deprecated, flexible-simp, tactic, and style warnings in the Turing-machine and permanent-approximation closure. Repair the warning set and proof-size issues recorded by the PR, then rerun full protected CI.

[Vilin97]

Source reconciliation and generated-index repair reviewed at 279484634ac315be14929ac12344dee8db44b213. The pinned generator now passes mk_all --module --check: this commit only sorts five extracted-module imports, resolving the previous Documentation preflight failure. Current main 0e9b057b was already included. All 708 project Lean files, the project card, and all 218 main cards were preserved byte-for-byte.

I carried forward the substantive review at 7b5af6a2 by comparing the full current source, not just module headers. The comparison includes type-level let assignments and match branches: 9,490 existing same-file theorem types are unchanged; all 97 moved theorem contracts and proof bodies and all 72 moved data declarations match; existing data definitions are unchanged apart from a redundant exposure annotation. The 68 new helper theorems and 41 refactored existing proofs preserve the earlier frame, readiness, resource, and machine-step assertions. The new empty-left binary add/sub helpers specialize the former induction cases. No new headline premise or mathematical definition was introduced.

Faithfulness, novelty, significance, and provenance/source assessments therefore carry forward: BeyondBethe.theoremOne remains the deterministic binary-input polynomial-time rational algorithm with the uniform permanent approximation guarantee, including dimensions 0 and 1. The pinned Complexitylib attribution and all 67 production dependencies protected by the earlier smoke-harness cleanup remain intact.

Code quality remains DISCUSS for the two existing maintainability advisories: the parallel bounded list-traversal developments and repeated parked-tape/transition lemmas are still present. The Boolean-matrix access/update routines have a particularly small reuse opportunity with the existing generic nested-matrix routines; this review does not claim those duplicates were removed. No cold local project build was launched. Fresh required CI remains necessary, so this is a source carry-forward recommendation and validated index repair, not final merge acceptance.

[Vilin97]

Bounded maintainability repair at 613f2daf4ce750a417dac2cb4cef78aa15e5cee7: the Boolean matrix entry/update routines retain their names and exact signatures while delegating to the existing generic nested-matrix routines. Their previous bodies were identical to those generic routines, so behavior is preserved on every input word, including malformed inputs. The FP and canonical-encoding results now specialize the generic proofs.

The 13 duplicated parked-prefix proofs, 16 duplicated phase-transition proofs, and two duplicated constant-addition time proofs now use three shared facts. Existing local helper names and statement types remain as thin wrappers. The bound is still exactly 4 * (fixedValue + 1)^2; no hypothesis or endpoint was weakened. The import graph remains acyclic. This removes 166 net lines across 25 files.

Independent source reviews passed, as did the unchanged repository header, forbidden-source and size checks, declaration-signature preservation checks, and actual pinned mk_all --module --check. Project cards, source attribution, and the generated index are unchanged. A bounded local tape-foundation check is queued; the large matrix dependency closure has not been rebuilt locally. Fresh required CI must validate elaboration and full acceptance. The broader bounded-list mapping abstraction and remaining natural-list-bound duplication are still advisory work; this change does not claim to resolve all maintainability findings.

[Vilin97]

Source and scoped validation follow-up on 03e1396b9e6d202227415a32850d823c0ad9beec.

Published four reviewed tactic repairs: explicit goal changes, closed no-start proofs, and explicit Counter witness/simplification steps. The existing theorem statements and definitions are preserved. The seven incoming importer repairs were retained before the guarded normal push.

The final Helpers, Generic and Counter sources each compiled warning-free in retained runs. The ten-module foundation check also retains the validated Defs/Combinators artifacts and four exact-source cached dependencies. Registers compiled with one show style warning; its reviewed one-word change repair still awaits the existing bounded recheck. The 28-file source-style batches are likewise pending on that same queued check.

The unchanged repository header, forbidden-source and file/proof-size checks pass on the four modified files. The actual pinned mk_all --module --check passed at this exact head. Source hashes for all ten foundation modules and all 28 style inputs were recorded for the eventual result.

Full-project compilation, Boolean/BinaryAdd consumer validation, compiled trust checks and required CI remain pending. This scoped update does not assert full approval or resolution of the broader traversal/refactoring advisories.

[Vilin97]

Source review of 7eaff9e1bc5f42d447c4896c61db2606653e4119, covering incoming commits 6ad666d0 and 7eaff9e1 against the 42 diagnostics from the preceding build.

The importer has already published the concrete three-file repair, so I preserved those commits. Nine cleanup helpers now introduce their existing type-level let bindings directly; the binder order and values match the removed local duplicates, and no new assumptions are introduced. The scanner proof rewrites the explicit source tape and head before discharging the same suffix obligations. The optimizer proof corrects the norm_num location syntax while retaining the same rules, hypotheses, goal and final arithmetic argument. All theorem statements are unchanged.

I inspected the complete incoming diff and checked the affected helper contracts and remaining proof bodies. The unchanged repository header, forbidden-text, file-size and proof-size checks pass for these three files, as does git diff --check.

These new fragments have not been compiled locally. Fresh CI must confirm elaboration; the other project warnings, full lint and compiled trust checks remain outstanding. This is a scoped source-review comment, not full-project approval.

[Vilin97]

Changes requested by automated review

Reviewed 05a5db4f54a99619477ee96d31f0cafde51f8630. The permanent approximation and polynomial-time machine endpoint remain significant; the nonnegative-rational input domain is explicit, and the source comparison supports that scope.

Blocking finding: Complexitylib/Models/RandomAccessMachine/Simulation/RegisterStore/Machine/Program/DenseInitProof.lean:284,296 applies terms with incompatible arities/types; line 477 then refers to the unbuilt denseInit_sequence_parked. These are actual compiler failures, not a cancelled aggregate check. Repair the changed machine-helper callers and compile the complete machine-to-approximation dependency closure.

Evidence: exact-head build log. Acceptance condition: the complete project, repository quality/axiom gates and required protected checks pass on the repaired head, and the remaining substantive/maintainability findings are resolved. The prior bot verdict does not override these reproduced source/build failures.

[Vilin97]

Changes requested by automated review

Reconciled to exact current head cd900c25de4a647ebe09d6817c431e7989db82ee. The main-branch integration leaves this project’s Lean sources byte-identical to the reviewed source; the existing substantive findings and acceptance conditions remain unresolved. The DenseInitProof missing/ill-typed sequence lemmas still prevent the machine-arithmetic dependency closure from compiling.

Preserve the valid completed repairs. Merge requires the cited author-actionable defects to be resolved and all protected checks to pass at the resulting head; this is not a needs-maintainer handoff.

[Vilin97]

{
"reviewed_head": "cd900c25de4a647ebe09d6817c431e7989db82ee",
"review_type": "focused incoming-source follow-up",
"assessment": "Read the complete two-file incoming delta. directedNegativeObjectiveCoordinate_bounds splits one norm_num invocation into two applications covering exactly the same rules, seven hypotheses, and goal, before the same nlinarith conclusion. controlCopy_entryScannerReady removes the unnecessary Nat.add_comm simplification rule; its hypotheses and conclusion are unchanged. No statement, definition, or algorithm change occurs.",
"scope": "Compared all own-project changes after reviewed 7eaff9e. All 708 project files including the umbrella remain; project card and own generated index are unchanged. This follow-up preserves the preceding substantive review and its outstanding full-port validation requirements.",
"validation": "Full incoming-diff and relevant constructor/proof-context review, project inventory/card/index comparison, and git diff --check passed. No fresh local compilation is claimed. Existing unresolved review findings and full CI, lint, and compiled trust requirements remain; this comment is not whole-project approval.",
"findings": []
}

[Vilin97]

{
"reviewed_commit": "a7e61adc94fe8c1e2ec404ac6886724879d7eb4e",
"base_commit": "26344ee88287c59673f561b7b790cb94478279ba",
"scope": "Focused one-file repair of the DenseInitProof compiler failure; prior full-port requirements remain.",
"conclusion": "The private sequencing helper now names the intended Turing-machine configuration type. Public theorem statements and every proof body are unchanged. Fresh compilation is required.",
"problem": {
"job": "https://github.com/Vilin97/lean-pool/actions/runs/36225409472/job/108358424525",
"evidence": "At the base commit, DenseInitProof.lean:284 applies Cfg to a tape count and state type. In its enclosing RAM namespace, Cfg resolves to the parameter-free RAM configuration (pc, regs), causing three Function expected diagnostics and downstream helper/caller errors."
},
"repair": "Qualify exactly two references as Complexity.Cfg, whose parameters and fields match TM.reachesIn, phase1Wrap, phase2Wrap and the four sequencing call sites. Machine definitions, phase order, tape data and time bounds are unchanged.",
"validation": [
"Two independent source reviews checked both Cfg definitions, the entire helper, reused sequencing theorem and all four callers.",
"The 708-file project inventory is retained; only the two private-helper type references and line wrapping changed. Cards, indexes and configuration are unchanged.",
"The four unchanged source-quality checks pass on the modified file, and git diff --check passes."
],
"limitations": "No local Lean compilation was run: the owned checkout lacks the four direct project dependency artifacts. The existing port still has substantial warnings and other validation work; this focused repair is not full-project acceptance."
}

[Vilin97]

{
"reviewed_commit": "8671478d792b39071ebf57157b5aa1e046e3346d",
"base_commit": "8046b5807caed5af1c65f0839b13d6c983d64e99",
"scope": "Focused repair of the two current MachineBooleanMemory compiler errors; existing full-port requirements and the request to leave this PR unmerged remain.",
"conclusion": "The Boolean matrix access and update proofs now apply the existing generic correctness theorems directly. The encoding functions, theorem statements, indices and update results are unchanged. Fresh compilation remains required.",
"problem": {
"job": "https://github.com/Vilin97/lean-pool/actions/runs/36227017672/job/108363175573",
"evidence": "At 8046b58, MachineBooleanMemory.lean:85 and :105 fail after simpa because the higher-order row encoder remains boolVectorCode on one side and binaryListCode boolElementCode on the other. These functions are definitionally equal."
},
"repair": "Replace exactly the two simpa-only wrappers with exact applications of machineNestedMatrixEntryAtUnary_encode and machineNestedMatrixUpdateAtUnary_encode specialized to boolElementCode, following the adjacent vector wrappers.",
"validation": [
"Two independent source reviews checked all encoding aliases, both complete generic correctness proofs, and the unchanged Boolean statements.",
"Only the two proof bodies changed; every other byte in the file and all cards, indexes and configuration are retained.",
"The four unchanged source-quality checks pass on the modified file; git diff --check passes."
],
"limitations": "No local Lean compile: the donor dependency closure contains legacy and stale artifacts, so a one-module validation would not be trustworthy. Full current-head CI is pending. The preceding build also reports substantial project warnings; this focused repair is not full-project acceptance."
}

[Vilin97]

{
"reviewed_commit": "8671478d792b39071ebf57157b5aa1e046e3346d",
"scope": "Focused follow-up on the fresh compiler result after the two Boolean memory proof repairs. Existing source reviews and the request to leave the port unmerged remain.",
"conclusion": "The full pool now compiles at this head, including MachineBooleanMemory. The build gate still fails because the imported project emits warnings; the remaining cleanup spans 233 files.",
"evidence": {
"job": "https://github.com/Vilin97/lean-pool/actions/runs/36228315227/job/108366527564",
"result": "Build completed successfully (14631 jobs); zero compiler error headers. MachineBooleanMemory built in 3.0s.",
"warnings": "1597 original warning headers across 233 BeyondBethe files, excluding the later numbered warning replay. These include 470 show-tactic goal changes and 230 unused simp arguments."
},
"requested_change": "Finish the project warning cleanup in scoped batches: replace goal-changing show with change, remove the exact reported unused simp arguments, update deprecated APIs/imports, and resolve the remaining tactic and declaration warnings. Preserve the production statements and proof dependencies; then obtain a warning-free required build and the remaining declaration/style/trust checks.",
"limitations": "This is fresh CI evidence of compilation, not full project acceptance. The warning guard exits before later checks, and the PR body still requests that the port remain unmerged."
}