# Potential integral density on curve character varieties

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Integral points on character varieties of curves](../../preprints/Integral-points-on-character-varieties-of-curves-September-25-2026/paper.pdf)

## Scope

The integral-density question asks whether integral points become Zariski dense in every component of a curve character variety after one finite extension of the number field. The linked formalization proves a supporting compatibility result for its marked-surface construction. Given a proper diagram with finitely many vertices, a chosen seam with maximal adjacent facet rank and a positive-genus parent, puncture data, an existing solution over a field, and a chosen boundary occurrence, the produced marked values satisfy every seam equation.

This is conditional compatibility of the produced solution. Potential integral density, including the prescribed-boundary and all-component conclusions, remains outside the selected statement.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Compatibility of the produced marked solution with every seam equation | [CharacterVarietiesAllSeamsSupport.lean](../ComparatorChallenges/CharacterVarietiesAllSeamsSupport.lean) |