{"schema_version":1,"revision":173,"release":"64e0b7080290d3124710289a08e430fc7d5eb7d841296e90906f5dd02bfef36f","totals":{"results":455,"projects":368},"entries":[{"abbreviated":false,"abstract":"Every continuous surjection between compact Hausdorff spaces factors through a compact Hausdorff quotient that collapses exactly the connected components of each original fiber. The first map has connected fibers and the second has totally disconnected fibers. Any two such factorizations have a unique commuting homeomorphism. Empty spaces are permitted.","authors":[{"name":"Arthur Freitas Ramos"},{"name":"David Barros Hulak"},{"name":"Ruy Jose Guerra Barretto de Queiroz"}],"classification":{"arxiv":["math.GN"],"msc2020":["54C10","54D05","54D30","54F05"]},"formalization":{"theorem_names":["MonotoneLight.isClosed_fiberRel","MonotoneLight.exists_monotone_light_factorization","MonotoneLight.unique_monotone_light_factorization"]},"id":"PALOMAR-2026-10-06-000010","path":"entries/PALOMAR-2026-10-06-000010-v1.json","preservation":{"repositories":[{"commit":"759906c53ae14a660ab0e473dcf075d859c5a5a9","fork_repository":"PalomarArchive/Arthur742Ramos--monotone-light-factorization-lean--a4e3fc9d4555","source_repository":"Arthur742Ramos/monotone-light-factorization-lean"}]},"preview":{"artifact_tree_sha256":"408a576a40dc691cd93259f589475cdc53a9836adfdaa278e614592d8d9f41b5","version":1},"published_at":"2026-10-06T11:07:21Z","source":{"commit":"759906c53ae14a660ab0e473dcf075d859c5a5a9","project_path":null,"repository":"Arthur742Ramos/monotone-light-factorization-lean"},"source_omitted":false,"status":"registered","title":"Monotone-Light Factorization of Compact Hausdorff Surjections","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"A complete Lean 4 formalization of Catalan's conjecture, proved by Preda Mihăilescu: 8 and 9 are the only consecutive positive proper perfect powers. The formal proof follows the cyclotomic proof in Yuri Bilu's expositions. Cassels' relations, Stickelberger annihilation, and height and counting estimates exclude the case in which one exponent is congruent to 1 modulo the other. Thaine's theorem on circular units, together with a Runge-type approximation argument, settles the remaining case. The class-field-theoretic input comes from a fixed, vendored subset of the ClassFieldTheory library. The registered results are four theorems: Catalan's conjecture over the natural numbers, in the form stated in Google DeepMind's Formal Conjectures; the same equation for integer bases greater than one; the classification of solutions of x^p − y^q = 1 with nonzero integer bases of either sign; and Mihăilescu's theorem that x^p = y^q + 1 has no solution in nonzero integers when p and q are odd primes. All four depend only on the axioms propext, Classical.choice and Quot.sound.","authors":[{"name":"Yao Xu"}],"classification":{"arxiv":["math.NT","cs.LO"],"msc2020":["11D61","11R18","11R29","11R37","68V20"]},"formalization":{"theorem_names":["PalomarCatalan.catalans_conjecture","PalomarCatalan.catalan_int","PalomarCatalan.catalan_int_signed","PalomarCatalan.mihailescu_odd_primes"]},"id":"PALOMAR-2026-10-06-000009","path":"entries/PALOMAR-2026-10-06-000009-v1.json","preservation":{"repositories":[{"commit":"597469e8eba93909efc94892e6f7df5ea4951fe3","fork_repository":"PalomarArchive/cadamcat--catalan-lean4--fdc727faf3c1","source_repository":"cadamcat/catalan-lean4"}]},"preview":{"artifact_tree_sha256":"753ca0685a86a8f6c6e7d9e983e6395de63ed7c19fa7e581f4d5281a2e79a29b","version":1},"published_at":"2026-10-06T08:38:52Z","source":{"commit":"597469e8eba93909efc94892e6f7df5ea4951fe3","project_path":null,"repository":"cadamcat/catalan-lean4"},"source_omitted":false,"status":"registered","title":"A Lean 4 formalization of Catalan's conjecture (Mihăilescu's theorem)","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"For a Borel subset E of the Euclidean plane with Hausdorff dimension d in (1, 5/4], a strict upper bound on its packing dimension by the explicit piecewise curve B_H(d) ensures a point y in E whose pinned distance set has positive one-dimensional Lebesgue measure. The three branches are 2d-1, 1+r_2(d-1), and 1/(3-2d), with the transitions and algebraic root defined independently in Challenge.lean. This is a sufficient criterion with an additional packing-dimension hypothesis, not a resolution of the general planar Falconer conjecture.","authors":[{"name":"Yongxi Lin"}],"classification":{"arxiv":["math.CA"],"msc2020":["28A80","42B10"]},"formalization":{"theorem_names":["FalconerPacking.exists_pin_volume_pinnedDistances_pos"]},"id":"PALOMAR-2026-10-06-000008","path":"entries/PALOMAR-2026-10-06-000008-v1.json","preservation":{"repositories":[{"commit":"70140ccedfb6de71342299523a21b1550df69ab9","fork_repository":"PalomarArchive/CoolRmal--falconer-packing--054762f09ea9","source_repository":"CoolRmal/falconer-packing"}]},"preview":{"artifact_tree_sha256":"672f8640af6e4ceb683a347efb4db13a4a40bf234cb139eb251403ee39c0a0c3","version":1},"published_at":"2026-10-06T08:09:27Z","source":{"commit":"70140ccedfb6de71342299523a21b1550df69ab9","project_path":null,"repository":"CoolRmal/falconer-packing"},"source_omitted":false,"status":"registered","title":"A Hausdorff–packing criterion for self-pinned distance sets","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"A Lean 4 formalization, with Mathlib, of the main results of the paper \"The Schur degree of block sums: L(4) = 16 and L(5) ≥ 49\" (paper/schur-degree-block-sums.md in this repository). Eliahou and Revuelta (Discrete Math. 344 (2021) 112332) defined a number L(n) through the Schur degree of the set of block sums of a sequence of positive integers, proved S(n−1) + 1 ≤ L(n) ≤ R_{n−1}(3) − 1 and S(n) ≤ n·L(n), and conjectured L(n) = S(n−1) + 1 (their Conjecture 5.6), that is, L(4) = 14 and L(5) = 45. The formalization proves L(4) = 16 (erL_four), 49 ≤ L(5) ≤ 65 (erL_five_bounds), the lift that turns a cover of the nonzero elements of ZMod m₁ × ZMod m₂ by q sets that are sumfree in the group into a sequence whose block sums have Schur degree at most q (lift_lemma), its corollary m₁m₂ ≤ L(n) (le_erL_of_groupPartition), and Theorem 4.1 and the upper bound of Proposition 5.3 of Eliahou and Revuelta, with the pigeonhole bound ramseyBound k in place of R_k(3) (le_sdeg_blockSums, erL_le). So Conjecture 5.6 is false for n = 4 and n = 5. The Lean upper bound for L(5) is 65, not the bound 61 of the paper: the formalization uses the pigeonhole bound R₄(3) ≤ 66 and not the bound R₄(3) ≤ 62 of Fettes, Kramer and Radziszowski. The finite checks use the Lean kernel (decide), with no native code. The sequence W, the lift, the proofs, the programs and the Lean formalization were produced with the AI system Claude (Anthropic; model Claude Opus 5.5) under the direction of the author.","authors":[{"name":"Adam McKenna"}],"classification":{"arxiv":["math.CO"],"msc2020":["05D10","11B75","05C55"]},"formalization":{"theorem_names":["ClassicalSchurClaims.erL_four","ClassicalSchurClaims.erL_five_bounds","ClassicalSchurClaims.le_erL_of_groupPartition","ClassicalSchurClaims.lift_lemma","ClassicalSchurClaims.le_sdeg_blockSums","ClassicalSchurClaims.erL_le"]},"id":"PALOMAR-2026-10-06-000007","path":"entries/PALOMAR-2026-10-06-000007-v1.json","preservation":{"repositories":[{"commit":"933000c135141347835300ca13b3a15ff050d03a","fork_repository":"PalomarArchive/mysticflounder--schur-degree-block-sums--b45c786b5e30","source_repository":"mysticflounder/schur-degree-block-sums"}]},"preview":{"artifact_tree_sha256":"8b5aca112f9faa7e57e679467755cff1822f88907c77fffb83aca281f3be9730","version":1},"published_at":"2026-10-06T05:54:20Z","source":{"commit":"933000c135141347835300ca13b3a15ff050d03a","project_path":"lean","repository":"mysticflounder/schur-degree-block-sums"},"source_omitted":false,"status":"registered","title":"The Schur degree of block sums: L(4) = 16 and L(5) ≥ 49","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"Hausdorff nullity for all finite products of squared successive logarithms and an upper parabolic box dimension bound of 25/23 for interior singular sets of unforced three-dimensional suitable weak Navier–Stokes solutions.","authors":[{"name":"Yongxi (Aaron) Lin"}],"classification":{"arxiv":["math.AP","math.MG"],"msc2020":["35Q30","28A78","28A80"]},"formalization":{"theorem_names":["FluidSingularSets.singularSet_iteratedLogHausdorffMeasure_zero","FluidSingularSets.singularSet_logSquaredHausdorffMeasure_zero","FluidSingularSets.singularSet_upperBoxDimension_le"]},"id":"PALOMAR-2026-10-06-000006","path":"entries/PALOMAR-2026-10-06-000006-v1.json","preservation":{"repositories":[{"commit":"dd3ae61ce421a634818f52a6e11a8b78dd1bfc97","fork_repository":"PalomarArchive/CoolRmal--FluidSingularSets--a936c36bd90d","source_repository":"CoolRmal/FluidSingularSets"}]},"preview":{"artifact_tree_sha256":"3d12abc167864b497d9cae9db7192e88712c4bd56b116f56857c256f6d3479d9","version":1},"published_at":"2026-10-06T04:18:16Z","source":{"commit":"dd3ae61ce421a634818f52a6e11a8b78dd1bfc97","project_path":null,"repository":"CoolRmal/FluidSingularSets"},"source_omitted":false,"status":"registered","title":"FluidSingularSets","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"Every nontrivial compact connected subset of a Hausdorff space contains two distinct points whose individual removals leave connected sets. A compact connected subset containing all non-cut points of a compact connected set equals that set.","authors":[{"name":"Arthur Freitas Ramos"},{"name":"David Barros Hulak"},{"name":"Ruy Jose Guerra Barretto de Queiroz"}],"classification":{"arxiv":["math.GN"],"msc2020":["54D05","54D30","54F15"]},"formalization":{"theorem_names":["NonCutPoints.exists_two_noncut_points","NonCutPoints.eq_of_contains_noncut_points"]},"id":"PALOMAR-2026-10-06-000005","path":"entries/PALOMAR-2026-10-06-000005-v1.json","preservation":{"repositories":[{"commit":"b1d0ed0338d098a4c84622828390cc84027df8dc","fork_repository":"PalomarArchive/Arthur742Ramos--non-cut-points-lean--51757670d602","source_repository":"Arthur742Ramos/non-cut-points-lean"}]},"preview":{"artifact_tree_sha256":"ed80ccc62f49c0fe1b05c7ab789f629f3e94c02ddae7791d9ebe3a7dd3bb4b5d","version":1},"published_at":"2026-10-06T02:45:48Z","source":{"commit":"b1d0ed0338d098a4c84622828390cc84027df8dc","project_path":null,"repository":"Arthur742Ramos/non-cut-points-lean"},"source_omitted":false,"status":"registered","title":"Non-Cut Points of Hausdorff Continua","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"A complete Lean 4 disproof of Erdős problem 575 in both its unrestricted and cycle-containing formulations: a finite family F of forbidden graphs containing a bipartite member need not contain a bipartite H ∈ F with ex(n; H) = O(ex(n; F)). Proves the unrestricted case from scratch via the bipartite forest family F_0 = {K_{1,2}, 2K_2} (where ex(n; F_0) ≤ 1 while ex(n; K_{1,2}) ≥ ⌊n/2⌋ and ex(n; 2K_2) ≥ n - 1), and resolves the cycle-containing case by adapting OpenAI's all-bipartite cyclic counterexample family from Erdős problem 180 (where ex(n; F) = O(n^(21/16)) and ex(n; H) = Ω(n^(4/3)) for every H ∈ F).","authors":[{"name":"Linmiao Xu"}],"classification":{"arxiv":["math.CO"],"msc2020":["05C35"]},"formalization":{"theorem_names":["Erdos575.not_erdos_575_corrected","Erdos575.not_erdos_575","Erdos575.not_erdos_575_all_bipartite","Erdos575.correctedCounterexample","Erdos575.quantitativeCounterexample","Erdos575.ForestCounterexample.forestCounterexample","Erdos575.ForestCounterexample.forestFamily_not_isBipartiteCompact","Erdos575.erdos_575","Erdos575.erdos_575_unrestricted"]},"id":"PALOMAR-2026-10-06-000004","path":"entries/PALOMAR-2026-10-06-000004-v1.json","preservation":{"repositories":[{"commit":"b135fd8f6e5ee25129c4855e06c93739dd80651d","fork_repository":"PalomarArchive/linrock--math-proofs--14cf37780a40","source_repository":"linrock/math-proofs"}]},"preview":{"artifact_tree_sha256":"d797ee544653a199866170b27770751896c582e0519539d0d061a7693c181319","version":1},"published_at":"2026-10-06T02:18:29Z","source":{"commit":"b135fd8f6e5ee25129c4855e06c93739dd80651d","project_path":"erdos-575","repository":"linrock/math-proofs"},"source_omitted":false,"status":"registered","title":"Erdős 575: bipartite extremal-graph compactness","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"A Lean 4 formalization, with Mathlib, of an upper bound for the Schur numbers in terms of the triangle Ramsey numbers, and of the structure of a colouring at the limit of that bound. If every colouring with k colours of the pairs of r points has a monochromatic triangle (R_k(3) ≤ r), then the interval [1, 2((k + 1)⌊(r − 1)/2⌋ + 1)] is not covered by k + 1 sumfree sets, so S(k + 1) ≤ 2(k + 1)⌊(r − 1)/2⌋ + 1. With R_2(3) ≤ 6 this gives S(3) ≤ 13, which is exact. Under the hypothesis R_4(3) ≤ 61, a computer-assisted claim of M. Tatarevic that this project does not prove, the pigeonhole step gives R_5(3) ≤ 302, and the bound then gives S(6) ≤ 1801; the hypothesis is an explicit argument (TriangleRamsey 4 61) of each theorem that uses it. The frontier theorems describe a Schur colouring of the largest interval that the bound allows. Let R_k(3) ≤ u + 1, (k + 1)u = 2t and m = (k + 2)t, and let c be a Schur colouring of [1, 2m + 1] with k + 2 colours. Then each colour occurs exactly t times in [1, m]; with q = c(m + 1), the neighbourhood of the centre m in the colour q is regular in every other colour; and c(m + 1 − d) = c(m + 1 + d) for every d in [1, m] with c(d) = q. For six colours under R_4(3) ≤ 61, a Schur colouring of [1, 1801] gives five sets of 60 points, each closed under x ↦ 1800 − x with no fixed point and with differences in at most four colours. These theorems do not exclude such a colouring and do not prove S(6) ≤ 1800. The arguments for the bound and for the frontier were first proposed by AI agents based on ChatGPT (OpenAI) in a project discussion. A Claude agent (Anthropic) audited the argument for the bound; the AI system Claude checked each step of the frontier argument, restated it with explicit hypotheses, and wrote all Lean proofs, under the direction of the author. The results have not been peer reviewed.","authors":[{"name":"Adam McKenna"}],"classification":{"arxiv":["math.CO"],"msc2020":["05D10","11B75","05C55"]},"formalization":{"theorem_names":["ClassicalSchur.triangleRamsey_succ","ClassicalSchur.not_coveredBySumFree_Icc_of_triangleRamsey","ClassicalSchur.not_coveredBySumFree_Icc_fourteen_three","ClassicalSchur.not_coveredBySumFree_Icc_six_of_triangleRamsey_four_sixtyOne","ClassicalSchur.coveredBySumFree_of_schurColoring","ClassicalSchur.exists_schurColoring_of_coveredBySumFree","ClassicalSchur.card_filter_Icc_eq_of_frontier","ClassicalSchur.card_centralNbhd_of_frontier","ClassicalSchur.card_colorNbhd_centralNbhd_of_frontier","ClassicalSchur.color_eq_of_card_filter_eq","ClassicalSchur.color_reflect_of_frontier","ClassicalSchur.endpointNbhd_of_frontier","ClassicalSchur.even_of_frontier","ClassicalSchur.schur_six_frontier_structure"]},"id":"PALOMAR-2026-10-06-000003","path":"entries/PALOMAR-2026-10-06-000003-v1.json","preservation":{"repositories":[{"commit":"6b1c69732d73428042efce8d563f67604320cad4","fork_repository":"PalomarArchive/mysticflounder--schur-centred-bound--746e036536c8","source_repository":"mysticflounder/schur-centred-bound"}]},"preview":{"artifact_tree_sha256":"fa338286734054d54ddd4e1e632f445368ecb24725185e9865312bd950fb3188","version":1},"published_at":"2026-10-06T01:33:00Z","source":{"commit":"6b1c69732d73428042efce8d563f67604320cad4","project_path":null,"repository":"mysticflounder/schur-centred-bound"},"source_omitted":false,"status":"registered","title":"S(6) ≤ 1801 if R₄(3) ≤ 61: a centred Schur bound and the structure at the frontier","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"A nonempty compact connected Hausdorff space covered by countably many pairwise disjoint closed sets has one piece equal to the whole space. Includes arbitrary countable index types, empty pieces, finite partitions, and the continuous-choice corollary.","authors":[{"name":"Arthur Freitas Ramos"},{"name":"David Barros Hulak"},{"name":"Ruy Jose Guerra Barretto de Queiroz"}],"classification":{"arxiv":["math.GN"],"msc2020":["54D05","54D30","54F15"]},"formalization":{"theorem_names":["Sierpinski.exists_eq_univ_of_nat_closed_partition","Sierpinski.exists_eq_univ_of_countable_closed_partition","Sierpinski.continuous_choice_eq_one"]},"id":"PALOMAR-2026-10-06-000002","path":"entries/PALOMAR-2026-10-06-000002-v1.json","preservation":{"repositories":[{"commit":"406069edac48c4845bbf303ecc83ee9ef000b99a","fork_repository":"PalomarArchive/Arthur742Ramos--sierpinski-closed-partition-lean--fd6de382b003","source_repository":"Arthur742Ramos/sierpinski-closed-partition-lean"}]},"preview":{"artifact_tree_sha256":"315b52f33cfa29fb8136cededdff82f42b528ec4acdaea299f28ddadba6a0c0f","version":1},"published_at":"2026-10-06T00:47:23Z","source":{"commit":"406069edac48c4845bbf303ecc83ee9ef000b99a","project_path":null,"repository":"Arthur742Ramos/sierpinski-closed-partition-lean"},"source_omitted":false,"status":"registered","title":"Sierpinski Closed Partitions of Continua","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"A Lean 4 formalization of unconditional bounds and conditional reductions for Erdős problem 1139 on consecutive P_2 almost-primes (Ω(u_k) ≤ 2). Extending Chojecki's (2026) Erdős 689 double-covering construction via protected-reserve omission, it proves unconditionally that limsup (u_{k+1} - u_k) / log(k + 1) ≥ A > 1 and that every large height X contains an almost-prime-free interval of length ≥ c log X (c > 1), alongside the mixed prime/prime-square CRT bridge, PNT primorial asymptotics, and squared-core deficiency classification. Using a squared-prime core and scale-adaptive dyadic prime shells, it also derives the full infinite-limsup conjecture conditionally from the Green–Tao–Ziegler (2010–2012) linear-forms asymptotic and proves its reverse implication to arbitrary-length prime progressions.","authors":[{"name":"Linmiao Xu"}],"classification":{"arxiv":["math.NT","math.CO"],"msc2020":["11N05","11N36","11B25"]},"formalization":{"theorem_names":["Erdos1139.Palomar.uniform_maximal_gap","Erdos1139.Palomar.limsup_strictly_gt_one","Erdos1139.Palomar.cover_crt_interval","Erdos1139.Palomar.seven_square_crt","Erdos1139.Palomar.primorial_log_limit","Erdos1139.Palomar.limsup_top_of_sparse","Erdos1139.Palomar.core_classification"]},"id":"PALOMAR-2026-10-06-000001","path":"entries/PALOMAR-2026-10-06-000001-v1.json","preservation":{"repositories":[{"commit":"38ad7ea8de1efe526f665c2b5204465e5ed879fe","fork_repository":"PalomarArchive/linrock--math-proofs--14cf37780a40","source_repository":"linrock/math-proofs"}]},"preview":{"artifact_tree_sha256":"d4bea87b44c5ed3fe6cabc8e3f42f92c72c624f3733b870ed2209bc360b622d0","version":1},"published_at":"2026-10-06T00:36:59Z","source":{"commit":"38ad7ea8de1efe526f665c2b5204465e5ed879fe","project_path":"erdos-1139","repository":"linrock/math-proofs"},"source_omitted":false,"status":"registered","title":"Erdős 1139: large gaps between almost-primes","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"Every component of a proper closed subset of a compact connected Hausdorff space meets its frontier. Through each point of the closed subset there is a compact connected subset of it meeting that frontier.","authors":[{"name":"Arthur Freitas Ramos"},{"name":"David Barros Hulak"},{"name":"Ruy Jose Guerra Barretto de Queiroz"}],"classification":{"arxiv":["math.GN"],"msc2020":["54D05","54D30"]},"formalization":{"theorem_names":["BoundaryBumping.closed_component_meets_frontier","BoundaryBumping.exists_subcontinuum_meeting_frontier"]},"id":"PALOMAR-2026-10-05-000009","path":"entries/PALOMAR-2026-10-05-000009-v1.json","preservation":{"repositories":[{"commit":"58831416a12f73312ac01cdaec19c060a6d4b142","fork_repository":"PalomarArchive/Arthur742Ramos--boundary-bumping-lean--12cab9337e49","source_repository":"Arthur742Ramos/boundary-bumping-lean"}]},"preview":{"artifact_tree_sha256":"22c6fe0521710c018068fbd870cc2131199d9f86d6bbd6fe0a5751537f320163","version":1},"published_at":"2026-10-05T22:35:11Z","source":{"commit":"58831416a12f73312ac01cdaec19c060a6d4b142","project_path":null,"repository":"Arthur742Ramos/boundary-bumping-lean"},"source_omitted":false,"status":"registered","title":"Boundary Bumping for Closed Subsets of Continua","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"Over any characteristic-zero field, two elements P and Q of the first Weyl algebra satisfying QP-PQ=1 generate the algebra when P has at most six nonzero homogeneous components for deg X=1 and deg Y=-1. The degree, order and mass of Q are unrestricted. The proof combines sparse-polynomial rigidity with internally proved Newton and Weyl-algebra structural results.","authors":[{"name":"Idris Ali Shaik"}],"classification":{"arxiv":["math.RA"],"msc2020":["16S32","16W20","16W50"]},"formalization":{"theorem_names":["Dixmier.Palomar.massSixGeneration"]},"id":"PALOMAR-2026-10-05-000006","path":"entries/PALOMAR-2026-10-05-000006-v2.json","preservation":{"repositories":[{"commit":"61783d52b6ae44cd2d8d20ad6cb798e7bbbce3ff","fork_repository":"PalomarArchive/shaikidris--DixmierMassSix-Palomar--ea6fbe79e423","source_repository":"shaikidris/DixmierMassSix-Palomar"}]},"preview":{"artifact_tree_sha256":"1fc4a1151423067c51ca2ff3f78ffee13c0a3bdfae626c7717b25daf7830d73e","version":2},"published_at":"2026-10-05T18:57:39Z","source":{"commit":"61783d52b6ae44cd2d8d20ad6cb798e7bbbce3ff","project_path":null,"repository":"shaikidris/DixmierMassSix-Palomar"},"source_omitted":false,"status":"registered","title":"The rank-one Dixmier conjecture for elements of mass at most six","trust":{"level":"high"},"version":2,"versions":2},{"abbreviated":false,"abstract":"A Lean formalization of the superdiffusive central limit theorem for a Brownian particle in a critically-correlated incompressible random drift (Armstrong, Bou-Rabee and Kuusi): the quenched superdiffusive invariance principle (Theorem A), quantitative homogenization of the Dirichlet problem (Theorem B), the large-scale C^{0,gamma} and C^{1,gamma} regularity theory (Theorems C and D) and the sharp asymptotics of the renormalized diffusivities (Theorem 5.1), with every result of Sections 2 to 8 of the paper that their proofs use. It is built on the public CoarseGraining homogenization library and the public MarkovProcess library.","authors":[{"name":"Scott Armstrong"}],"classification":{"arxiv":["math.PR","math-ph","math.AP"],"msc2020":["60K37","35B27","60J60","60F17"]},"formalization":{"theorem_names":["SuperdiffusionCLT.StatementAudit.TheoremA.theoremA"]},"id":"PALOMAR-2026-10-05-000008","path":"entries/PALOMAR-2026-10-05-000008-v1.json","preservation":{"repositories":[{"commit":"b407c97da6af47b63f8067aaf531e2e255bfc78d","fork_repository":"PalomarArchive/scottnarmstrong--SuperdiffusionCLT--db2e44683f08","source_repository":"scottnarmstrong/SuperdiffusionCLT"}]},"preview":{"artifact_tree_sha256":"1617924d408679e4a083b5c4d2400607f94d4ab11ff9272934484fbcb8ab7403","version":1},"published_at":"2026-10-05T18:45:33Z","source":{"commit":"b407c97da6af47b63f8067aaf531e2e255bfc78d","project_path":null,"repository":"scottnarmstrong/SuperdiffusionCLT"},"source_omitted":false,"status":"registered","title":"Superdiffusive central limit theorem for a Brownian particle in a critically-correlated incompressible random drift","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"A conditional Lean 4 formalization of E. Markman, \"Cycles on abelian 2n-folds of Weil type from secant sheaves on abelian n-folds\" (arXiv:2502.03415v2). The paper proves that the Hodge-Weil classes of polarized abelian sixfolds of Weil type with discriminant -1 are algebraic (Theorem 1.5.1) and deduces the Hodge conjecture for abelian fourfolds (Corollary 1.6.1).\n\nEvery result of the paper about cohomology classes, Clifford algebras, spin representations, Hodge structures and period domains is proved in a linear-algebra model of the cohomology of abelian varieties (abelian varieties up to isogeny as polarizable rational Hodge structures of weight one), by the paper's arguments except the departures listed under fidelity (notably Proposition 6.1.2 and Lemma 4.0.2, proved by other arguments with the owner's approval): rational secant lines to the spinor variety and the abelian 2n-folds of Weil type they give (Sections 2-4), the Spin(V)-equivariance of Orlov's equivalence (Section 6, Proposition 6.1.2), Theorem 1.4.1(3) and (4) (the characteristic class of the secant-square sheaf stays of Hodge type on every Weil-type deformation of X x X^, and its K-translates with h^3 span Q h^3 + HW), Corollary 1.3.2, the cohomological results of Section 8, and Section 10. The results the paper cites from Chevalley, Igusa (Lemmas 1-2, Section 2, Proposition 3 except the orbits over subfields in which -d is not a square), Golyshev-Lunts-Orlov, Orlov, Huybrechts, Trautman, van Geemen (Def. 4.9, and Th. 5.2(3) through Landherr's theorem and Meyer's theorem), Markman (2023) and Schoen (Prop. 10, from push-forward of cycles, by Voisin's argument) are proved in the case the paper uses.\n\nTheorem 1.5.1 and Corollary 1.6.1 are proved assuming, as named hypotheses in their statements, the paper's own sheaf-theoretic Sections 7-9 (in the form: the class kappa_3(E) is algebraic near X x X^ wherever kappa(E) is of Hodge type) and results from algebraic geometry not yet available in Lean: about algebraic cycles, pullbacks, push-forwards along projections and products of algebraic classes, the Lefschetz (1,1) theorem, Voisin's algebraicity loci and a theorem of Ramon-Mari; about Hodge structures, two theorems of Moonen-Zarhin. Remark 10.1.2(1) assumes part of Igusa's Proposition 3 when -d is not a square. Eleven statements of the paper are false or misprinted as printed and are formalized in corrected form (the basis of Example 10.2.2 is also misprinted, with no effect on the value computed there); REPORT.md audits the paper.","authors":[{"name":"The-Anh Vu-Le"}],"classification":{"arxiv":["math.AG"],"msc2020":["14C30","14C25","14K22","14K12","15A66","14F08"]},"formalization":{"theorem_names":["WeilClasses.Challenge.Kd_Nm","WeilClasses.Challenge.fX_mul_self","WeilClasses.Challenge.JX_mem_weilDomain","WeilClasses.Challenge.discIs_XXhat","WeilClasses.Challenge.rank_chE","WeilClasses.Challenge.theorem1_4_1_3","WeilClasses.Challenge.theorem1_4_1_4","WeilClasses.Challenge.theorem1_5_1","WeilClasses.Challenge.corollary1_6_1"]},"id":"PALOMAR-2026-10-05-000007","path":"entries/PALOMAR-2026-10-05-000007-v1.json","preservation":{"repositories":[{"commit":"4be865ee7242c8ac4e7b7f92b192b31f9d1c3338","fork_repository":"PalomarArchive/vltanh--lean4-markman25-hodge-abelian-fourfolds--041dfda52aff","source_repository":"vltanh/lean4-markman25-hodge-abelian-fourfolds"}]},"preview":{"artifact_tree_sha256":"e8f341eeeee325a186bc0d1278f498df0efaca2e2e60a6f7768f79a0b8d5bb7c","version":1},"published_at":"2026-10-05T17:07:39Z","source":{"commit":"4be865ee7242c8ac4e7b7f92b192b31f9d1c3338","project_path":null,"repository":"vltanh/lean4-markman25-hodge-abelian-fourfolds"},"source_omitted":false,"status":"registered","title":"Weil classes on abelian sixfolds and the Hodge conjecture for abelian fourfolds (Markman)","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"A formalization and provably correct implementation of a linear-time algorithm for triangulating a simple polygon.  The implementation is a concrete program for an explicit exact real RAM.  Lean proves that on every simple polygon with n vertices the program halts within C(n+1) steps, with natural-number words at most K(n+1), and outputs a conforming triangulation with exactly n - 2 triangles on the input vertices.  No general-position assumption is made.  The proofs use exactly Lean's three standard axioms (propext, Classical.choice, Quot.sound), with no sorry and no native_decide.  They are checked by the Lean kernel and replayed by independent kernels.  The algorithm is a variant of Chazelle's (B. Chazelle, Triangulating a simple polygon in linear time, Discrete & Computational Geometry 6 (1991), 485-524), and the main theorem is the triangulation conclusion of his Theorem 4.3.  The program follows the structure of Chazelle's algorithm: visibility maps of polygonal chains, merging with conformality restoration and granularity enforcement, ray-shooting and arc-cutting oracles built with planar separators, the up phase and the down phase, and the final stage from the visibility map to the triangulation.  It departs from the paper's algorithm in documented ways; in particular its down phase recurses only for n >= 2^30 + 2.  The running-time bound is proved for this program, not for the algorithm as the paper describes it.  The program is also given by name with explicit (very large) constants, and a merge-level refinement theorem shows that its run follows an abstract model of the algorithm written from the paper.","authors":[{"name":"Robert D. Barish"}],"classification":{"arxiv":["cs.CG"],"msc2020":["68U05","68Q25","68W40","52B55"]},"formalization":{"theorem_names":["Chazelle.linear_time_triangulation"]},"id":"PALOMAR-2026-10-05-000003","path":"entries/PALOMAR-2026-10-05-000003-v2.json","preservation":{"repositories":[{"commit":"92cc7745aa026aad3e80e7a72fe88cfbd909614a","fork_repository":"PalomarArchive/RBarish-UTokyo--LinearTimeTriangulation-ChazelleAlgorithm-Lean4--0d58a8483c03","source_repository":"RBarish-UTokyo/LinearTimeTriangulation-ChazelleAlgorithm-Lean4"}]},"preview":{"artifact_tree_sha256":"7dc8d6fa0b8f6b7324db704a2666fbebf50f51c45f6a5ba1f78f7415c14f0014","version":2},"published_at":"2026-10-05T14:21:34Z","source":{"commit":"92cc7745aa026aad3e80e7a72fe88cfbd909614a","project_path":null,"repository":"RBarish-UTokyo/LinearTimeTriangulation-ChazelleAlgorithm-Lean4"},"source_omitted":false,"status":"registered","title":"Linear-Time Triangulation of Simple Polygons (Chazelle's Algorithm) in Lean 4","trust":{"level":"high"},"version":2,"versions":2},{"abbreviated":false,"abstract":"A complete Lean 4 proof of all three parts of Erdős problem 1054. For the least integer f(n) whose k smallest divisors sum to n, we prove that f(n) is not o(n), is not o(n) on any density-one set, and satisfies limsup f(n)/n = ∞ on every density-one subtype. Building on the qualitative divisor-prefix sieve and almost-all binary Goldbach proof from Principia-Math-Solutions, this formalization proves the Formal Conjectures statements along with a sharp second-moment lower-density bound c / [A^3 (1 + log A)^4] for odd n with f(n) > A n, the Tao–Kovač small-ratio upper bound #{n ≤ X : 0 < f(n) ≤ δ n} ≤ C δ^3 X, liminf_{f(n)>0} f(n)/n = 0, and the asymptotic density equivalence between {s(2d)} and even aliquot values.","authors":[{"name":"Linmiao Xu"}],"classification":{"arxiv":["math.NT"],"msc2020":["11A25","11N36","11P32"]},"formalization":{"theorem_names":["Erdos1054.Palomar.answer_i","Erdos1054.Palomar.answer_ii","Erdos1054.Palomar.answer_iii","Erdos1054.Palomar.official_answer_i","Erdos1054.Palomar.official_answer_ii","Erdos1054.Palomar.official_answer_iii","Erdos1054.Palomar.limsup_on_every_density_one","Erdos1054.Palomar.odd_subtype_limsup","Erdos1054.Palomar.f_undefined_at_2","Erdos1054.Palomar.f_undefined_at_5","Erdos1054.Palomar.quantitative_odd_sharp_second_moment_logarithmic_endpoint","Erdos1054.Palomar.quantitative_odd_sharp_second_moment_logarithmic_endpoint_eventual_count","Erdos1054.Palomar.quantitative_odd_almost_full_three_plus_epsilon","Erdos1054.Palomar.quantitative_odd_pure_power_six","Erdos1054.Palomar.small_ratio_count_le_cubic","Erdos1054.Palomar.small_ratio_upper_density_le_cubic","Erdos1054.Palomar.littleO_on_subtype_imp_represented_density_zero","Erdos1054.Palomar.f_sigma_le","Erdos1054.Palomar.frequently_represented_small_ratio","Erdos1054.Palomar.cofactor_two_lower_density_eq_even_aliquot","Erdos1054.Palomar.cofactor_two_upper_density_eq_even_aliquot"]},"id":"PALOMAR-2026-10-05-000005","path":"entries/PALOMAR-2026-10-05-000005-v1.json","preservation":{"repositories":[{"commit":"0917cd01090b52088aa82b09c8c84689047b8171","fork_repository":"PalomarArchive/linrock--math-proofs--14cf37780a40","source_repository":"linrock/math-proofs"}]},"preview":{"artifact_tree_sha256":"e2236be9d84afe5cd548c3fada9a742406cae32c434ff4d780b8cde160414bdb","version":1},"published_at":"2026-10-05T07:51:18Z","source":{"commit":"0917cd01090b52088aa82b09c8c84689047b8171","project_path":"erdos-1054","repository":"linrock/math-proofs"},"source_omitted":false,"status":"registered","title":"Erdős 1054: sums of smallest divisors","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"A complete Lean 4 proof of the negative answer to Erdős problem 958: for every n ≥ 4, there exists an n-point configuration in the Euclidean plane determining n - 1 distinct interpoint distances with multiplicities {1, 2, ..., n - 1} that is neither equidistant on a line nor equidistant on a circle. Formalizing the May 2025 construction of Clemen, Dumitrescu, and Liu, the proof places n - 1 equally spaced points on a short arc of the unit circle together with the center (0, 0), uses strict monotonicity of chord lengths on [0, π/3) to compute the exact distance-multiplicity profile, and eliminates collinear and concyclic progressions algebraically. It also proves the positive baseline results that every equidistant collinear configuration of size n ≥ 2 has n - 1 distinct distances with multiplicities {1, ..., n - 1}, and that for every n ≥ 2 there exists an n-point circular equidistant configuration with that distance-multiplicity profile.","authors":[{"name":"Linmiao Xu"}],"classification":{"arxiv":["math.CO","math.MG"],"msc2020":["52C10","05D99"]},"formalization":{"theorem_names":["Erdos958.Palomar.erdos_958","Erdos958.Palomar.not_erdos_958","Erdos958.Palomar.clemen_dumitrescu_liu","Erdos958.Palomar.equidistantOnLine_has_profile","Erdos958.Palomar.equidistantOnCircle_exists_has_profile"]},"id":"PALOMAR-2026-10-05-000004","path":"entries/PALOMAR-2026-10-05-000004-v1.json","preservation":{"repositories":[{"commit":"08152671ab394392fd941b18654daba734c26518","fork_repository":"PalomarArchive/linrock--math-proofs--14cf37780a40","source_repository":"linrock/math-proofs"}]},"preview":{"artifact_tree_sha256":"01e62e1dcf7260ad373299b2696033f97d2d3991d2971716f1c01a4edbe48904","version":1},"published_at":"2026-10-05T07:11:27Z","source":{"commit":"08152671ab394392fd941b18654daba734c26518","project_path":"erdos-958","repository":"linrock/math-proofs"},"source_omitted":false,"status":"registered","title":"Erdős 958: planar point sets with distance multiplicities {1, ..., n - 1}","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"A complete Lean 4 proof of the negative answer to Erdős problem 2 (Hough 2015; Balister–Bollobás–Morris–Sahasrabudhe–Tiba 2022): there is an absolute constant B such that every finite covering of the integers by distinct moduli > 1 contains a modulus ≤ B. For any finite set D of moduli above B with N = lcm(D), the proof builds a probability measure on ZMod N prime by prime via the BBMST half-cap fiber update, preserving the progression bound w(z ≡ a mod d) ≤ 2^ω(d)/d while bounding each prime-p loss by C (log p)^6 / (p - 1)^2 via Euler factorization and Mertens' third theorem. Combining this summable tail with Euler's product bound on A-smooth reciprocals keeps the covered mass below 1/2, proving the Formal Conjectures ideal statement (erdos_2), its direct negation (not_arbitrarilyLarge_ideal_coverings), the uniform minimum-modulus bound (minimum_modulus_bound), and finite-set noncoverage (finite_noncoverage_bound).","authors":[{"name":"Linmiao Xu"}],"classification":{"arxiv":["math.NT","math.CO"],"msc2020":["11A07","11B25"]},"formalization":{"theorem_names":["Erdos2.Standalone.erdos_2","Erdos2.Standalone.not_arbitrarilyLarge_ideal_coverings","Erdos2.Standalone.minimum_modulus_bound","Erdos2.Standalone.finite_noncoverage_bound"]},"id":"PALOMAR-2026-10-05-000002","path":"entries/PALOMAR-2026-10-05-000002-v1.json","preservation":{"repositories":[{"commit":"7caa4144741e10f96cf79d6f7313a0efd9a18b67","fork_repository":"PalomarArchive/linrock--math-proofs--14cf37780a40","source_repository":"linrock/math-proofs"}]},"preview":{"artifact_tree_sha256":"c526182899c1bacd23c6999d1bf22e0b8c90b0f1f71ec81e1a9af88210570449","version":1},"published_at":"2026-10-05T05:09:05Z","source":{"commit":"7caa4144741e10f96cf79d6f7313a0efd9a18b67","project_path":"erdos-2","repository":"linrock/math-proofs"},"source_omitted":false,"status":"registered","title":"Erdős 2: minimum modulus of distinct covering systems","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"Higher-cell attachment invariance for ordinary topological fundamental groups. For any path-connected topological space X, any basepoint, an index type in an independent universe, independently varying cell dimensions at least three, and arbitrary continuous unit-sphere attaching maps, the genuine adjunction quotient of X and the coproduct of closed Euclidean unit balls is constructed with its quotient topology. The actual inclusion-induced fundamental-group homomorphism is bijective and is the underlying homomorphism of the displayed multiplicative equivalence. Mixed dimensions and the empty family are included. No finiteness, countability, CW, separation or local-connectivity hypotheses are added, and no retraction, simple-connectivity or kernel oracle is assumed.","authors":[{"name":"Arthur Freitas Ramos"},{"name":"David Barros Hulak"},{"name":"Ruy Jose Guerra Barretto de Queiroz"}],"classification":{"arxiv":["math.AT","math.CT"],"msc2020":["55Q05","18B40"]},"formalization":{"theorem_names":["HigherCellAttachment.higher_cell_attachment"]},"id":"PALOMAR-2026-10-05-000001","path":"entries/PALOMAR-2026-10-05-000001-v1.json","preservation":{"repositories":[{"commit":"bcf788e349b4969f4d8379ee9cb4df7a28352af1","fork_repository":"PalomarArchive/Arthur742Ramos--higher-cell-attachment-lean--839dc8f39578","source_repository":"Arthur742Ramos/higher-cell-attachment-lean"}]},"preview":{"artifact_tree_sha256":"d4432379a30d3a56de3a768aa83953b7ccccc6f702cc3c0de3c39e1d1eb92564","version":1},"published_at":"2026-10-05T02:16:29Z","source":{"commit":"bcf788e349b4969f4d8379ee9cb4df7a28352af1","project_path":null,"repository":"Arthur742Ramos/higher-cell-attachment-lean"},"source_omitted":false,"status":"registered","title":"Fundamental Groups of Arbitrary Higher-Cell Attachments","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"The full arbitrary-family two-cell attachment theorem for ordinary topological fundamental groups. For any path-connected topological space X, any basepoint, and any indexed family of continuous circle attaching maps, a genuine adjunction quotient is constructed from X and the coproduct of closed complex unit disks. The actual inclusion-induced fundamental-group homomorphism is surjective and its kernel is precisely the normal closure of the once-around attaching loops, transported along the specified basepoint paths. A quotient group isomorphism is proved compatible with the actual inclusion map. No finiteness, CW, separation, local-connectivity or semilocal-simple-connectivity hypotheses are added.","authors":[{"name":"Arthur Freitas Ramos"},{"name":"David Barros Hulak"},{"name":"Ruy Jose Guerra Barretto de Queiroz"}],"classification":{"arxiv":["math.AT","math.CT"],"msc2020":["55Q05","18B40"]},"formalization":{"theorem_names":["CellAttachment.two_cell_attachment"]},"id":"PALOMAR-2026-10-04-000011","path":"entries/PALOMAR-2026-10-04-000011-v1.json","preservation":{"repositories":[{"commit":"1c671038e320cecc58ca1d81dca11bbe2e2a507c","fork_repository":"PalomarArchive/Arthur742Ramos--cell-attachment-lean--38d25cf83333","source_repository":"Arthur742Ramos/cell-attachment-lean"}]},"preview":{"artifact_tree_sha256":"55348345b49b9e1aa993ea61e7ac2b938d82727a65d9335643d242c6f16a73d0","version":1},"published_at":"2026-10-04T20:55:47Z","source":{"commit":"1c671038e320cecc58ca1d81dca11bbe2e2a507c","project_path":null,"repository":"Arthur742Ramos/cell-attachment-lean"},"source_omitted":false,"status":"registered","title":"Fundamental Groups of Arbitrary Two-Cell Attachments","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"A complete Lean 4 proof of the affirmative answer to Erdős problem 546 (Sudakov's theorem): there exists an absolute constant C > 0 such that every finite simple graph G with m edges and no isolated vertices has diagonal Ramsey number R(G) ≤ 2^(C √m). Formalizing Sudakov's 2011 proof—including high-degree vertex deletion, greedy bounded-degree embedding and hereditary sparse cuts, low-density monochromatic-pair extraction, and iterative clique-reservoir amplification. This proves the uniform explicit bound R(G) ≤ 2^(4000 √m) across all finite simple graphs without isolated vertices (including m = 0), together with the exact Formal Conjectures statement.","authors":[{"name":"Linmiao Xu"}],"classification":{"arxiv":["math.CO"],"msc2020":["05C55","05C35","05D10"]},"formalization":{"theorem_names":["erdos_546_original_statement","Erdos546.erdos_546","Erdos546.sudakov_sparse_bound","Erdos546.sparse_graph_ramsey_witness","Erdos546.boundedDegree_sparse_cut","Erdos546.exists_monoPair_of_low_edgeDensity","Erdos546.quantitative_monoPair_amplification"]},"id":"PALOMAR-2026-10-04-000010","path":"entries/PALOMAR-2026-10-04-000010-v1.json","preservation":{"repositories":[{"commit":"7caa4144741e10f96cf79d6f7313a0efd9a18b67","fork_repository":"PalomarArchive/linrock--math-proofs--14cf37780a40","source_repository":"linrock/math-proofs"}]},"preview":{"artifact_tree_sha256":"91962f832d137ef4feedcba935368c58f49481d7eef0d07466945e1c699b217b","version":1},"published_at":"2026-10-04T20:31:23Z","source":{"commit":"7caa4144741e10f96cf79d6f7313a0efd9a18b67","project_path":"erdos-546","repository":"linrock/math-proofs"},"source_omitted":false,"status":"registered","title":"Erdős 546: sparse graph Ramsey numbers","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"A fully-dynamic Maximum-Cardinality-Search (MCS) ordering algorithm that, on a single-edge insertion or deletion into a loop-free undirected graph, scans the affected window between the two endpoints for the first step at which the current ordering's choice stops being a legal MCS pick, and only then regreedies the suffix (probe-then-repair). Correctness - every order produced stays a valid MCS ordering of the updated graph, and in fact equals the from-scratch canonical ordering - is machine-checked in Lean 4 / Mathlib, together with locality (the first position whose choice can change lies inside the window between the endpoints; after a break the suffix is regreedyed, so positions past the window may also change), an executable boolean-adjacency implementation proved to refine the abstract update, and per-update cost in a unit-cost query model (counting legality checks and pick steps along the real executable control flow): at most n units for an insertion and n + 1 for a deletion, so the worst case matches static recomputation. A stability-boundary result is also proved: if the neighbour count of every vertex in one graph exceeds that in the other by at most one along every chosen prefix, the two graphs admit a common MCS ordering; in particular inserting or deleting a matching, or flipping a single edge, always preserves a common MCS ordering.","authors":[{"name":"Md Thoriqul Islam Thonmay"},{"name":"Gregory Morse"}],"classification":{"arxiv":["cs.DS","math.CO"],"msc2020":["05C85","68Q25"]},"formalization":{"theorem_names":["Challenge.init_valid","Challenge.insert_update_valid","Challenge.delete_update_valid","Challenge.greedySuffix_full","Challenge.update_from_prefix","Challenge.setEdge_preserves_symm","Challenge.setEdge_preserves_loopless","Challenge.mcsOrder_eq_greedySuffix","Challenge.exec_insert_recompute_valid","Challenge.exec_delete_recompute_valid","Challenge.IsMCSOrdering_unique","Challenge.insert_update_eq_initOrder","Challenge.delete_update_eq_initOrder","Challenge.legal_upto_earlierPos","Challenge.legal_after_laterPos","Challenge.delete_legal_between","Challenge.insert_break_iff","Challenge.insert_update_eq_self_iff","Challenge.delete_update_eq_self_iff","Challenge.exec_insert_update_eq","Challenge.exec_delete_update_eq","Challenge.exec_insert_cost_le","Challenge.exec_delete_cost_le","Challenge.exec_insert_cost_of_no_break","Challenge.exec_delete_cost_of_no_break","Challenge.exec_insert_cost_of_break","Challenge.exec_delete_cost_of_break","Challenge.exec_insert_update_c_fst","Challenge.exec_delete_update_c_fst","Challenge.exists_common_ordering","Challenge.common_order_extends_prefix","Challenge.insert_matching_common_order","Challenge.delete_matching_common_order","Challenge.flip_common_order","Challenge.triangle_no_common_order","Challenge.p4_no_common_order","Challenge.mixed_matching_no_common_order"]},"id":"PALOMAR-2026-10-04-000009","path":"entries/PALOMAR-2026-10-04-000009-v1.json","preservation":{"repositories":[{"commit":"a872fddca7025ae0ecedd654238fa0c06729dc2e","fork_repository":"PalomarArchive/thonmay--thesis-lean--090f8db89fc3","source_repository":"thonmay/thesis-lean"}]},"preview":{"artifact_tree_sha256":"1c6c19656f5c44e33db94a341df4d02788be075942e81eeb653d7427e7f61d84","version":1},"published_at":"2026-10-04T18:32:42Z","source":{"commit":"a872fddca7025ae0ecedd654238fa0c06729dc2e","project_path":null,"repository":"thonmay/thesis-lean"},"source_omitted":false,"status":"registered","title":"Dynamic MCS Ordering Maintenance","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"A complete Lean 4 proof of the affirmative answer to Erdős problem 956: for all sufficiently large n, there exist n pairwise-disjoint translates of a compact convex planar set with more than n^(1+c) unordered pairs at Euclidean set-distance 1 (for c = 1/4). Adapting the parabolic construction announced by Valtr (2005) and detailed in Chojecki's April 2026 manuscript, the formalization proves the supporting-hyperplane theorem for a centrally symmetric signed parabolic cap and constructs a four-layer parabolic grid of disjoint translates. This establishes the explicit lower bound h(n) > (1/26) n^(4/3) for all n ≥ 80 and the sharper eventual bound h(n) > (2/5) n^(4/3).","authors":[{"name":"Linmiao Xu"}],"classification":{"arxiv":["math.MG","math.CO"],"msc2020":["52C10","52A10","05D99"]},"formalization":{"theorem_names":["Erdos956.Palomar.erdos_956_superlinear","Erdos956.Palomar.erdos_956","Erdos956.Palomar.erdos_956_omega_four_thirds","Erdos956.Palomar.erdos_956_four_layer_polynomial","Erdos956.Palomar.erdos_956_eventual_two_fifths"]},"id":"PALOMAR-2026-10-04-000008","path":"entries/PALOMAR-2026-10-04-000008-v1.json","preservation":{"repositories":[{"commit":"2afe25fe500b036dfabef8e00c369a434bfff763","fork_repository":"PalomarArchive/linrock--math-proofs--14cf37780a40","source_repository":"linrock/math-proofs"}]},"preview":{"artifact_tree_sha256":"43eb7ad3d2d757f5502376240df94a111596235f450c953f7bc767681708ede1","version":1},"published_at":"2026-10-04T16:32:39Z","source":{"commit":"2afe25fe500b036dfabef8e00c369a434bfff763","project_path":"erdos-956","repository":"linrock/math-proofs"},"source_omitted":false,"status":"registered","title":"Erdős 956: unit distances between disjoint convex translates","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"The critical-window laws for autocatalytic emergence in reversible binary-polymer networks lead to survival profiles for independent open reaction channels. For both the ordered split-position and commuting-factor quotient models, with all binary words of length at most two as food, explicit total algorithms enclose each survival probability at every rational openness in [0,1] to any prescribed positive rational accuracy. Computable seed lengths and finite-record contraction estimates provide uniform truncation bounds on intervals bounded away from zero. The associated intensity profiles S(1 − exp(−λ)) are smaller than every fixed power of λ as λ tends to zero from above. Rational interval bounds also compare these profiles with finite-network RAF-existence probabilities under explicit catalyst-pool and input-probability conditions. These results extend the split and quotient critical-window laws with certified approximation and quantitative control.","authors":[{"name":"Michael Mislan"}],"classification":{"arxiv":["math.PR","q-bio.MN"],"msc2020":["60K35","92E20","05C80","03D78","68V20"]},"formalization":{"theorem_names":["RAF.Concrete.reaction_length_add","RAF.Concrete.reaction_left_pos","RAF.Concrete.reaction_right_pos","RAF.Concrete.reaction_product_le","RAF.Concrete.reaction_pow_split","RAF.Concrete.molLength_reactionLeft","RAF.Concrete.molLength_reactionRight","RAFCriticalWindowQuantitative.seedTest_exists","HordijkSteelThreshold.measurable_currySplitField","RAFReactionQuotient.precedes_total","RAFCriticalWindowQuantitative.geometricTest_exists","RAFCriticalWindowQuantitative.repair_ratio","RAFCriticalWindowQuantitative.quantitative_critical_window_resolution"]},"id":"PALOMAR-2026-10-04-000007","path":"entries/PALOMAR-2026-10-04-000007-v1.json","preservation":{"repositories":[{"commit":"b46f8d0747b6dfb4c00a50d386f3df4f330e861e","fork_repository":"PalomarArchive/mmislan--palomar-p046-critical-window-shape-law--e3ad53e8d156","source_repository":"mmislan/palomar-p046-critical-window-shape-law"}]},"preview":{"artifact_tree_sha256":"2194cb4ccf7a4ea6af2f62c0ae23567c0ad8ed1efcbfe5f983ae233104a45d90","version":1},"published_at":"2026-10-04T15:07:36Z","source":{"commit":"b46f8d0747b6dfb4c00a50d386f3df4f330e861e","project_path":null,"repository":"mmislan/palomar-p046-critical-window-shape-law"},"source_omitted":false,"status":"registered","title":"Effective approximation and low-intensity flatness of RAF critical-window profiles","trust":{"level":"high"},"version":1,"versions":1},{"abbreviated":false,"abstract":"Every connected finite simple graph admits an edge partition into at most ceil(|V(G)|/2) simple paths when at most two vertices of its induced even-degree graph have degree greater than three. One positive designated even vertex can be exposed twice at the ceiling budget. Two designated even vertices can be exposed twice simultaneously within floor(|V(G)|/2)+1 paths, giving simultaneous ceiling exposure at odd order. Exceptional and ordinary degrees are unrestricted. Simultaneous even-order ceiling exposure and the unrestricted Gallai conjecture are not claimed.","authors":[{"name":"Idris Ali Shaik"}],"classification":{"arxiv":["math.CO"],"msc2020":["05C38","05C70"]},"formalization":{"theorem_names":["Gallai.Submission.prescribed_endpoint","Gallai.Submission.ceiling_bound","Gallai.Submission.simultaneous_floor_add_one","Gallai.Submission.odd_order_simultaneous"]},"id":"PALOMAR-2026-10-04-000006","path":"entries/PALOMAR-2026-10-04-000006-v1.json","preservation":{"repositories":[{"commit":"5f4130a2e14b836cfaa86cad6ae59beb9768b9ea","fork_repository":"PalomarArchive/shaikidris--gallai-two-exception--3391d32f463e","source_repository":"shaikidris/gallai-two-exception"}]},"preview":{"artifact_tree_sha256":"a806a85e212c93464b974b01693f7de5d8f741f450aada546ee712e59eeafb4c","version":1},"published_at":"2026-10-04T13:47:26Z","source":{"commit":"5f4130a2e14b836cfaa86cad6ae59beb9768b9ea","project_path":null,"repository":"shaikidris/gallai-two-exception"},"source_omitted":false,"status":"registered","title":"Gallai's conjecture with two exceptional even vertices","trust":{"level":"high"},"version":1,"versions":1}],"previous":null,"next":"eyJyZXZpc2lvbiI6MTczLCJxdWVyeSI6ImRhYzQyYzA2NTVkM2RjYzBlZWM3MWE1ODlmNDczMDNiOTk0NDJmN2Y0YmUwY2RiNzRkYjllYzgyZDdkN2VjNzUiLCJkaXJlY3Rpb24iOiJuZXh0IiwiZGF0ZSI6IjIwMjYtMTAtMDRUMTM6NDc6MjZaIiwiaWQiOiJQQUxPTUFSLTIwMjYtMTAtMDQtMDAwMDA2In0=","dropped":[],"message":null}