{"id":"6a418c2e-3ee3-4c8f-bf1d-e4c30923a6f1","arxiv_id":"2506.16433","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"An inhabited complemented subset of the natural numbers has a least element exactly when it is downset located, proved with a new coinductive well-foundedness principle DWF_N.","lead":"This constructive mathematics paper introduces a coinductive version of well-foundedness for the natural numbers and uses it to prove a constructive least number principle for complemented subsets. The payoff is a positive, negation-free condition, downset locatedness, that exactly characterizes when a complemented subset has a least element.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 5.6 is proved in MIN+DWF_N, not in MIN: DWF_N requires strong induction/EFQ, and the 0 in A1 case of CLNP adds a non-minimal disjunctive syllogism in Cor 5.5(iii).","rationale":"The reader's weakest assumption correctly identifies DWF_N as the load-bearing gap: the main theorem's proof is conditional on a principle that is not established within minimal logic. My read does not change the verdict: the conditional statement (MIN + DWF_N implies CLNP for a1 > 0) appears valid, and the 0 in A1 case is additionally entangled with a non-minimal disjunctive syllogism. The paper should state Theorem 5.6 with DWF_N as an explicit hypothesis, or prove DWF_N in MIN, and should repair or qualify Cor 5.5(iii) and the full CLNP. This is a genuine correctness risk for the abstract's minimal-logic claim, but not a fatal flaw in the mathematical content once the extra premise is acknowledged. Hence I reaffirm the CONDITIONAL verdict.","tokens_in":18415,"tokens_out":14455,"duration_ms":140708,"concrete_test":"Formalize the proof of Theorem 5.6 in a proof assistant with a minimal-logic fragment (e.g., Coq with ex falso excluded, or Agda without absurd elimination), removing DWF_N from the axiom list. If the (ii)->(i) direction cannot be derived from Peano axioms and order axioms alone, then DWF_N is an extra premise and the 'within MIN' claim fails; re-run with DWF_N as an explicit hypothesis to confirm the theorem holds conditionally.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central constructive least number principle CLNP is claimed to be proved 'within minimal logic', but the proof of Theorem 5.6(ii)->(i) invokes the scheme DWF_N directly: 'Hence, by DWF_N there is x...' (Section 5, formal proof). DWF_N is not derived in the paper from the stated minimal-logic axioms. Proposition 3.1(i) proves DWF_N from strong induction @WF_N, and the paper explicitly notes that IND_N -> @WF_N requires EFQ at the base case (the proof of P(0) from the vacuous hypothesis uses K->P(0)). Thus within MIN, DWF_N is an unproved extra premise. The abstract's 'within minimal logic' claim is therefore only supported as 'within MIN plus DWF_N'. Additionally, the full CLNP covering the case 0 in A1 depends on Cor 5.5(iii), whose proof uses a disjunctive syllogism: from x in A1 or x in A0 and not(x in A1), it infers x in A0. This step is not valid in minimal logic without EFQ. If DWF_N is accepted as a primitive coinductive principle, the equivalence is a valid conditional theorem, but the claim that CLNP is proved within minimal logic is overstated and should be qualified or the missing derivation supplied.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces a coinductive well-foundedness scheme DWF_N for the natural numbers, a 'dual' to induction whose conclusion is existential and whose hypothesis allows a backward descent step. It then states and proves CLNP: an inhabited complemented subset A of N has a least element if and only if it is downset located. The paper also generalizes DWF_N to D-well-founded sets, proves several preservation properties (embeddings, restrictions, products, coproducts, lexicographic products, and Sigma-sets), and presents a case study on divisibility by primes. The central claimed logical strength is that CLNP is proved within minimal logic, with DWF_N as a constructive descent principle.","tokens_in":18774,"tokens_out":6718,"duration_ms":67144,"significance":"If the logical claims are corrected, the paper makes a useful contribution. DWF_N is a clearly described, algorithmically meaningful descent scheme, and the equivalence between least-element existence and downset locatedness for complemented subsets is a genuine positive reformulation of the classical least number principle. The generalization to D-well-founded sets, with preservation under products, sums, lexicographic products, and Sigma-sets, is a coherent and instructive development. The paper is, however, not machine-checked, and its central 'within minimal logic' claim is not supported as stated; the results are best read as theorems of minimal logic plus the explicitly named scheme DWF_N together with certain disjunctive-syllogism instances.","major_comments":[{"comment":"The claim that CLNP (Theorem 5.6) is proved 'within minimal logic' is not supported as stated. The formal direction (ii) to (i) invokes DWF_N directly ('Hence, by DWF_N there is x...'), and DWF_N is not derived from the stated minimal-logic axioms. Proposition 3.1(i) derives DWF_N only from the strong induction scheme @WF_N, and the paper itself notes that IND_N to @WF_N requires EFQ at the base case. Theorem 5.6 is therefore a theorem of MIN plus the additional scheme DWF_N, not of MIN alone. Please either supply a derivation of DWF_N within MIN, or state the abstract and theorem with the explicit extra axiom DWF_N.","section":"Abstract; Section 3, Proposition 3.1; Section 5, Theorem 5.6"},{"comment":"The proof of Corollary 5.5(iii), which is used for the '0 in A1' case of CLNP, is not minimal. From x in A1 or x in A0 and the derived not(x in A1), the proof concludes x in A0. This is a disjunctive syllogism, which is not derivable in minimal logic without an explosion principle. Since the full if-and-only-if statement of CLNP covers inhabited complemented subsets with 0 in A1, this is a second place where the 'within MIN' claim requires a non-minimal step.","section":"Section 5, Corollary 5.5(iii)"}],"minor_comments":[{"comment":"Proposition 2.1 is labelled (MIN), but its step from 0 in A_P, i.e. (0=1) or (0=0 and P), together with 0 not equal to 1, to P is again a disjunctive syllogism. Since this proposition is not used in the proof of the main theorem, it should be restated with the needed assumption or explicitly relegated to a remark about non-minimal logical strength.","section":"Section 2, Proposition 2.1"},{"comment":"There are several typographical errors that should be corrected in a revision, including 'Generealising' in the abstract, 'anrgument' in Section 3, 'tohether' and 'ther is' and 'exluded' in Section 5, and 'disjumction' in Section 6.","section":"Abstract and throughout"},{"comment":"The informal proof of (ii) to (i) describes a descent of at most a1+1 steps, but the formal proof delegates termination to DWF_N. It would improve clarity to state explicitly that DWF_N is being used as a primitive descent axiom in this proof, rather than as a consequence of the minimal-logic framework.","section":"Section 5, formal proof of Theorem 5.6"}],"recommendation":"major_revision","confidential_remarks":"The main issue is the overstatement of the logical strength: the central theorem is proved in MIN plus DWF_N, with an additional non-minimal step in the 0-in-A1 case. This is fixable by qualification or by supplying the missing derivation. I see no novelty or citation-practice concern; the heavy reliance on the author's own BST framework is disclosed and is normal for this line of work."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: there's a real idea here—a positive, negation-free least-number principle for complemented subsets of N, with a coinductive descent principle doing the work—but the advertised 'minimal logic' proof is not what the paper actually delivers. The main theorem is a conditional in MIN + DWF_N, and one case of the full CLNP uses a disjunctive syllogism that minimal logic doesn't allow.\n\nThe genuinely new bits: DWF_N (a descent scheme: if Q is inhabited and every Q point either satisfies P or has a smaller Q point, then P is inhabited) and the equivalence in Theorem 5.6 that a complemented subset with a1>0 has a least element iff it is downset located. That's a clean, positive counterpart to LNP, in the same spirit as locatedness for suprema. Section 6 generalizes to D-well-founded sets and gives closure properties (subsets, product, sum, Sigma-type) that look correct in the intended semi-formal framework. The analogy is apt and the positive formulation is a real improvement over negated formulations.\n\nThe soft spots are the logical hygiene claims. The stress-test is right: Proposition 3.1(i) proves DWF_N from strong induction @WF_N, and the paper itself notes IND_N → @WF_N needs EFQ at the base case (the vacuous proof of ∀y<0 P(y) uses K_N → P(y), which is exactly ex falso). So within MIN, DWF_N is an extra axiom, not a consequence. The formal proof of (ii)→(i) in Theorem 5.6 invokes DWF_N directly, so the theorem is proved in MIN + DWF_N, not MIN. Separately, Corollary 5.5(iii) derives x∈A0 from x∈A1∨x∈A0 and ¬(x∈A1); that's disjunctive syllogism, invalid in minimal logic. The full CLNP covering the case 0∈A1 leans on this. So the abstract overstates the logic.\n\nNone of this kills the mathematical content. If DWF_N is accepted as a primitive coinductive principle (or as a consequence of strong induction in intuitionistic logic), the equivalence is solid. The paper would be improved by stating Theorem 5.6 as 'within MIN plus DWF_N', by flagging Corollary 5.5(iii) as requiring intuitionistic (or classical) logic, and by making the dependence on earlier BST works explicit enough that a referee can check the key steps without reading the habilitationsschrift.\n\nWho should read it: constructive mathematicians and proof theorists interested in descent principles. It deserves a serious referee; the logic claims need revision, but the core idea is worthy. I'd send it to review with a request to fix the minimal-logic framing.","headline":"Genuinely new positive least-number principle for complemented subsets, but the advertised 'within minimal logic' proof is overstated: DWF_N is an extra premise in MIN, and Cor 5.5(iii) uses disjunctive syllogism.","tokens_in":19295,"tokens_out":5189,"would_cite":false,"duration_ms":48340,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03F65","03B20"],"pacs":[],"model":"deepseek-v4-flash","headline":"An inhabited complemented subset of the natural numbers has a least element exactly when it is downset located, proved by a coinductive descent principle in minimal logic.","keywords":["coinductive well-foundedness","least number principle","complemented subsets","minimal logic","downset located","descent principle","natural numbers","constructive mathematics"],"falsifier":"Build a Kripke model of minimal arithmetic containing a complemented subset $A=(A_1,A_0)$ with a prover $a_1>0$ such that downset locatedness holds at every stage but no element is least across all stages; if $\\mathrm{DWF}_{\\mathbb{N}}$ is valid in the model, the theorem's conclusion would fail, and such a model would show exactly where the descent scheme is doing the work.","tokens_in":18146,"feed_emoji":"⬇️","tokens_out":15657,"duration_ms":132997,"temperature":0.7,"pith_summary":"The paper sets out to make the least number principle constructive by replacing the classical “every nonempty subset of $\\mathbb{N}$ has a least element” with a positive statement about complemented subsets: an inhabited complemented subset $A$ has a least element if and only if it is downset located. The work is carried out in minimal logic, with the coinductive descent scheme $\\mathrm{DWF}_{\\mathbb{N}}$ doing the work that the classical principle does by choosing a minimum. A sympathetic reader should care because the equivalence turns an existence assertion into a checkable local condition, and the proof of the “if” direction is a terminating descent algorithm: from any prover in $A$, either a smaller prover exists or the current element is least. The same scheme is then generalised to arbitrary sets with an inequality and an order, where it yields a coinductive notion of well-foundedness.","feed_headline":"Descent rule makes the least-number principle constructive","feed_subtitle":"Least elements for complemented subsets of the natural numbers are exactly the downset-located ones, proved in minimal logic.","key_machinery":"The central object is the scheme $\\mathrm{DWF}_{\\mathbb{N}}$, a coinductive, existential counterpart to strong induction on $\\mathbb{N}$. It states that if a predicate $Q$ is inhabited and every $x$ satisfying $Q$ either satisfies $P$ or has a smaller $y$ satisfying $Q$, then some $x$ satisfies $P$. This scheme carries the argument by encoding a descent algorithm: start at a witness of $Q$, and whenever the current element does not satisfy $P$, move to a strictly smaller witness of $Q$, so after finitely many steps a $P$-witness is reached. Complemented subsets $A=(A_1,A_0)$ supply the positive vocabulary: elements of $A_1$ are provers, elements of $A_0$ refuters, and downset locatedness is exactly the local hypothesis that lets $\\mathrm{DWF}_{\\mathbb{N}}$ start the descent from any chosen prover.","core_discovery":"The central claim is Theorem 5.6: for a complemented subset $A=(A_1,A_0)$ of $\\mathbb{N}$ with $a_1\\in A_1$ and $a_1>0$, $A$ has a least element if and only if it is downset located. Downset located means that for every prover $x\\in A_1$, either the whole downset $D_A(x)=\\{y\\in A_1\\cup A_0\\mid y<x\\}$ is contained in the refuter part $A_0$, or some element of the downset is itself a prover. Under this condition, the descent scheme $\\mathrm{DWF}_{\\mathbb{N}}$ produces the least element: starting from $a_1$, if the downset is not entirely in $A_0$, a smaller prover is found, and the scheme guarantees the search terminates. Conversely, a least element forces the disjunction at every prover. The paper also states the constructive least number principle CLNP for every inhabited complemented subset of $\\mathbb{N}$, notes that classically it is equivalent to the ordinary least number principle, and proves it within minimal logic.","pith_inferences":["A testable extension: the same equivalence may hold for any dichotomous, strong D-well-founded order, with downset located defined using that order's provers and refuters; checking it on a lexicographic product would show whether the descent principle composes as cleanly as the closure theorems suggest.","The proof suggests the computational content of the least number principle is a bounded linear search rather than a global minimum oracle: Theorem 5.6 can be read as saying that a starting prover plus downset locatedness is enough to compute the least element in at most $a_1+1$ descent steps.","Because the paper's constructive justification of $\\mathrm{DWF}_{\\mathbb{N}}$ passes through strong induction and an ex-falso step, a natural next question is whether CLNP can be derived from a weaker descent principle; a realizability model separating the two would locate the exact logical strength needed."],"forward_implications":["The classical least number principle becomes a constructively valid equivalence: an inhabited complemented subset of $\\mathbb{N}$ has a least element exactly when it is downset located, so the existence of a least element can be verified locally.","The descent scheme $\\mathrm{DWF}_{\\mathbb{N}}$ gives a terminating algorithm for finding the least element: from any prover, each non-terminal step produces a strictly smaller prover, bounding the search by the initial element.","Arithmetic facts classically proved by choosing a least counterexample, such as the existence of a prime divisor of a composite number, can be proved in minimal logic using $\\mathrm{DWF}_{\\mathbb{N}}$ instead of the least number principle.","The generalisation to arbitrary sets with an inequality and an order yields D-well-founded sets, and these are closed under images, substructures, products, sums, lexicographic products, and indexed sums, giving a toolbox for coinductive well-foundedness.","Within $\\mathrm{DWF}_{\\mathbb{N}}$, every sequence in $\\mathbb{N}$ has a term no larger than its successor; classically the principle is equivalent to the absence of infinite descending sequences."],"supporting_citations":[{"why":"It supplies the constructive analytic framework and the order-locatedness formulation for least upper bounds that motivates CLNP.","marker":"[4]"},{"why":"It introduces the complemented subsets on which CLNP is stated.","marker":"[2]"},{"why":"It provides the set-theoretic foundations used for the formal proofs.","marker":"[20]"},{"why":"It gives the classical least number principle and the relationship between strong induction and well-foundedness that DWF_N is compared with.","marker":"[29]"},{"why":"It records that the classical least upper bound principle implies excluded middle, the parallel obstruction that a locatedness reformulation avoids.","marker":"[6]"}],"fun_headline_variants":["Coinductive descent for constructive least-number principle","Least elements from coinductive well-foundedness","Downset-located sets have least elements","Minimal logic proves least-number principle coinductively","Coinduction replaces induction for least numbers"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the descent scheme $\\mathrm{DWF}_{\\mathbb{N}}$ is a valid principle: termination of the descent is delegated to it, and its constructive justification, along with the case $0\\in A_1$, invokes the ex-falso rule that a contradiction proves anything.","fun_headline_variants_meta":{"raw":{"variants":["Coinductive descent for constructive least-number principle","Least elements from coinductive well-foundedness","Downset-located sets have least elements","Minimal logic proves least-number principle coinductively","Coinduction replaces induction for least numbers"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000905,"raw_usage":{"total_tokens":3852,"prompt_tokens":865,"completion_tokens":2987,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":481,"completion_tokens_details":{"reasoning_tokens":2916}},"tokens_in":481,"tokens_out":2987,"duration_ms":20531,"temperature":1.0,"reasoning_tokens":2916,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T19:31:58.636564+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Build a Kripke model of minimal arithmetic containing a complemented subset $A=(A_1,A_0)$ with a prover $a_1>0$ such that downset locatedness holds at every stage but no element is least across all stages; if $\\mathrm{DWF}_{\\mathbb{N}}$ is valid in the model, the theorem's conclusion would fail, and such a model would show exactly where the descent scheme is doing the work.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"It records that the classical least upper bound principle implies excluded middle, the parallel obstruction that a locatedness reformulation avoids."}],"review_version":1}