{"id":"af76c5d6-2443-416a-832a-dd0a4a4f059d","arxiv_id":"2412.03203","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Four new axioms for homotopy type theory, modeling light condensed sets, suffice to develop synthetic topology and prove Brouwer's fixed-point theorem, with all functions continuous on the interval.","lead":"This paper sets up a new axiomatic foundation in homotopy type theory for reasoning about light condensed sets, a framework from Clausen and Scholze. It shows that from four axioms one can prove classical-looking principles like Markov's principle and LLPO, and then prove topological theorems such as Brouwer's fixed-point theorem internally.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Validity of the Local choice axiom in the intended model is unproved; the derived results rest on it, so the central claim remains conditional.","rationale":"I read the paper in good faith and found the proofs broadly coherent; I did not identify an internal inconsistency in the axiom system. The weakest point is exactly what the reader flagged: the validity of the four axioms in the topos of light condensed sets is not proved. Among the axioms, Local choice is the most load-bearing because it is a strong choice principle used in the cohomology arguments and the Σ-closure of compact Hausdorff spaces, both needed for the final fixed-point theorem. The paper itself concedes that not all properties of light condensed sets are internally valid, citing Wärn, which underscores that the intended model could fail an axiom. Since the reader's conditional verdict already reflects this uncertainty, my stress-test does not change the verdict. A concrete way to settle the concern is to check Local choice in the model, for example by testing it on the specific non-split surjection from Lemma 1.4.5. Until such a model verification is provided, the central claim should remain conditional.","tokens_in":18484,"tokens_out":31704,"duration_ms":311258,"concrete_test":"Verify the axioms in the intended model by constructing a model of HoTT in the topos of light condensed sets (e.g., via the constructive sheaf models of [CRS21]) and checking each of the four axioms, with special attention to Local choice. A more targeted test: take the non-split surjection s : N∞+N∞ → N∞ from Lemma 1.4.5 and check internally whether there exists a Stone cover q : T → N∞ such that s has a section over T. If no such cover exists, Local choice fails in light condensed sets, and the central claim is unsupported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central claim is that the four axioms of §1.2 capture the internal logic of the higher topos of light condensed sets, and that the internally proved theorems (Markov's principle, continuity of all functions on I, H^1(S,Z)=0, Brouwer's fixed-point theorem) are therefore facts about condensed sets. This requires the axioms to be valid in that model, but the paper does not prove this; it only conjectures completeness and suggests a constructive metatheory justification [CRS21]. The most load-bearing and least secure axiom is Local choice: it asserts that every type family over a Stone space that is pointwise merely inhabited is selected on a Stone cover. This is a strong choice principle, and its validity in light condensed sets is not demonstrated. It is used essentially in Lemma 4.2.2 (CHaus closed under Σ) and Lemma 6.2.3 (H^1(S,Z)=0), which in turn underpin the Čech-cohomology comparison (Theorem 6.3.5) and the proof of Brouwer's fixed-point theorem (Theorem 6.5.10). If Local choice fails in the intended model, those results do not express facts about light condensed sets. The paper's own warning that Wärn found an internally invalid property of abelian groups in this setting shows that internal validity is not automatic, making this a real gap rather than a technicality.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops a synthetic form of Stone duality in homotopy type theory by adjoining four axioms: Stone duality, surjections are formal surjections, local choice, and dependent choice. On this axiomatic basis it proves Markov's principle, LLPO, and the negation of WLPO; introduces a synthetic topology via open and closed propositions; establishes that Stone and compact Hausdorff types have the expected closure properties; shows that every function from the unit interval to itself is continuous in the epsilon-delta sense; and derives a Čech-cohomology comparison theorem leading to an internal proof of Brouwer's fixed-point theorem. The manuscript presents this development as capturing the internal logic of the higher topos of light condensed sets, but it does not prove that the four axioms are valid in that model; the completeness of the axiom system is only conjectured, and the intended justification in a constructive metatheory is left to future work.","tokens_in":18708,"tokens_out":8820,"duration_ms":79851,"significance":"If the four axioms really are valid internally in the topos of light condensed sets, this is a significant contribution: it would give a compact HoTT-level foundation from which strong constructive principles and nontrivial topological and cohomological theorems follow. The paper is honest about its limitations, explicitly records Wärn's example of a non-internally-valid property, and contains many non-formal but plausible proofs. The strongest aspects are the axiomatic derivation of Markov's principle, LLPO and ¬WLPO; the synthetic treatment of Stone and compact Hausdorff spaces; and the use of higher types to prove Brouwer's fixed-point theorem. The main weakness is semantic: the central claim that the axioms hold in light condensed sets is not established, and several compressed arguments (the interval definition, a compactness step in Lemma 4.1.4, and the use of local choice in Lemma 6.2.3) need to be supplied before the reader can fully trust the results. No machine-checked formalization is provided; that is not a defect for a mathematical paper, but it makes these compressed steps more consequential.","major_comments":[{"comment":"The paper's central interpretational claim is that the four axioms in §1.2 are internally valid in the topos of light condensed sets. This claim is not proved; the introduction only conjectures completeness and refers to future work [CRS21]. In particular, Local choice is a strong choice principle, and its validity in the intended model is not demonstrated. This is load-bearing: Local choice is used essentially in Lemma 4.2.2 and in Lemma 6.2.3, which underlie Theorem 6.3.5 and Theorem 6.5.10. The authors themselves note (Introduction) that Wärn found a property of light condensed sets that is not internally valid, so internal validity is not automatic. Please either prove validity of Local choice in the intended model or explicitly reframe the paper's theorems as conditional on the four axioms, with the condensed-set interpretation stated as a conjecture.","section":"Introduction and §1.2 (Axiom Local choice)"},{"comment":"The unit interval I is not formally defined as a type. The text says it can be defined using Cauchy or Dedekind reals and then cites [BB85], but these constructions are not equivalent in general HoTT, and the later theorems—Theorem 5.0.9 and Theorem 6.5.10—depend on the choice. Please specify the exact type constructor used for I, prove or cite that cs : 2^N → I is surjective, and make precise the sense in which the topology on I is generated by open intervals (the step leading to Theorem 5.0.9).","section":"§5 (Definitions 5.0.1–5.0.3 and Theorem 5.0.4)"},{"comment":"The proof of Lemma 4.1.4 asserts 'there is some k : N with ⋁_{n≤k} c_n = 1' from 0 = 1 in B/(c_n)_{n:N}. This is a finiteness/compactness property of countably presented Boolean algebras that is not proved or referenced, and it is not automatic in a constructive metatheory. Lemma 4.1.4 is used in Corollary 4.1.5 and Lemma 4.3.4, so the missing argument is load-bearing. I suggest making this step a separate lemma with a complete proof.","section":"§4.1, Lemma 4.1.4"},{"comment":"The proof of Lemma 6.2.3 is too compressed: 'We use local choice to get T : S → Stone such that ∏_{x:S}||T_x|| with β : ∏_{x:S}(α(x) = ∗)^{T_x}' skips the construction of the family T from α and the verification that local choice applies to the relevant propositional family. Since Lemma 6.2.3 is what yields H^1(S,Z)=0 and enters Theorem 6.3.5, the full construction should be written out.","section":"§6.2, Lemma 6.2.3"},{"comment":"The proof of Brouwer's fixed-point theorem is a sketch. The existence and uniqueness of the intersection point r(x) of the line H_x(t) = f(x) + t·d_x with S^1 is asserted via 'exactly one solution' of a quadratic equation, but the constructive justification is not given, and the verification that the resulting map r : D^2 → S^1 preserves S^1 and is a retraction is only stated. Please expand this proof or supply the missing analytic lemmas with precise references to [BB85].","section":"§6.5, Theorem 6.5.10"}],"minor_comments":[{"comment":"The formula for d1 has a typo: it reads '+ βx(u,w)' at the end, but the standard coboundary formula requires '+ βx(u,v)'.","section":"§6.1, Definition 6.1.1"},{"comment":"In the proof, after fixing n as the index of the sequence, the text writes 'α(n) = β(0,1)+...+β(n−1,n)' using n again for a point of I_n; this clashes with the outer n and should be rewritten with a fresh variable.","section":"§6.4, Lemma 6.4.2"},{"comment":"There is a missing closing parenthesis in the statement: 'Sp(2/(αn)n:N' should be 'Sp(2/(αn)n:N)'.","section":"§1.1, Lemma 1.1.9"},{"comment":"There are a few typos, for example 'Hausforff' should be 'Hausdorff'.","section":"Introduction"},{"comment":"Lemma 5.0.7 is stated without proof; in a constructive setting this deserves at least a one-sentence justification or reference, since it is used to identify open subsets of I with countable unions of open intervals.","section":"§5, Lemma 5.0.7"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is promising and the axiomatic development is largely coherent, but the semantic claim connecting the axioms to light condensed sets is not yet established. If the journal is willing to publish a purely axiomatic development with the condensed-set interpretation explicitly marked as conjectural, the conditional framing may be acceptable. My recommendation of major revision is driven mainly by the unproved validity of Local choice and by the compressed interval and cohomology arguments; these are fixable with expansion and reframing."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"This is a real contribution, not a stunt. The four axioms in §1.2 are new, and the authors show they are strong enough to prove Markov's principle, LLPO, and the negation of WLPO (Theorems 1.4.1–1.4.4). The development of open and closed propositions, the characterization of closed subtypes of Stone spaces, the proof that all functions on the unit interval are epsilon-delta continuous (Theorem 5.0.9), and the internal proof of H^1(I,Z)=0 and Brouwer's fixed-point theorem (Theorems 6.4.3 and 6.5.10) are substantial and non-trivial. The paper is well-organized and the proofs are broadly coherent, and the authors are honest about the limits: they explicitly say the system is conjectured to be complete for internally valid properties and that justification in a constructive metatheory is future work. Credit is also due for flagging Wärn's counterexample, which shows internal validity is not automatic.\n\nThe main soft spot is exactly what the stress-test note says: the axioms, especially Local choice, are not proved to hold in the higher topos of light condensed sets. This is the load-bearing assumption. If Local choice fails there, the theorems about Stone covers, the Čech cohomology comparison, and ultimately Brouwer's fixed-point theorem do not express facts about condensed sets. That is a real gap, but it is not a hidden one. The paper frames itself as a proposed foundation, and the internal mathematics is developed from the axioms in a way that makes the dependency clear. I do not see a circularity problem: the theorems are genuine consequences of the axioms, not restatements of the model.\n\nA few smaller issues: several compactness steps (e.g., Lemma 4.1.4) are asserted with shortcuts, and there is no machine-checked verification. These are places where errors could hide, but they are the normal kind of referee-level gaps, not obvious flaws. The constructive-analysis background for the interval is used lightly, but the claims there look consistent with the cited literature.\n\nWho is this for? People working in HoTT, synthetic topology, or condensed mathematics who want an internal language for light condensed sets. It deserves a serious referee: the question of whether the axioms are valid in the intended model is exactly the kind of thing a specialist should check. The paper is not yet a definitive foundation, but it is a solid candidate that advances the program.","headline":"A genuinely new axiomatic foundation for synthetic topology in HoTT, with real internal theorems, but its validity in the intended model of light condensed sets is conjectured rather than proved.","tokens_in":19267,"tokens_out":1242,"would_cite":true,"duration_ms":14156,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B38","03F65"],"pacs":[],"model":"deepseek-v4-flash","headline":"Four axioms on top of homotopy type theory yield a synthetic topology for light condensed sets in which all functions are continuous and Brouwer's fixed-point theorem is provable.","keywords":["homotopy type theory","light condensed sets","synthetic topology","Stone duality","compact Hausdorff spaces","Brouwer fixed-point theorem","Markov's principle","Cech cohomology"],"falsifier":"Look in the intended model of light condensed sets for a countably presented Boolean algebra $B$ whose evaluation map $B \\to 2^{\\mathrm{Sp}(B)}$ is not an isomorphism, or for a surjection of spectra $\\mathrm{Sp}(C) \\to \\mathrm{Sp}(B)$ not induced by an injection $B \\to C$. Either would break the first two axioms, and with them the derived theorems on continuity, vanishing of $H^1$, and Brouwer's fixed point as statements about condensed sets. A concrete starting point is the Boolean algebra $B_\\infty$ with generators $g_n$ and relations $g_m \\wedge g_n = 0$ for $m \\neq n$, where the axioms force every map $N_\\infty \\to 2$ to be represented by an element of the algebra.","tokens_in":18272,"feed_emoji":"📐","tokens_out":14267,"duration_ms":117917,"temperature":0.7,"pith_summary":"This paper proposes that homotopy type theory — a formal language in which mathematical objects are types rather than sets — can serve as an internal language for the mathematical universe of light condensed sets, a modern way of building topological spaces out of profinite pieces. To do this, it adds four axioms and shows that they yield a synthetic topology inside the theory: open propositions induce a topology on every type, every function is continuous, and on Stone spaces, second-countable compact Hausdorff spaces, and the unit interval this topology is the classical one. The axioms also imply Markov's principle and LLPO, refute WLPO, and give an internal proof of Brouwer's fixed-point theorem for the disk. If the axioms are true of light condensed sets — which the paper takes as a working assumption and conjecture — then a large part of condensed mathematics and classical topology becomes derivable in one machine-checkable system.","feed_headline":"Four axioms prove Brouwer's fixed-point theorem in type theory","feed_subtitle":"The same axioms make every function on the unit interval continuous and capture Stone–compact Hausdorff duality.","key_machinery":"The key machinery is the type of countably presented Boolean algebras, denoted $\\mathrm{Boole}$, together with its spectrum $\\mathrm{Sp}(B)$ of Boolean homomorphisms into $2$. The Stone duality axiom — evaluation $B \\to 2^{\\mathrm{Sp}(B)}$ is an isomorphism — makes $\\mathrm{Sp}$ a dual equivalence between $\\mathrm{Boole}$ and the type of Stone spaces, so Stone spaces behave as sequential limits of finite sets. The remaining axioms (surjections are formal surjections, local choice, dependent choice) make these spectra interact with arbitrary types the way light condensed sets do. A proposition is open when it is a countable disjunction of decidable propositions, and the collection of open propositions is a dominance: a class of propositions that induces a topology on every type, which is what makes the statement that every function is continuous meaningful. For the cohomological application, the mechanism also includes the first cohomology group $H^1(X,\\mathbb{Z})$ defined as maps into the delooping $B\\mathbb{Z}$, compared with Cech cohomology of a Stone cover, and localization at the unit interval to run Brouwer's fixed-point argument.","core_discovery":"The paper's central claim is that four axioms on top of homotopy type theory suffice to carry out a synthetic theory of Stone duality and compact Hausdorff spaces in the internal language of light condensed sets. The axioms state that every countably presented Boolean algebra is recovered from its spectrum (Stone duality: evaluation $B \\to 2^{\\mathrm{Sp}(B)}$ is an isomorphism), that injective algebra maps correspond exactly to surjections of spectra, that local choice holds for Stone spectra, and that dependent choice holds. In this system open propositions form a dominance, so every type carries an intrinsic topology and every function is continuous; on Stone spaces, second-countable compact Hausdorff spaces, and the unit interval this topology is the classical one. The system proves Markov's principle and LLPO, refutes WLPO, identifies Stone spaces with totally disconnected compact Hausdorff spaces, shows $H^1(S,\\mathbb{Z})=0$ for Stone spaces and $H^1(X,\\mathbb{Z})=\\check{H}^1(X,S,\\mathbb{Z})$ for compact Hausdorff spaces with a Cech cover, and proves Brouwer's fixed-point theorem internally. The authors state that the validity of the axioms in the light condensed set model is a working assumption and a conjecture, not established in this paper.","pith_inferences":["Inference: if the completeness conjecture is right, the four axioms could serve as a practical internal calculus for light condensed sets, letting proofs about profinite sets, compact Hausdorff spaces, and cohomology be formalized in homotopy type theory without leaving the axiomatic system.","Inference: the exact combination of Markov's principle, LLPO, and the negation of WLPO gives the internal logic a precise place among constructive systems; it is worth testing whether other toposes share this signature, which would show how characteristic the light condensed set model is.","Inference: the Cech-cohomology route should extend to higher cohomology groups and to the circle; the paper already notes that a similar computation for $S^1$ would give $H^1(S^1,\\mathbb{Z}) = \\mathbb{Z}$, opening the way to synthetic degree theory and further fixed-point or invariance theorems.","Inference: a concrete next step is to formalize the four axioms together with the proofs of the principles of omniscience, continuity, and Brouwer's theorem in a proof assistant; that would verify the derivation chain even while the model-theoretic justification remains open."],"forward_implications":["Every function between types is continuous for the induced topology; in particular every map $[0,1] \\to [0,1]$ is continuous in the usual epsilon-delta sense (Theorem 5.0.9).","The system proves Markov's principle and LLPO and refutes WLPO, so the internal logic of light condensed sets is a specific constructive logic rather than plain intuitionistic logic (Theorems 1.4.1, 1.4.3, 1.4.4).","Stone spaces are exactly the totally disconnected compact Hausdorff spaces, and both Stone and compact Hausdorff types are closed under dependent pair types — a statement that needs types, not just sets (Theorem 4.3.7, Lemma 4.2.2).","$H^1(S,\\mathbb{Z})=0$ for every Stone space; for every compact Hausdorff space with a Cech cover, $H^1(X,\\mathbb{Z})$ equals its Cech cohomology; and $H^1([0,1],\\mathbb{Z})=0$ (Lemma 6.2.3, Theorem 6.3.5, Proposition 6.4.3).","Brouwer's fixed-point theorem holds internally for the disk: every map $D^2 \\to D^2$ has a fixed point (Theorem 6.5.10)."],"supporting_citations":[{"why":"Supplies the higher topos of light condensed sets that the axiom system is intended to model.","marker":"[CS24]"},{"why":"Establishes the method of using homotopy type theory as an internal language for a higher topos, here shifted from affine schemes to Stone spaces.","marker":"[CCH23]"},{"why":"Provides the homotopy type theory foundations: univalence, higher inductive types, and the delooping-based definition of cohomology.","marker":"[Pro13]"},{"why":"Introduces the synthetic topology setting in which a dominance of open propositions gives every type an intrinsic topology.","marker":"[Esc04]"},{"why":"Supplies constructive analysis facts about real numbers and the unit interval used to prove the interval is compact Hausdorff and for the intermediate value theorem.","marker":"[BB85]"},{"why":"Gives the constructive reverse mathematics results on open and closed propositions used in the derivations of Markov's principle and LLPO closures.","marker":"[Die18]"},{"why":"Provides the theory of sequential colimits in homotopy type theory used to identify overtly discrete and Stone spaces as limits of finite types.","marker":"[SDR20]"},{"why":"States the characterization of cohomology of compact Hausdorff spaces whose special case is recovered as H^1 equals Cech cohomology.","marker":"[Dyc76]"},{"why":"Supplies the earlier type-theoretic proof of Brouwer's fixed-point theorem that the paper adapts to its axiomatic setting.","marker":"[Shu18]"},{"why":"Provides localization at a type, the modality used in the final contradiction of the Brouwer fixed-point proof.","marker":"[RSS20]"}],"fun_headline_variants":["Four axioms give synthetic Stone duality and Brouwer's theorem","Synthetic Stone duality from four axioms, proving Brouwer","HoTT plus four axioms: Stone duality, continuity, Brouwer fixed point","Four axioms yield synthetic Stone duality and Brouwer's fixed point"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the four axioms are valid statements about the internal logic of light condensed sets; the paper does not prove this and presents it as a working assumption and a conjecture awaiting a constructive justification.","fun_headline_variants_meta":{"raw":{"variants":["Four axioms give synthetic Stone duality and Brouwer's theorem","Synthetic Stone duality from four axioms, proving Brouwer","HoTT plus four axioms: Stone duality, continuity, Brouwer fixed point","Four axioms yield synthetic Stone duality and Brouwer's fixed point"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000968,"raw_usage":{"total_tokens":4159,"prompt_tokens":1029,"completion_tokens":3130,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":645,"completion_tokens_details":{"reasoning_tokens":3058}},"tokens_in":645,"tokens_out":3130,"duration_ms":21110,"temperature":1.0,"reasoning_tokens":3058,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T22:41:51.844747+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Look in the intended model of light condensed sets for a countably presented Boolean algebra $B$ whose evaluation map $B \\to 2^{\\mathrm{Sp}(B)}$ is not an isomorphism, or for a surjection of spectra $\\mathrm{Sp}(C) \\to \\mathrm{Sp}(B)$ not induced by an injection $B \\to C$. Either would break the first two axioms, and with them the derived theorems on continuity, vanishing of $H^1$, and Brouwer's fixed point as statements about condensed sets. A concrete starting point is the Boolean algebra $B_\\infty$ with generators $g_n$ and relations $g_m \\wedge g_n = 0$ for $m \\neq n$, where the axioms force every map $N_\\infty \\to 2$ to be represented by an element of the algebra.","supporting_citations":[],"review_version":1}