How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Log HMS surface data with distinguished complex structure
Definition
A log HMS surface datum is a smooth rational projective surface over with a nodal anticanonical divisor as in Log Calabi–Yau pair, toric degeneration and scattering data, together with a chosen toric model and the source’s distinguished complex-structure data. A toric model includes a smooth projective toric pair , a sequence of interior blow-ups of points on the toric boundary components that leaves the boundary unchanged, and the corner blow-ups and total transforms specifying . For the distinguished structure, on each toric boundary component choose its torus coordinate from the fixed torus action and place the selected interior blow-up point at , using the corresponding point on successive strict transforms when iterating. The selected model and blow-up sequence are part of the datum.
This records the hypotheses used by Hacking–Keating; it does not assert existence or uniqueness of a toric model, nor does it produce a mirror fibration or categorical equivalence.