Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Subject and independence
Role. Independent reviewer in a fresh context, commissioned for
refutation with only the assignment text. The reviewer took no part in
writing the connections page, the reconstruction pages or the library
pages read, and had no contact with their author. Nothing under the
folder's evidence/ directory, no review, grade, standing or acceptance
text of the section, and no page outside the named read set was
consulted, except as the exposures below record. No web search was made.
Subject. The source as it stood on 2026-09-28T13:50:48Z (called "the
subject commit" below), page
wiki/research/erdos_416/connections.md, section
"## Problem 694: the extreme fiber ratio", lines 493–518 (the H2 at line
493 to the line before the next H2 at line 519). The section files no
lead page; its recorded outcome is "Fails".
Read, and at what depth.
- The section in full; every sentence is restated below.
- The page's shared sections (lines 1–90): the standing paragraph, the notation (, , , , , , , ), the imported inputs (F), (F8), (W), (KK) and the search paragraph, read as inputs at interface level; their own proofs are another reviewer's.
- The Problem 417 section (lines 91–341) at interface level only, because the section under review cites its "bounded-record premise" and its Theorem 417.3: the statement of Theorem 417.3, its Step 1 (the witness with preimages and ) and Step 2 (every has ), and the pair-family bullet under "What it does not give" (lines 262–271), which states the premise.
wiki/research/erdos_416/kruer_kohlmeyer_theorem_1_1_reconstruction.mdin full, as the premise that defines the pair family and the estimates (3)–(5).- The Statement of
wiki/problems/arithmetic_functions/E0694/_index.md. - The library card of the five-page note (card), its result page theorem_2_1 (Statement), and the held PDF at the card's path, pp. 4–5 on the rendered page images and in the text layer: Proposition 3.1 with its proof, read clause by clause and re-derived.
- The card of Ford (1998) and the held conversion: §1.3 (Theorem 8 and the sentence calling it a trivial corollary of the proof of Theorem 2) and §7 (the proof of Theorem 8 and the list of witnesses).
- The provenance paragraph of the card of Pollack, Pomerance and Treviño (2013) and, in the held conversion of the 17-page manuscript, the definition of a number convenient for a totient (its p. 1) and Lemma 4.1 with the first paragraph of its proof (§4).
docs/verification.md("Grading and claim standing", the shared audit checklist, "Whole-claim report", "Audit checklist"),docs/approach_vetting.md,docs/evidence.md("Source fidelity") anddocs/math_authoring.md.
Exposures. Five over-wide reads, none of which is a review, grade or
standing text of the section: (1) in E0694.md, the Status, Source,
References and Formalization paragraphs and the first two paragraphs of
"Current assessment" (the question as imported and the status-defining
source) came through a read that ran past the Statement; the section's
second sentence was checked against that Status paragraph, which the
assignment excludes, and the check is marked as such below; (2) the whole
card of the five-page note beyond its provenance paragraphs (read status,
contents, compiled scope, formal artifacts, bears-on and results);
(3) the Ford card's bears-on line and results list; (4) the summary
paragraph of the 2013 manuscript's card; (5) the Statements of
E0417.md and E0051.md, read to test the section's sentence about the
catalog.
Restatement
Notation as on the page: is the set of totient values in , , and are the least and greatest preimages of a totient , is the set of totients all of whose preimages are divisible by , and is Euler's function.
- S1 (target). Problem 694 asks to investigate over the totient values , the maximum restricted to .
- S2 (status characterization). The problem page records the site's status solved (Lean) with the qualification that the asymptotic rests on the five-page note's Theorem 2.1 and on two external Lean developments read as text, no refereed publication or independent review being held.
- S3 (obstruction). The reconstructed mechanism, the pair family of the write-up's Proposition 4.1 with its estimates (3)–(5) and the doubling-law and cluster-interval bookkeeping, gives nothing for the question, because (a) every retained pair supplies exactly one preimage of its value , so nothing in the family sees ; and (b) the values attaining the extreme ratio form a set that estimates of the form "all but totients " do not constrain.
- S4 (conditional transfer). Under the bounded-record premise of the Problem 417 section (the selected records satisfy , a premise stated in no held text), the mechanism gives: for every there is a constant, written here and in the Problem 417 section, such that for all large all but of the totients satisfy .
- S5 (catalog). No catalog problem asks for the statement S4.
- S6 (pointer). The statement S4 "is the object of Problem 417".
- S7 (the shared device). Proposition 3.1 of the note, as the section restates it: if , then for every prime the value is a totient with preimages and ; and this propagation is the multiplication by convenient integers behind Ford's Theorem 8 and Lemma 4.1 of the 2013 manuscript.
- S8 (propagation of the witness). The witness of Theorem 417.3 propagates the same way: for every prime , that is for every prime , the value carries the property that Theorem 417.3 uses at , membership in , as carries the collision in Proposition 3.1.
- S9 (outcome). The connection fails: the mechanism has no bearing on a question the page records as solved, and the shared device belongs to Ford's paper, not to the reconstructions.
Checklist
- Quantifiers and scope. Fails at S8. The exact-preimage property behind Ford's Theorem 8 holds for at least half of Ford's set and, in the form the 2013 manuscript attributes to Erdős, for almost all primes; S8 asserts it for every prime , the almost-all-to-all upgrade, and the witness below refutes it. Elsewhere pass: S4's "-proportion" is an eventual statement over , and its becomes by running the premise at .
- Circularity. Pass. The section proves nothing from its own conclusions; S3 and S9 are negative claims argued from the shape of the inputs.
- Model and convention changes. Pass with a flag at S7's identification (F2). The multiplication in Proposition 3.1 is by an arbitrary prime coprime to and uses only that and are preimages, while a multiplier is convenient for (the 2013 manuscript's definition, Erdős's notion) when has no preimages beyond the products of with the preimages of ; the section equates the two by vocabulary, and S8 is the consequence. The ratio convention (maximum over totient values) matches the problem's parenthetical and the note's . The renaming of as is a convention change without effect.
- Finite and statistical overreach. Pass. The section reports no computation and draws no statistical inference; the reviewer's enumeration below is exact and serves only as a counterexample.
- Uniformity. Pass. The only constant, , is stated with its dependence; the obstruction S3 involves no constants.
- Extremal conclusions. Pass. S1 is in the problem's own units; the sparseness of the extreme fibers behind S3(b) is derived below in those units (a lower bound on the fiber ratio forces a lower bound on for ).
- Consequences and composition. Fails at S8, a consequence sentence attached to S7 that does not follow from it. S4 inherits three premises, estimate (3) of (KK), the write-up's description of the family with its actual-values property, and the record bound; the section names the third and carries the first two only through the pointer to the Problem 417 section (F5). S9 follows from S3.
- Computation. Pass for the section, which has none. The reviewer's witness is hand-checkable: .
- Reproduction. Not applicable: the section states no rerun instruction or coverage claim.
- Source and verdict fidelity. Pass with two notes. Proposition 3.1 is restated faithfully against the page images of pp. 4–5; Theorem 8, the "trivial corollary" sentence and the witness list match Ford's §1.3 and §7; Lemma 4.1(ii) of the 2013 manuscript is exactly the convenient property. The notes: the 2013 manuscript attributes the convenient-number observation to Erdős, so "the shared device is Ford's" is loose (F4); and "Theorem 2.1 on its card" links the result page, not the card (F6). The status characterization S2 matches the page's Status paragraph, read only through the exposure declared above.
Weakest steps
1. S8, re-derived, fails. Take , , , so that and . Proposition 3.1 gives, for every prime , the preimages and of , both divisible by . Membership in needs every preimage divisible by . For , , and with ; also and . So although the collision propagates to it. For , with ; for , with prime. An exact enumeration of the preimages of (preimages listed by their largest prime factor; the routine was checked against a complete sieve of for every value up to ) over the primes finds for and only, where the preimages are exactly and ; every other in that range has a preimage coprime to . What does propagate is the collision, which is Proposition 3.1 with and is not the property Theorem 417.3 uses. The property that Theorem 417.3 uses propagates along the multipliers for which has only the preimages and , Ford's "at least half of the numbers " in §7, which is Theorem 8 itself and not the note's device.
2. S3(b), re-derived, holds. Let and let be a totient with ; write and . Since ,
for large , using (the note's p. 1) and the elementary bound (Lemma 1.1 of the note gives the constant). If has distinct prime factors , then with the -th prime (Mertens' product bound), so and for any fixed and large . An integer with at least distinct prime factors has a squarefree divisor with exactly of them, so their number is at most
for large , with . Hence the totients whose fiber ratio is at least number for every , while ; the extreme fibers are and lie inside the exceptional allowance of estimate (3) for every . Estimate (3) does not average anything; it tolerates an exceptional set, and the extreme fibers fit in it (F7). S3(a) is the actual-values bullet of the reconstruction page: and , one preimage per pair.
3. S4, re-derived, holds as a conditional. For a retained pair with core , value and the top prime exceeding every prime of , the integer is a preimage of , so
under the record bound , since . Estimate (3) with Step 2 of the reconstruction page ( by Chebyshev) leaves at most totients outside the family for large . This is the Problem 417 section's bullet with its constant ; the section under review writes for that constant. The deduction uses, besides the record bound, estimate (3) of (KK) and the write-up's description of the family (the actual-values property), which the abstract form of Proposition 4.1 on the reconstruction page does not carry.
Strongest attack
- S1. Compared clause by clause with the problem page's Statement (the maximum over of the form ). No gap.
- S2. Compared with the note's result page (Theorem 2.1, read depth "read in full", "nothing here is independently reviewed") and, through the declared exposure, with the page's Status paragraph. The attack looked for a standing claim stronger than the page records; there is none.
- S3. The attack: collisions inside the pair family, two pairs with , do exhibit two preimages and of one value, so the family is not blind to multiple preimages. It fails because the ratio of two such preimages is divided by the same expression for the other pair, at most over the selected records, bounded under the record premise and in any case tied to the records and not to ; and estimate (4) makes such collisions , the same order as the extreme fibers (Weakest step 2), so no counting statement of the form (3)–(5) can reach the value , whose upper bound is the extremal order of and whose lower bound is a Linnik-prime construction.
- S4. The attack looked for a case where the retained pair's product is not a preimage () or where the family's values leave ; both are excluded by the family's definition (; the top prime exceeds every prime of the record). The remaining weakness is the premise set, which the section carries by pointer; the conditional is stated as conditional.
- S5. The candidates in the catalog are Problems 417, 51 and 694. Problem 417 asks whether exists and exceeds , which by Lemma 417.1(a) concerns the totients with ; a typical bound with constrains none of them, as the Problem 417 section records. Problem 51 asks whether along an infinite set of totients, which a typical bound leaves open in both directions. Problem 694 is S1. The sentence survives for these; the catalog beyond the problems the page's search names was not read.
- S6. Not a mathematical claim; read literally it conflicts with the Problem 417 section's own verdict that the typical-ratio statement "gives again only " (F3).
- S7. Proposition 3.1 re-derived: for a prime , , the values are distinct for distinct , and ; this matches pp. 4–5 of the note. The identification with the convenient-integer device is where the attack lands: Ford's §7 proof of Theorem 8 needs that "has only the pre-images ", the 2013 manuscript's Lemma 4.1(ii) needs convenient for and , and neither clause is in Proposition 3.1, which needs only existence. The identification is a vocabulary match of the operation, not an entailment; it is not false as a description of the operation, and it is what leads to S8 (F2).
- S8. Refuted by ; see Weakest step 1. The alternative reading, that only the collision between and propagates, is Proposition 3.1 itself and says nothing about the witness property of Theorem 417.3, so it does not rescue the sentence (F1).
- S9. The attack on "no bearing" is S3's attack and fails. The attribution "Ford's" is loose: the 2013 manuscript (p. 1) attributes the observation, and the almost-all-primes theorem, to Erdős and calls its Lemma 4.1 a variant proved by Ford's methods; Ford's §7 uses the device for Theorem 8. The substantive clause, that the device is not the reconstructions', stands (F4).
Premises
- Proposition 4.1 of the write-up and the pair family (estimates (3)–(5), the pairs , the actual-values property), from the Theorem 1.1 reconstruction at the subject commit: author-recorded; the proposition is imported from an accepted Lean file that is not held, and the family description is the write-up's prose. Read in full. Used within its hypotheses in S3 and S4; the review notes that the actual-values property is part of the family description, not of the abstract proposition.
- Chebyshev's bound (the page's notation; the reconstruction page's imported input), used in Weakest step 2.
- Theorem 417.3 and the bounded-record premise, from the Problem 417 section of the same page: author-recorded, read at interface level (statement, Step 1, Step 2, the pair-family bullet). The witness was confirmed by exact enumeration. Their proofs are another reviewer's subject.
- Proposition 3.1 of the five-page note, held PDF at the card's path, pp. 4–5, read on the page images and in the text layer; statement and proof re-derived. Standing: author-recorded on the card; no refereed publication is held.
- Theorem 2.1 of the note, statement only, from the result page; its proof was not read, and nothing here depends on it beyond the size bound and Lemma 1.1, used in Weakest step 2 and taken at statement level from the result page.
- Ford (1998), Theorem 8, held conversion §1.3 (statement; "a trivial corollary to the proof of Theorem 2") and §7 (the proof: for at least half of the totient has only the preimages ; the witnesses , , , and ). Refereed; statement level; the proof in §5 was not read.
- Pollack, Pomerance and Treviño (2013), Lemma 4.1 and the definition of "convenient for " (p. 1 of the held 17-page manuscript): a number is convenient for a totient with preimages when is a totient with preimages and no others; the manuscript attributes to Erdős that for each fixed totient almost all primes are convenient for , and Lemma 4.1 gives integers with , convenient for two given totients, and . Statement level; the almost-all-primes attribution is used here only as the source's characterization, not as an input to any verdict.
- Mertens' product bound and the prime-reciprocal sum , standard, used in Weakest step 2 only.
- Problem statements of E0694 (target), E0417 and E0051 (for S5).
Findings
- F1 (required). Location: lines 513–514, "and the witness of Theorem 417.3 propagates the same way." Defect: read with the propagation just described, to for every prime , the sentence asserts for every prime , and that is false; the property Theorem 417.3 uses at propagates only along convenient multipliers, whose existence in quantity is Ford's Theorem 8 and not the note's Proposition 3.1. Witness: , , , (also and ); , , ; , . Among the primes , only and give . Replacement: "The witness of Theorem 417.3 does not propagate this way: lies in only when is convenient for , and shows that is not. The propagation Theorem 417.3 would need is the exact-preimage clause of Ford's §7, which is Theorem 8 itself."
- F2 (suggested). Location: lines 510–513, "The one shared device is the note's Proposition 3.1, that a collision ... propagates to the values for primes : this is the multiplication by convenient integers behind Ford's Theorem 8 and the Problem 49 folder's Lemma 4.1". Defect: Proposition 3.1 uses only that and are preimages, for every prime ; a convenient multiplier (the 2013 manuscript's definition) is one for which these products are all the preimages, and that clause, the whole content of Ford's §7 argument and of Lemma 4.1(ii), is absent from Proposition 3.1. The identification is by vocabulary; F1 is its consequence. Witness: the same , where the collision propagates to (preimages and ) while has seventeen further preimages. Replacement: "The one shared device is the existence half of the multiplication by convenient integers behind Ford's Theorem 8 and the Problem 49 folder's Lemma 4.1: the note's Proposition 3.1 observes that a collision gives the preimages and for every prime , and needs nothing about the other preimages of , whose absence is what 'convenient' means."
- F3 (suggested). Location: lines 509–510, "which no catalog problem asks and which is the object of Problem 417." Defect: Problem 417 asks whether exists and exceeds , which concerns the totients with ; the Problem 417 section itself records that the typical-ratio statement "gives again only ", so the statement is not that problem's object, and the two clauses read as contradicting each other. Witness: the page's own pair-family bullet (lines 262–271). Replacement: "which no catalog problem asks: Problem 417 concerns the totients with , which an upper bound on typical least preimages does not reach (the Problem 417 section's pair-family bullet), and Problem 51 asks whether is unbounded along an infinite set, which a typical bound leaves open."
- F4 (note). Location: lines 516–517, "the shared device is Ford's". The 2013 manuscript (p. 1) attributes the convenient-number observation and the almost-all-primes theorem to Erdős and describes its Lemma 4.1 as a variant proved with Ford's methods; Ford's §7 uses the device for Theorem 8. Replacement: "the shared device is Erdős's, as Ford's Theorem 8 and the 2013 manuscript use it, not the reconstructions'."
- F5 (note). Location: lines 506–509. Three small imprecisions in the conditional: the constant is in the Problem 417 section and here, the same symbol for different constants (harmless, since neither is specified); "for all but an -proportion of totients" lacks its range, all but of the totients for all large ; and the premise set beyond the record bound, estimate (3) of (KK) together with the write-up's description of the family, is carried only by the pointer to the Problem 417 section. Replacement: "a typical-ratio statement, for all but of the totients , under (KK) and the write-up's family as the Problem 417 section states them".
- F6 (note). Location: line 499, "Theorem 2.1 on its card". The link
resolves to the result page
theorem_2_1, not to the card. Replacement: "Theorem 2.1 on its result page". - F7 (note). Location: lines 505–506, "the extreme fibers that (3)–(5) average away". The estimates tolerate an exceptional set of values; they do not average. The extreme fibers number at most for some (Weakest step 2), so they fit inside that allowance. Replacement: "the extreme fibers, a set of values that lies inside the exceptional allowance of (3)".
Verdict
- S1: refutation-failed. The target is stated in the problem's own units.
- S2: refutation-failed. The characterization matches the result page and, through the declared exposure, the page's Status paragraph.
- S3: refutation-failed. The pair family supplies one preimage per value, and the extreme fibers are , inside the allowance of estimate (3); the collision attack fails.
- S4: refutation-failed, as a conditional whose constant is the Problem 417 section's renamed; its premise set is named by pointer (F5).
- S5: refutation-failed for Problems 417, 51 and 694; the rest of the catalog was not read.
- S6: not a claim; an informal pointer whose literal reading conflicts with the Problem 417 section (F3).
- S7: refutation-failed for the restatement and proof of Proposition 3.1; the identification with the convenient-integer device is a vocabulary match that omits the exact-preimage clause (F2).
- S8: refuted-as-stated. Witness : with not divisible by , so ; the property of the witness used by Theorem 417.3 does not pass to for every prime .
- S9: refutation-failed for "no bearing" and for "not the reconstructions'"; the attribution to Ford is loose (F4).
Limitations. The section is a connections note, and S3, S5 and S9 are negative claims; the review attacked them with the strongest positive route it could find (collisions inside the pair family; the statements of Problems 417 and 51) and reports that those attacks fail, which is not a proof that no route exists. The proofs of (F), (F8), (KK), of Theorem 417.3 and of the note's Theorem 2.1 were not reviewed here; the section uses them at their stated interfaces, and the one place where it uses an interface beyond its strength is S8. The enumeration behind F1 covers the primes ; the refutation needs only , which is checkable by hand. This focused review assigns no tier and changes no status.