Registry snapshots

Verify, install, and query an immutable caller-supplied registry snapshot. Snapshot integrity authenticates the bytes and schema; it does not certify every stored mathematical claim.

geometric_function_atlas.snapshot

Immutable registry snapshots and typed, local-only queries.

The website database is a separately versioned data artifact. This module never ships a database in the wheel and never opens a snapshot for writing. A caller must provide a manifest when installing or verifying an artifact; ordinary query operations can open an already trusted local SQLite file without network access.

MANIFEST_SCHEMA_VERSION = 1 module-attribute

DEFAULT_MAX_COMPRESSED_BYTES = 512 * 1024 * 1024 module-attribute

DEFAULT_MAX_DECOMPRESSED_BYTES = 2 * 1024 * 1024 * 1024 module-attribute

__all__ = ['MANIFEST_SCHEMA_VERSION', 'Application', 'Counterexample', 'Evidence', 'Fact', 'FamilyDetail', 'FunctionFamily', 'FunctionInstance', 'Paper', 'PaperClaim', 'PaperDetail', 'PropertyImplication', 'RegistrySnapshot', 'SearchResult', 'SnapshotError', 'SnapshotInfo', 'SnapshotIntegrityError', 'SnapshotManifest', 'SnapshotManifestError', 'SnapshotResourceLimitError', 'SnapshotStats', 'SnapshotVerification', 'VerificationRun', 'install_snapshot', 'snapshot_info', 'verify_snapshot'] module-attribute

SnapshotError

Base class for invalid, unverifiable, or unusable snapshots.

SnapshotIntegrityError

Raised when a snapshot or manifest fails a required integrity check.

SnapshotManifestError

Raised when a manifest is malformed or missing a required field.

SnapshotResourceLimitError

Raised before a download or decompression can exceed its byte bound.

SnapshotManifest dataclass

The minimum identity and population contract for a registry snapshot.

dataset_version: str instance-attribute

database_filename: str instance-attribute

database_bytes: int instance-attribute

database_sha256: str instance-attribute

application_tables: tuple[str, ...] instance-attribute

row_counts: Mapping[str, int] instance-attribute

manifest_schema_version: int = MANIFEST_SCHEMA_VERSION class-attribute instance-attribute

compressed_filename: str | None = None class-attribute instance-attribute

compressed_bytes: int | None = None class-attribute instance-attribute

compressed_sha256: str | None = None class-attribute instance-attribute

package_commit: str | None = None class-attribute instance-attribute

source_url: str | None = None class-attribute instance-attribute

__init__(dataset_version: str, database_filename: str, database_bytes: int, database_sha256: str, application_tables: tuple[str, ...], row_counts: Mapping[str, int], manifest_schema_version: int = MANIFEST_SCHEMA_VERSION, compressed_filename: str | None = None, compressed_bytes: int | None = None, compressed_sha256: str | None = None, package_commit: str | None = None, source_url: str | None = None) -> None

__post_init__() -> None

from_dict(payload: Mapping[str, Any]) -> _SnapshotManifestT classmethod

load(path: str | os.PathLike[str]) -> _SnapshotManifestT classmethod

to_dict() -> dict[str, Any]

SnapshotVerification dataclass

Machine-readable result of all required snapshot checks.

path: str instance-attribute

dataset_version: str instance-attribute

checks: Mapping[str, str] instance-attribute

errors: tuple[str, ...] instance-attribute

database: Mapping[str, Any] instance-attribute

success: bool property

status: str property

__init__(path: str, dataset_version: str, checks: Mapping[str, str], errors: tuple[str, ...], database: Mapping[str, Any]) -> None

to_dict() -> dict[str, Any]

SnapshotInfo dataclass

SQLite metadata and populations exposed by snapshot info.

path: str instance-attribute

dataset_version: str | None instance-attribute

sha256: str instance-attribute

bytes: int instance-attribute

sqlite_version: str instance-attribute

user_version: int instance-attribute

page_size: int instance-attribute

page_count: int instance-attribute

freelist_count: int instance-attribute

quick_check: str instance-attribute

integrity_check: str instance-attribute

application_tables: tuple[str, ...] instance-attribute

row_counts: Mapping[str, int] instance-attribute

verified: bool instance-attribute

__init__(path: str, dataset_version: str | None, sha256: str, bytes: int, sqlite_version: str, user_version: int, page_size: int, page_count: int, freelist_count: int, quick_check: str, integrity_check: str, application_tables: tuple[str, ...], row_counts: Mapping[str, int], verified: bool) -> None

to_dict() -> dict[str, Any]

SnapshotStats dataclass

dataset_version: str | None instance-attribute

families: int instance-attribute

instances: int instance-attribute

facts: int instance-attribute

