Comparator challenges

Install comparator, landrun, and lean4export, and make them available on PATH. Then, from lean/:

lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json

Supporting-result comparisons

These setups verify supporting results, not the corresponding papers’ main theorems:

CharacterVarietiesAllSeamsSupport.json: compatibility of the produced marked solution with every seam equation.
CartierChartCompactnessSupport.json: compactness of normalized chart-field retractions.
SurfaceConeCandidateSupport.json: ring-theoretic properties of the completed surface cone.
TraceIdealTransportSupport.json: transport of finite and zero ideals, with the construction-provider statements required by the original comparison.
HoneycombBridgeMassSupport.json: finiteness and quarter-power bounds for the strict honeycomb bridge mass.

See the scope notes for per-paper coverage and limitations.