Isolated adversarial reconstruction of the compiled Erdős #530 interface, followed by a kernel-checked comparison with the repository's existing Sidon API and a minimal API-reuse refactor.

Progress

The pre-refactor candidate's warning-fatal exact target build was validated. Independent review then found that the candidate duplicated the repository's existing IsSidon API. A separate Lean checker proved the old and project predicates equivalent for every finite real set and passed adversarial repeated-summand and swap controls. The candidate was refactored to reuse the project definition. Its new hash is queued/running in a checkpointed target build and is not yet claimed to compile.

Strategy and discriminator

isolated adversarial reconstruction

Reconstruct the source meanings independently, detect repository API duplication, and compile a universal equivalence theorem before changing the candidate.

Hypothesis: The candidate's finite-set Sidon predicate is extensionally equivalent for every Finset ℝ to the repository's reusable set-level IsSidon predicate, including repeated summands and swapped-pair triviality.

Test: Compile a separate Lean file that restates the removed finite predicate and proves an iff with project IsSidon for an arbitrary Finset ℝ, plus repeated-summand and swap controls.

Rationale

The universal Lean equivalence is stronger and more relevant than another bounded enumeration and directly justifies the API refactor. The prior lab receipt supports only the old source hash, so the verification contract remains incomplete for the current candidate.

Claims requiring scrutiny

For every Finset ℝ, the removed LegacyFinsetIsSidon predicate is logically equivalent to the repository's IsSidon predicate on its set coercion.
The pre-refactor candidate hash 208af82a29f35bf60d55f86669f7794cf30aae39d71eb24968f255b8cfa771c9 passed its exact warning-fatal Lean target build and produced a 126000-byte OLean.
The current candidate hash e27b8c80ed9edb57989006cc9bd299fdd58331c2b2a30b69ec9721b409562a2e reuses project IsSidon and has not yet been claimed to build.
The maintained problem page and issue #773 still present Problem #530 as open and without an accepted formalization.

Evidence and scope

Lean 4.27.0 accepted checks/Erdos530SemanticAudit.lean in experiment 20260721-223233-e53846, return code 0, empty stdout/stderr.
Validated lab-scout-bdf77f43574b-83c018dc57aa, return code 0, 886.529 seconds, exact target success.
sha256sum FormalConjectures/ErdosProblems/530.lean = e27b8c80ed9edb57989006cc9bd299fdd58331c2b2a30b69ec9721b409562a2e.
Official source and issue inspected on 2026-07-21.

Computational experiments

.proof-experiments/20260721-223233-e53846: universal equivalence checker passed in 10.082 seconds with empty diagnostics.
.proof-experiments/20260721-222914-f94e3f: infrastructure-only failure from a stale mounted OLean path before theorem elaboration.
.proof-experiments/20260721-223142-8e7b27: isolated checker rejected unavailable category syntax before semantic elaboration.
lab-runs/lab-scout-bdf77f43574b-83c018dc57aa/segment-000001/20260721-220709-5122ed: pre-refactor exact target passed in 886.529 seconds.

Independent checker

checks/Erdos530SemanticAudit.lean independently restates the removed predicate, imports the reusable project definition directly, and proves their equivalence for an arbitrary Finset ℝ; it does not rely on model agreement or finite extrapolation.

Contribution gate

not_requested

No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.

Original model outcome: progress
Public classification: progress

Cross-domain transfers tested

None recorded.

Established facts

LegacyFinsetIsSidon S ↔ IsSidon (S : Set ℝ) for every S : Finset ℝ.
Lean theorem legacyFinsetIsSidon_iff_projectIsSidon; experiment 20260721-223233-e53846. · All finite subsets of the real numbers. · proved
The pre-refactor source hash 208af82a…71c9 is warning-clean for its exact Lean target.
Validated lab-scout-bdf77f43574b-83c018dc57aa and OLean hash 5401908c…3201. · Pinned checkout 8f6e745…, Lean 4.27.0, exact module target only. · computed
The maintained source marked Problem #530 open and not formalised on 2026-07-21.
https://www.erdosproblems.com/530 · Maintained-site status, subject to its explicit literature-completeness warning. · conditional

Ruled out in this epoch

Retain a namespace-local finite-set IsSidon definition in the Problem 530 file.
Current Formal Conjectures interface design. · The repository already exports an extensionally equivalent reusable predicate, proved equivalent by Lean. · checks/Erdos530SemanticAudit.lean and experiment 20260721-223233-e53846. · A maintainer explicitly requires a local wrapper despite the existing project API.
Claim that the exact target eliminated 8037 unrelated build jobs.
Search-efficiency accounting for this checkout. · The validated exact-target stdout itself reports an 8038-job dependency closure. · lab-scout-bdf77f43574b-83c018dc57aa stdout. · A measured dependency-graph comparison with a full build establishes a different exact count.
Formalize weak Sidon uniqueness while ignoring repeated summands.
Problem #530 statement design. · It wrongly accepts {0,1,2}. · Prior 512-case regression and the new projectIsSidon_rejects_zero_one_two theorem. · An authoritative source changes the target to weak Sidon sets.
Demand uniqueness of ordered pair representations.
Problem #530 statement design. · It wrongly rejects the commutative swap. · Universal equivalence and swapped-pair control. · None for the present source statement.

Open leads

Review the refactored target lab.
It is the cheapest decisive check of the current source hash. · Inspect the completed record, hashes, stdout, stderr, and OLean for lab-scout-bdf77f43574b-03d1a8ffc4cf. · high · open
Resolve placement of extremal helper definitions.
The contribution guide may require definitions needed for the conjecture in FormalConjecturesForMathlib. · Compare accepted nearby extremal-function files and request maintainer review of the two possible layouts. · high · open
Clean-checkout and full-CI reproduction.
These are explicit remaining verification-contract gates after source placement stabilizes. · Apply only the stabilized patch to a clean pinned checkout, run the exact target, then submit a checkpointed full lake --wfail build. · normal · open

Continuation checkpoint

Objective: Convert the API-refactored declaration into a kernel-checked, placement-reviewed Formal Conjectures contribution.

First action: Inspect durable state for lab-scout-bdf77f43574b-03d1a8ffc4cf and stop at its first exact warning or elaboration discrepancy.

Stop condition: Redirect on the first build or placement discrepancy; advance only after the current hash passes and a reviewer accepts the interface layout.

Next moves

Inspect durable completion state for lab-scout-bdf77f43574b-03d1a8ffc4cf without resubmitting it.
If the refactored target passes, conduct a maintainer-style placement review for GuaranteedSidonSize, ell, and supporting lemmas.
After placement is settled, run a clean-checkout target control and a checkpointed full lake --wfail build.
Seek human Formal Conjectures review and linked-PR acceptance; do not claim upstream formalization beforehand.

Citations

Tool disclosure

Sol principal: GPT-5.6 per campaign configuration, using shell inspection, web source verification, SHA-256, Python 3.12.3 experiment capture, Lean 4.27.0, and Lake 5.0.0. Terra delegate: gpt-5.6-terra performed prior bounded source reconnaissance; its memo was advisory only, all relied-on claims were independently checked, and its unsupported 8037-target reduction claim was rejected. No CAS, SAT/SMT solver, proof assistant other than Lean, or additional subagent was used this epoch.

Duration: 848.4s
Review state: not a result claim
Attempt ID: scout-bdf77f43574b-20260721-223958-e0f52b

Human review ledger

No human review recorded.