proven_facts: int instance-attribute

disproven_facts: int instance-attribute

verification_runs: int instance-attribute

evidence: int instance-attribute

papers: int instance-attribute

paper_claims: int instance-attribute

row_counts: Mapping[str, int] instance-attribute

function_families: int property

__init__(dataset_version: str | None, families: int, instances: int, facts: int, proven_facts: int, disproven_facts: int, verification_runs: int, evidence: int, papers: int, paper_claims: int, row_counts: Mapping[str, int]) -> None

to_dict() -> dict[str, Any]

FunctionFamily dataclass

id: int instance-attribute

canonical_key: str instance-attribute

name: str instance-attribute

display_name: str | None instance-attribute

closed_form: str | None instance-attribute

generating_def: str | None instance-attribute

is_parametric: bool instance-attribute

param_spec: Any instance-attribute

arity: int instance-attribute

family_group: str | None instance-attribute

is_polynomial: bool instance-attribute

is_entire: bool instance-attribute

coeff_formula: str | None instance-attribute

coeff_decay: str | None instance-attribute

notes: str | None instance-attribute

application_areas: tuple[str, ...] instance-attribute

__init__(id: int, canonical_key: str, name: str, display_name: str | None, closed_form: str | None, generating_def: str | None, is_parametric: bool, param_spec: Any, arity: int, family_group: str | None, is_polynomial: bool, is_entire: bool, coeff_formula: str | None, coeff_decay: str | None, notes: str | None, application_areas: tuple[str, ...]) -> None

to_dict() -> dict[str, Any]

FunctionInstance dataclass

id: int instance-attribute

family_id: int instance-attribute

param_values: Any instance-attribute

coefficients: Any instance-attribute

num_terms: int | None instance-attribute

coeff_source: str | None instance-attribute

coeff_fingerprint: str | None instance-attribute

__init__(id: int, family_id: int, param_values: Any, coefficients: Any, num_terms: int | None, coeff_source: str | None, coeff_fingerprint: str | None) -> None

to_dict() -> dict[str, Any]

Fact dataclass

id: int instance-attribute

family_id: int | None instance-attribute

instance_id: int | None instance-attribute

property_id: int instance-attribute

property_name: str | None instance-attribute

property_param: float | None instance-attribute

fact_kind: str instance-attribute

holds: bool | None instance-attribute

value: float | None instance-attribute

value_exact: str | None instance-attribute

disk_radius: float | None instance-attribute

is_sharp: bool | None instance-attribute

provenance: str instance-attribute

status: str instance-attribute

confidence: str | None instance-attribute

fact_hash: str | None instance-attribute

family_key: str | None instance-attribute

__init__(id: int, family_id: int | None, instance_id: int | None, property_id: int, property_name: str | None, property_param: float | None, fact_kind: str, holds: bool | None, value: float | None, value_exact: str | None, disk_radius: float | None, is_sharp: bool | None, provenance: str, status: str, confidence: str | None, fact_hash: str | None, family_key: str | None) -> None

to_dict() -> dict[str, Any]

Evidence dataclass

id: int instance-attribute

fact_id: int | None instance-attribute

relation_id: int | None instance-attribute

paper_id: int | None instance-attribute

theorem_number: str | None instance-attribute

page_number: int | None instance-attribute

statement_text: str | None instance-attribute

evidence_type: str | None instance-attribute

legacy_claim_id: int | None instance-attribute

family_key: str | None instance-attribute

__init__(id: int, fact_id: int | None, relation_id: int | None, paper_id: int | None, theorem_number: str | None, page_number: int | None, statement_text: str | None, evidence_type: str | None, legacy_claim_id: int | None, family_key: str | None) -> None

to_dict() -> dict[str, Any]

VerificationRun dataclass

id: int instance-attribute

fact_id: int instance-attribute

instance_id: int | None instance-attribute

verifier: str instance-attribute

direction: str instance-attribute

outcome: str instance-attribute

margin: float | None instance-attribute

domain_radius: float | None instance-attribute

witness: Any instance-attribute

tail_bound: float | None instance-attribute

engine_version: str instance-attribute

params: Any instance-attribute

runtime_ms: int | None instance-attribute

family_key: str | None instance-attribute

__init__(id: int, fact_id: int, instance_id: int | None, verifier: str, direction: str, outcome: str, margin: float | None, domain_radius: float | None, witness: Any, tail_bound: float | None, engine_version: str, params: Any, runtime_ms: int | None, family_key: str | None) -> None

to_dict() -> dict[str, Any]

PaperClaim dataclass

id: int instance-attribute

paper_id: int | None instance-attribute

function_name: str | None instance-attribute

claim_type: str | None instance-attribute

claim_text: str | None instance-attribute

