Awkronos waddle
Each paper is a module cluster under Hong/. The pieces more than one paper needs live in Hong/Infrastructure and are imported by name, so a Lucas sequence means the same thing in the K3 cluster as it does in the moonshine cluster. This page walks the clusters and names what is still open in each.
Hong/BallantineMerca/ · imports FormalPowerSeries, FranklinInvolution
The seven pairs are the visible surface. Underneath is the reduction f_a ≡ f_b · f_24 (mod 2), developed in ThetaMod2.lean on top of formal power series and Franklin's involution, the classical bijection that proves Euler's pentagonal number theorem. The Weber class-field input is kept as a named hypothesis instead of being assumed silently.
Hong/Moonshine/ · imports Hypergeometric, JFunction
The cluster carries the flat-coordinate construction, the hypergeometric identity, and the statement of the Caldararu–He–Huang conjecture itself. Two bridges carry the analytic weight: CHHUpperHalfPlaneBridge, which locates the expansion in the upper half plane, and JInversionBridge, which inverts the j-function on the relevant domain. Discharge those two and the identity is unconditional.
Hong/SquareFree/ · imports SquareFreeWord
Two quantities race each other as the alphabet grows. The number of square-free extensions available at each step grows like (k − 2)(n + 1) · 10; the number an extremal word can afford is bounded by 147n, which is the 14.7n bound written over a common denominator. The first passes the second at k = 17. The inequality is a closed theorem in the source. The 14.7n bound is the named input, Corollary23CountingBridge.
Hong/MarkovChains/ · imports EdgeColoring, LatinRectangle
Proper edge-colorings of a bipartite graph are Latin rectangles in disguise, which is why both modules are imported. The Metropolis–Hastings factorization is closed. The repair lemma for almost-colorings, the step that fixes a coloring which fails at exactly one edge, is annotated as open in AlmostColoring.lean. It is the real content of Lemma 2.1 and the honest gap in this cluster.
Hong/LFunctions/ · imports LucasSequence
The E_λ family has seven parameter values at which the surface acquires complex multiplication. The cluster carries the family, the symmetric-square coefficients, and the parity lemma. Modularity in the sense of Wiles and the isogeny bound of Mazur are retained as named hypotheses. They are true and famous, and they are still not proved here, so they are visible.
Hong/PatternAvoidance/ · imports InversionSequence, LabelIncreasingTree, SInvLift
The fiber decomposition is closed and the label-increasing tree machinery is built. The conjecture the paper leaves open, numbered 3.18, is stated in Lean as a typed proposition rather than as a comment, which means an attempt on it either compiles or does not. It has not compiled yet. This is the cluster where new mathematics would land first.
Hong/PopStack/ · imports TamariLattice
The Tamari lattice orders the ways to parenthesize a product, and its size is Catalan. Pop-stack sorting on it yields a rational generating function whose denominator carries those same Catalan numbers as coefficients. Small t is closed computation. The recurrence machinery that would give every t sits in the same cluster.
Hong/EulerKronecker/ · imports BrunTitchmarsh, ConsecutiveSquares
The Brun–Titchmarsh sieve bounds primes in arithmetic progressions, and it is what the decomposition leans on. The γ₃ term is proved nonnegative. One analytic input in Decomposition.lean is written as a named open goal rather than assumed, which keeps the shape of the argument honest while the estimate is worked out.
Three named bridges, one repair lemma, one analytic estimate, and Conjecture 3.18. Each is a specific mathematical statement in a specific file, not a general disclaimer. Anyone who closes one has done real work.