# yaml-language-server: $schema=https://raw.githubusercontent.com/mathlib-initiative/formalization.yaml/main/schema/formalization.schema.json version: "v0.4" project: name: "fs-formal: an improved Furstenberg-Sárközy lower bound" description: >- A Lean 4 formalization of an explicit construction for the Furstenberg-Sárközy problem. If D(N) is the largest size of a subset of {1,...,N} with no nonzero square difference, the development proves that an explicit eleven-block constant alphaInf is at most liminf log D(N)/log N, that every exponent below alphaInf holds eventually pointwise, and that 0.7537 < alphaInf. The proof includes the finite certificates, the composite even-digit lift, CRT gluing, asymptotic passage, and kernel-checked numerical inequalities. This strictly improves Krachun's preceding explicit exponent 0.752796455874514... and moves the lower bound farther beyond 3/4. authors: - "JD Jones" license: "MIT" responsible_maintainers: - "JD Jones" classification: arxiv: ["math.CO", "math.NT"] msc2020: ["11B30", "11B75"] sources: - title: "An improved lower bound for the Furstenberg-Sárközy problem" authors: - "JD Jones" id: "https://github.com/JD-Jones-ASES/fs-lower-bound/tree/c2c06875ee4544e069e8da16564ee429d870a13e" type: "other" location: "https://github.com/JD-Jones-ASES/fs-lower-bound" relationship: "formalizes" note: >- This is the mathematical source followed by the Lean development. It presents the improved eleven-block construction and the composite even-digit lift. The Lean repository reproves the entire chain needed for the compared results. license: "MIT" author_endorsement: "participated" - title: "Square-difference-free sets beyond the three-quarter barrier" authors: - "D. Krachun" id: "arXiv:2608.01325" type: "paper" location: "https://arxiv.org/abs/2608.01325" relationship: "background" note: >- Supplies the Paley-chain construction and the ranked-block mechanisms extended by the source result. The Lean development proves the needed analogues of Lemmas 4 and 5 rather than assuming them. related_formalizations: - id: "https://github.com/JD-Jones-ASES/fs-lower-bound-lean/tree/2e6c33c82e57415e5238467620a44a8e1d9b5904" relationship: "adapts" revision: "2e6c33c82e57415e5238467620a44a8e1d9b5904" note: >- Canonical completed Lean development from which this Palomar-ready repository was copied. This repository adds the independent Mathlib-only Challenge, proved Solution bridge, Comparator configuration, registry metadata, and immutable CI pins, and ports the project from unsupported patch release v4.33.1 to v4.33.0. status: scope: >- The three compared theorems prove alphaInf <= liminf log D(N)/log N, the eventual pointwise bound for every rho < alphaInf, and 0.7537 < alphaInf. The formalization does not state all digits of the informal approximation 0.753741541837329405..., an endpoint estimate with a fixed multiplicative constant, optimality of the pool or certificates, or the induced point-line matching corollary in the source note. Deliberate sorries occur only in Challenge.lean and are excluded from the proof counts below; Solution and the proof development are sorry-free. sorry_count: 0 sorry_in_definitions: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] main_results: - declaration: "FsFormal.sdf_liminf_ge" file: "Solution.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "comparator.json" - declaration: "FsFormal.sdf_pointwise" file: "Solution.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "comparator.json" - declaration: "FsFormal.alphaInf_gt" file: "Solution.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "comparator.json" automation: methods: - method: "agent" models: - "Claude Code (Fable 5)" - "Codex (GPT 5.6 Sol)" - "Grok Build (Grok 4.6)" - "OpenAI Codex (Palomar adaptation; exact model not recorded)" framework: "mixed AI-agent workflow" tool_setup: >- The mathematical result and Lean proof were AI-generated under JD Jones's direction using the first three systems, as recorded in the source disclosure. OpenAI Codex prepared this Palomar statement/solution separation, metadata, CI, and supported-toolchain port. Lean's kernel, the repository axiom audit, Comparator, lean4export, and NanoDa provide replayable checks independent of the generating systems. prompting_notes: >- The human operator set the theorem, managed the workflow, required explicit certificate and scope boundaries, and asked agents to prove, audit, and package the result. Detailed prompt and token accounting was not retained here. spend_usd: "not tracked" notes: >- AI systems generated and audited substantial mathematics and code; JD Jones directed the work and is the responsible author and maintainer. Git history and the source DISCLOSURE.md preserve the recorded division of work. fidelity: divergences: >- The compared Lean statements match the three targets in the canonical formalization. The rational inequality 0.7537 < alphaInf is formalized, but the longer decimal shown informally is not a Lean theorem. The informal induced-matching corollary is omitted. The Palomar port changes Lean and Mathlib from v4.33.1 to v4.33.0 for exact exporter compatibility; it does not intentionally change any mathematical declaration. review: status: "self-assessed" reviewers: - "JD Jones" notes: >- No independent human expert or peer review is recorded. The completed upstream project passed Lean CI. This port's transitive axiom audit covers 129 declarations, and its source guards also pass. Palomar's pinned Comparator accepted the three declarations and Lean-kernel replay in a local macOS development run; that run used Comparator's unsandboxed development shim and disabled NanoDa. The real Landrun and NanoDa replay remain the Linux CI and Palomar-verifier checks. Those checks establish proof replay and statement equality, not novelty, significance, or correctness of the informal interpretation. alignment: namespace: "FsFormal" statements: - source: "fs-lower-bound README, main liminf theorem" lean: "FsFormal.sdf_liminf_ge" module: "Solution" status: "proved" note: >- Uses the exact eleven-block alphaInf and the extremal function D reproduced in Challenge.lean. - source: "fs-lower-bound README, equivalent pointwise form" lean: "FsFormal.sdf_pointwise" module: "Solution" status: "proved" note: >- Gives an eventual lower bound for each rho strictly below alphaInf; it does not claim the endpoint with a fixed constant. - source: "fs-lower-bound README, verified numerical headline" lean: "FsFormal.alphaInf_gt" module: "Solution" status: "proved" note: >- Certifies only the exact rational threshold 0.7537, using natural-power comparisons rather than floating-point evaluation. acknowledgements: >- Lean, Mathlib, Comparator, lean4export, NanoDa, Landrun, the Palomar starter and verifier projects, D. Krachun's construction, and the AI systems disclosed above.