verified_match: bool | None instance-attribute

extraction_source: str | None instance-attribute

statement_human: str | None instance-attribute

__init__(id: int, paper_id: int | None, function_name: str | None, claim_type: str | None, claim_text: str | None, verified_match: bool | None, extraction_source: str | None, statement_human: str | None) -> None

to_dict() -> dict[str, Any]

Paper dataclass

id: int instance-attribute

title: str | None instance-attribute

authors: str | None instance-attribute

year: int | None instance-attribute

journal: str | None instance-attribute

filename: str | None instance-attribute

bibtex: str | None instance-attribute

abstract: str | None instance-attribute

structured: Any instance-attribute

doi: str | None instance-attribute

msc_codes: tuple[str, ...] = () class-attribute instance-attribute

theorem_count: int property

Number of structured theorem records attached to the paper.

function_classes: tuple[str, ...] property

Canonical class labels preserved in the structured paper record.

__init__(id: int, title: str | None, authors: str | None, year: int | None, journal: str | None, filename: str | None, bibtex: str | None, abstract: str | None, structured: Any, doi: str | None, msc_codes: tuple[str, ...] = ()) -> None

to_dict() -> dict[str, Any]

LegacyFunction dataclass

A row from the website's legacy functions table.

id: int instance-attribute

name: str instance-attribute

display_name: str | None instance-attribute

category: str | None instance-attribute

dlmf_ref: str | None instance-attribute

power_series: Any instance-attribute

description: str | None instance-attribute

source_type: str | None instance-attribute

source_ref: str | None instance-attribute

tags: tuple[str, ...] = () class-attribute instance-attribute

__init__(id: int, name: str, display_name: str | None, category: str | None, dlmf_ref: str | None, power_series: Any, description: str | None, source_type: str | None, source_ref: str | None, tags: tuple[str, ...] = ()) -> None

to_dict() -> dict[str, Any]

Tag dataclass

A website tag with explicit function and paper populations.

id: int instance-attribute

name: str instance-attribute

category: str | None instance-attribute

function_count: int = 0 class-attribute instance-attribute

paper_count: int = 0 class-attribute instance-attribute

__init__(id: int, name: str, category: str | None, function_count: int = 0, paper_count: int = 0) -> None

to_dict() -> dict[str, Any]

PaperDetail dataclass

paper: Paper instance-attribute

claims: tuple[PaperClaim, ...] instance-attribute

class_tags: tuple[Mapping[str, Any], ...] instance-attribute

family_links: tuple[Mapping[str, Any], ...] instance-attribute

evidence: tuple[Evidence, ...] instance-attribute

id: int property

title: str | None property

__init__(paper: Paper, claims: tuple[PaperClaim, ...], class_tags: tuple[Mapping[str, Any], ...], family_links: tuple[Mapping[str, Any], ...], evidence: tuple[Evidence, ...]) -> None

to_dict() -> dict[str, Any]

FamilyDetail dataclass

family: FunctionFamily instance-attribute

instances: tuple[FunctionInstance, ...] instance-attribute

facts: tuple[Fact, ...] instance-attribute

evidence: tuple[Evidence, ...] instance-attribute

runs: tuple[VerificationRun, ...] instance-attribute

papers: tuple[Paper, ...] instance-attribute

aliases: tuple[str, ...] instance-attribute

id: int property

canonical_key: str property

name: str property

__init__(family: FunctionFamily, instances: tuple[FunctionInstance, ...], facts: tuple[Fact, ...], evidence: tuple[Evidence, ...], runs: tuple[VerificationRun, ...], papers: tuple[Paper, ...], aliases: tuple[str, ...]) -> None

to_dict() -> dict[str, Any]

SearchResult dataclass

kind: str instance-attribute

id: int instance-attribute

canonical_key: str | None = None class-attribute instance-attribute

name: str | None = None class-attribute instance-attribute

display_name: str | None = None class-attribute instance-attribute

title: str | None = None class-attribute instance-attribute

year: int | None = None class-attribute instance-attribute

__init__(kind: str, id: int, canonical_key: str | None = None, name: str | None = None, display_name: str | None = None, title: str | None = None, year: int | None = None) -> None

to_dict() -> dict[str, Any]

Application dataclass

area: str instance-attribute

family_id: int instance-attribute

family_key: str instance-attribute

family_name: str instance-attribute

source: str instance-attribute

paper_count: int = 0 class-attribute instance-attribute

__init__(area: str, family_id: int, family_key: str, family_name: str, source: str, paper_count: int = 0) -> None

to_dict() -> dict[str, Any]

Counterexample dataclass

fact: Fact instance-attribute

property_name: str | None instance-attribute

runs: tuple[VerificationRun, ...] instance-attribute

