// SPDX-License-Identifier: CC-BY-SA-4.0
// SPDX-FileCopyrightText: 2024-2025 Ehsaneddin Asgari and Contributors
= Mathematical Proofs for 1000Langs
:toc:
:toclevels: 3

This directory contains formal mathematical proofs and specifications for the
1000Langs corpus crawler, verified using https://github.com/hyperpolymath/echidna[Echidna].

== Proof Categories

=== 1. Data Integrity Proofs

Proofs that ensure the integrity of crawled and stored data:

* *Checksums*: Cryptographic verification of data consistency
* *Encoding*: UTF-8 validity and normalization guarantees
* *Idempotency*: Re-crawling produces identical results

=== 2. Alignment Correctness

Proofs about parallel text alignment:

* *Bijection*: One-to-one mapping between verse references
* *Transitivity*: If A aligns with B and B with C, then A aligns with C
* *Completeness*: All verses in source appear in alignment

=== 3. Statistical Properties

Proofs about statistical computations:

* *KL-Divergence*: Non-negativity, asymmetry properties
* *Jensen-Shannon*: Symmetry, boundedness (0 ≤ JSD ≤ 1)
* *Entropy*: Maximized by uniform distribution

=== 4. Type Safety Guarantees

Proofs derived from the ReScript type system:

* *ISO 639 Codes*: Valid language code formats
* *Verse References*: Well-formed reference structures
* *Configuration*: Type-safe Nickel schemas

== Directory Structure

[source]
----
proofs/
├── theories/       # Background mathematical theories
│   ├── information_theory.agda
│   ├── set_theory.agda
│   └── language_types.agda
├── specs/          # Formal specifications
│   ├── alignment.spec
│   ├── crawler.spec
│   └── statistics.spec
└── verified/       # Verified implementations
    ├── kl_divergence.v
    ├── alignment.v
    └── iso639.v
----

== Using Echidna

=== Running Proofs

[source,bash]
----
# Verify all proofs
just prove

# Check specific proof
just prove-check alignment_correctness

# Generate proof obligations
just prove-gen
----

=== Adding New Proofs

1. Create specification in `specs/`
2. Implement proof in appropriate prover syntax
3. Add to verification pipeline in `echidna.toml`
4. Run `just prove` to verify

== Proof Obligations

=== Alignment Module

[cols="1,2,1"]
|===
|Property |Description |Status

|`align_bijective`
|Alignment creates bijective mapping
|Pending

|`align_transitive`
|Alignment is transitive across languages
|Pending

|`coverage_monotonic`
|Adding translations increases coverage
|Pending
|===

=== Statistics Module

[cols="1,2,1"]
|===
|Property |Description |Status

|`kl_nonnegative`
|KL-divergence ≥ 0
|Pending

|`kl_zero_identical`
|KL(P\|\|P) = 0
|Pending

|`js_symmetric`
|JSD(P\|\|Q) = JSD(Q\|\|P)
|Pending

|`js_bounded`
|0 ≤ JSD ≤ 1
|Pending

|`entropy_maximum`
|H(uniform) = log(n)
|Pending
|===

=== ISO 639 Module

[cols="1,2,1"]
|===
|Property |Description |Status

|`code_format_valid`
|All codes match regex patterns
|Pending

|`conversion_injective`
|ISO 639-1 → 639-3 is injective
|Pending

|`special_codes_disjoint`
|Special codes don't overlap regular codes
|Pending
|===

== Integration with OpenCyc

Proofs can leverage OpenCyc's common-sense reasoning for:

* Language family relationships
* Geographic constraints on language distribution
* Script compatibility with language features

See `theories/opencyc_integration.agda` for details.
