SearcharxivSearch

arXiv subjects

Jihoon Hyun

Publications and source records attributed to Jihoon Hyun.

4 recordsLinked to original sources

When Finite Free Curves Split

We characterize equality in the finite free Stam and entropy-power inequalities, proving that Hermite polynomials are the unique extremizers among simple real-rooted inputs, up to independent translations and scalings. The proof turns this classification into a rigidity problem for projective plane curves. Using hyperbolicity and the Helton-Vinnikov theorem, we express the Jacobian defect as an off-diagonal squared norm in a definite symmetric pencil. Together with score transport, this yields a matrix proof of Stam for all real-rooted inputs. For each simple base pair, the directions in which the defect vanishes are the independent translations and common dilation, forming a three-dimensional subspace in every degree whose curves split into $n$ projective lines. At a collision, the leading configurations are again finite free convolutions of normalized derivatives of the velocity polynomials of the colliding input clusters. Combined with incidence counting, this local formula shows that at most one real fiber is singular, every real singularity is an ordinary totally real multiple point, and the ordered collision multiplicities determine the real normalization covering. For $n\geq3$, every non-split curve has at least $2n-2$ non-real projective discriminant zeros, counted with multiplicity, with equality attained by irreducible curves of geometric genus zero through every simple input pair. The leading Fisher-information coefficient is determined by the colliding tangent configurations, while the finite entropy term retains the gaps between clusters. For $n\geq3$, maximal logarithmic entropy divergence along the optimally weighted score direction is equivalent to Stam equality.

math.AG

Algorithmic Cost in "Exact Real Computation"

Turing completeness of a programming language or system characterizes its expressive power; and the strong Church-Turing hypo-/thesis refines such from qualitative to polynomial-time equivalence. Exact Real Computation (ERC) is a novel numerical programming language paradigm: for the imperative processing of continuous data as entities appearing as exact, i.e. devoid of rounding errors [doi:10.1007/978-3-662-44199-2_107]. ERC has been designed [doi:10.46298/lmcs-20(2:17)2024] as convenient and practical alternative, namely proven qualitatively equivalent, to the Turing machines originally underlying Computable Analysis [doi:10.1007/978-3-642-56999-9,doi:10.1007/978-1-4684-6802-1]. The present work quantitatively strengthens this qualitative Turing-completeness: We assign bit-costs to ERC's operational primitives (including partial/multivalued tests) in such a way that any real function incurring polynomial cost becomes Turing-computable in polynomial time, and vice versa. Runtime measurements on implementations in the iRRAM C++ library confirm our theoretical performance predictions.

math.NA

Formalizing Flag Algebras in Lean

Razborov's flag algebra method is a powerful tool for proving asymptotic inequalities in extremal graph theory, often reducing the task to finding a finite certificate by semidefinite programming. We present a machine-checked formalization of the method for finite simple graphs, together with a certificate-to-proof compiler that turns externally generated certificate data into algebraic proofs checked by Lean. The formalization covers the foundations of the method: partially labeled graphs, their densities in large graphs, the quotient algebra of density expressions, graph-limit semantics through positive homomorphisms, and the downward operators used to average out labels. The compiler treats the external semidefinite programming output as candidate data rather than trusted input: Lean independently computes the required density and multiplication facts, verifies positive semidefiniteness exactly over $\mathbb{Q}$, and carries out the algebraic normalization steps of flag-algebra proofs. Our case studies yield formal proofs of seven Tur\'an-type upper bounds, including Mantel's theorem and the Erd\H{o}s pentagon theorem, a $C_4$-density bound for triangle-free graphs, and edge-density bounds for $K_4$-free, $K_5$-free, and $C_5$-free graphs. Independently of the compiler, we formalize the matching constructions that complete the exact Tur\'an densities of Mantel's theorem and the Erd\H{o}s pentagon theorem, and prove two inequalities of Goodman. Our constrained semantics also prompted a meta-theoretic comparison of two ways of imposing graph constraints: building a hereditary constraint into the flag algebra from the start, or testing inequalities afterward on constrained graph limits with labels chosen at random. We state the resulting root-plantability criterion characterizing when the two approaches agree; a forthcoming paper will present the complete account.

cs.LO

Lean-GAP: A Dataset of Formalized Graduate Algebra Problems

We present Lean-GAP (Lean-Graduate Agebra Problems), 430 formalized graduate-level algebra problems from the textbook Abstract Algebra by Dummit and Foote. We develop a scalable pipeline consisting of PDF-to-LaTeX preprocessing, autoformalization into Lean 4, and verification of informal-formal correspondence. While the preprocessing and autoformalization stages can be largely automated, we find that verification remains the most subtle and labor-intensive component, requiring careful human oversight. Our contributions include (i) the construction of a structured dataset of formalized exercises, (ii) a systematic methodology for formalizing textbook mathematics, and (iii) an analysis of recurring challenges in the formalization process. We also compare the performance of different autoformalization models and highlight key bottlenecks in translating informal statements into formal language.

cs.LO