id: int property

__init__(fact: Fact, property_name: str | None, runs: tuple[VerificationRun, ...]) -> None

to_dict() -> dict[str, Any]

PropertyImplication dataclass

id: int instance-attribute

from_property: str instance-attribute

to_property: str instance-attribute

condition: str | None instance-attribute

source: str | None instance-attribute

from_property_name: str property

to_property_name: str property

__init__(id: int, from_property: str, to_property: str, condition: str | None, source: str | None) -> None

to_dict() -> dict[str, Any]

RegistrySnapshot

A context-managed, immutable SQLite view of a verified snapshot.

path = path instance-attribute

connection = connection instance-attribute

manifest = manifest instance-attribute

__init__(path: Path, connection: sqlite3.Connection, manifest: SnapshotManifest | None) -> None

open(path: str | os.PathLike[str], *, manifest: SnapshotManifest | Mapping[str, Any] | str | os.PathLike[str] | None = None, max_bytes: int = DEFAULT_MAX_DECOMPRESSED_BYTES) -> _RegistrySnapshotT classmethod

close() -> None

__enter__() -> 'RegistrySnapshot'

__exit__(exc_type: type[BaseException] | None, exc: BaseException | None, tb: TracebackType | None) -> None

info() -> SnapshotInfo

stats() -> SnapshotStats

families(*, group: str | None = None, setting: str | None = None, limit: int = 10000) -> tuple[FunctionFamily, ...]

family(identifier: int | str, *, limit: int = 10000) -> FamilyDetail

facts(family: int | str | None = None, *, property: str | None = None, status: str | None = None, limit: int = 10000) -> tuple[Fact, ...]

evidence(family: int | str | None = None, *, paper: int | None = None, limit: int = 10000) -> tuple[Evidence, ...]

runs(family: int | str | None = None, *, limit: int = 10000) -> tuple[VerificationRun, ...]

legacy_functions(query: str | None = None, *, tag: str | None = None, category: str | None = None, limit: int = 10000) -> tuple[LegacyFunction, ...]

List the site's legacy function rows and their tags.

function(identifier: int | str) -> LegacyFunction

Return one legacy function by id or exact name.

tags(query: str | None = None, *, category: str | None = None, limit: int = 10000) -> tuple[Tag, ...]

List website tags with function and paper population counts.

paper_facets() -> dict[str, dict[str, int]]

Return the explorer facets used for paper filtering.

papers(query: str | None = None, *, author: str | None = None, year: int | None = None, decade: int | str | None = None, journal: str | None = None, doi: str | None = None, citation: str | None = None, class_key: str | None = None, tag: str | None = None, claim: str | None = None, msc: str | None = None, has_theorems: bool | None = None, theorem: str | None = None, sort: str = 'relevance', limit: int = 10000) -> tuple[Paper, ...]

paper(identifier: int | str, *, limit: int = 10000) -> PaperDetail

applications(area: str | None = None, family: int | str | None = None, *, limit: int = 10000) -> tuple[Application, ...]

counterexamples(family: int | str | None = None, *, property: str | None = None, limit: int = 10000) -> tuple[Counterexample, ...]

search(query: str, *, kind: str | None = None, limit: int = 100) -> tuple[SearchResult, ...]

aliases(query: str | None = None, *, limit: int = 10000) -> tuple[Mapping[str, Any], ...]

normalize_class(text: str) -> str

hierarchy(property: str | None = None, *, limit: int = 10000) -> tuple[PropertyImplication, ...]

verify_snapshot(path: str | os.PathLike[str], *, manifest: SnapshotManifest | Mapping[str, Any] | str | os.PathLike[str] | None = None, max_bytes: int = DEFAULT_MAX_DECOMPRESSED_BYTES, raise_on_error: bool = False) -> SnapshotVerification

Verify hashes, populations, and SQLite integrity without mutating a file.

install_snapshot(source: str | os.PathLike[str], destination: str | os.PathLike[str], *, manifest: SnapshotManifest | Mapping[str, Any] | str | os.PathLike[str] | None = None, max_compressed_bytes: int = DEFAULT_MAX_COMPRESSED_BYTES, max_decompressed_bytes: int = DEFAULT_MAX_DECOMPRESSED_BYTES) -> Path

Download/copy, verify, and atomically install an immutable snapshot.

The destination is a plain SQLite file. The source may be a local SQLite or Zstandard file, or an HTTPS URL. A manifest is mandatory so an untrusted or mutable database can never silently become the active snapshot.

snapshot_info(path: str | os.PathLike[str], *, manifest: SnapshotManifest | Mapping[str, Any] | str | os.PathLike[str] | None = None) -> SnapshotInfo

Return immutable SQLite metadata; no network access is performed.