formal-ai 0.91.0

//! A small in-process library of classical theorems and their textbook proofs.
//!
//! Used by the universal proof engine when a prompt names one of the
//! well-known results (Pythagorean theorem, infinitude of primes,
//! irrationality of √2, Fermat's little theorem, Gödel's first
//! incompleteness theorem, and a Newtonian / Laplacian-determinism
//! reduction).
//!
//! Every entry stores the proof in four languages (en/ru/hi/zh) so the
//! presenter never has to fall back to English for the localized chat
//! surface. The proofs are deliberately short but real: they reproduce the
//! standard deductive structure mathematicians have been using for these
//! results, not a stub.

use crate::proof_engine::types::{Proof, ProofMethod, ProofStep, StepKind};

/// Hand-rolled multilingual proof bodies for the theorems the engine
/// recognizes by keyword.
pub(super) struct KnownTheoremEntry {
    pub id: &'static str,
    pub method: ProofMethod,
    pub match_keywords: &'static [&'static str],
    pub statement_en: &'static str,
    pub statement_ru: &'static str,
    pub statement_hi: &'static str,
    pub statement_zh: &'static str,
    pub steps: &'static [LocalizedStep],
    pub conclusion_en: &'static str,
    pub conclusion_ru: &'static str,
    pub conclusion_hi: &'static str,
    pub conclusion_zh: &'static str,
}

/// One step rendered in every supported language.
pub(super) struct LocalizedStep {
    pub kind: StepKind,
    pub en: &'static str,
    pub ru: &'static str,
    pub hi: &'static str,
    pub zh: &'static str,
}

impl KnownTheoremEntry {
    pub fn matches(&self, normalized: &str) -> bool {
        self.match_keywords.iter().any(|kw| normalized.contains(kw))
    }

    pub fn build_proof(&self, language: &str) -> Proof {
        let statement = match language {
            "ru" => self.statement_ru,
            "hi" => self.statement_hi,
            "zh" => self.statement_zh,
            _ => self.statement_en,
        };
        let conclusion = match language {
            "ru" => self.conclusion_ru,
            "hi" => self.conclusion_hi,
            "zh" => self.conclusion_zh,
            _ => self.conclusion_en,
        };
        let steps = self
            .steps
            .iter()
            .map(|step| ProofStep {
                kind: step.kind,
                text: String::from(match language {
                    "ru" => step.ru,
                    "hi" => step.hi,
                    "zh" => step.zh,
                    _ => step.en,
                }),
            })
            .collect();
        Proof {
            statement: statement.to_owned(),
            steps,
            conclusion: conclusion.to_owned(),
            method: self.method,
        }
    }
}

/// All theorems the engine can discharge by direct lookup. The first
/// entry whose `matches` returns true wins.
pub(super) const REGISTRY: &[KnownTheoremEntry] = &[
    PYTHAGOREAN,
    EUCLID_INFINITUDE_OF_PRIMES,
    SQRT_TWO_IRRATIONAL,
    FERMAT_LITTLE,
    GODEL_FIRST_INCOMPLETENESS,
    LAPLACIAN_DETERMINISM,
];

const PYTHAGOREAN: KnownTheoremEntry = KnownTheoremEntry {
    id: "pythagorean_theorem",
    method: ProofMethod::KnownTheorem,
    match_keywords: &[
        "pythagor",
        "пифагор",
        "毕达哥拉斯",
        "勾股",
        "पाइथागोरस",
        "पाइथागोरियन",
    ],
    statement_en:
        "In any right triangle with legs a, b and hypotenuse c we have a² + b² = c².",
    statement_ru:
        "В любом прямоугольном треугольнике с катетами a, b и гипотенузой c выполняется a² + b² = c².",
    statement_hi:
        "किसी भी समकोण त्रिभुज जिसके लंब a, b और कर्ण c है, के लिए a² + b² = c² होता है।",
    statement_zh: "在任意直角三角形中,若两直角边为 a、b,斜边为 c,则 a² + b² = c²。",
    steps: &[
        LocalizedStep {
            kind: StepKind::Hypothesis,
            en: "Consider a right triangle with legs of length a and b and hypotenuse of length c. \
                 The right angle is opposite the hypotenuse.",
            ru: "Рассмотрим прямоугольный треугольник с катетами длины a и b и гипотенузой c. \
                 Прямой угол лежит напротив гипотенузы.",
            hi: "मान लीजिए कि एक समकोण त्रिभुज है जिसके लंब a, b और कर्ण c है। \
                 समकोण कर्ण के सामने है।",
            zh: "考虑一个直角三角形,两直角边长分别为 a 与 b,斜边长为 c,直角与斜边相对。",
        },
        LocalizedStep {
            kind: StepKind::Definition,
            en: "Drop the altitude from the right angle onto the hypotenuse. It splits the \
                 hypotenuse into two segments of lengths p (adjacent to a) and q (adjacent to b), \
                 with p + q = c.",
            ru: "Опустим высоту из прямого угла на гипотенузу. Она делит гипотенузу на \
                 отрезки длин p (примыкающий к a) и q (примыкающий к b), причём p + q = c.",
            hi: "समकोण से कर्ण पर लम्ब डालिए। यह कर्ण को दो खंडों p (a के निकट) तथा q \
                 (b के निकट) में बाँट देता है, p + q = c।",
            zh: "从直角顶点向斜边作高,它把斜边分成长度为 p(靠近 a)与 q(靠近 b)的两段,\
                 且 p + q = c。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en: "The two smaller triangles created by the altitude are similar to the original \
                 (AA-similarity: each shares the right angle and one acute angle with the \
                 original). Hence a/c = p/a and b/c = q/b, i.e. a² = c·p and b² = c·q.",
            ru: "Два малых треугольника, образованных высотой, подобны исходному (по двум углам: \
                 у каждого общий прямой угол и общий острый угол с исходным). Поэтому a/c = p/a \
                 и b/c = q/b, то есть a² = c·p и b² = c·q.",
            hi: "उच्चता द्वारा बने दोनों छोटे त्रिभुज मूल त्रिभुज के समरूप होते हैं (AA समरूपता: \
                 हर एक में समकोण और एक न्यूनकोण मूल त्रिभुज से समान है)। अतः a/c = p/a तथा \
                 b/c = q/b, यानी a² = c·p और b² = c·q।",
            zh: "高线分出的两个小三角形与原三角形相似(AA 相似:各有原三角形的直角和一个锐角)。\
                 因此 a/c = p/a 与 b/c = q/b,即 a² = c·p,b² = c·q。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en: "Add the two equalities: a² + b² = c·p + c·q = c·(p + q) = c·c = c².",
            ru: "Сложим эти равенства: a² + b² = c·p + c·q = c·(p + q) = c·c = c².",
            hi: "दोनों समीकरणों को जोड़िए: a² + b² = c·p + c·q = c·(p + q) = c·c = c²।",
            zh: "把两个等式相加:a² + b² = c·p + c·q = c·(p + q) = c·c = c²。",
        },
    ],
    conclusion_en: "Therefore a² + b² = c² for every right triangle. ∎",
    conclusion_ru: "Следовательно, a² + b² = c² для любого прямоугольного треугольника. ∎",
    conclusion_hi: "अतः प्रत्येक समकोण त्रिभुज के लिए a² + b² = c² सिद्ध होता है। ∎",
    conclusion_zh: "故对一切直角三角形都有 a² + b² = c²。∎",
};

const EUCLID_INFINITUDE_OF_PRIMES: KnownTheoremEntry = KnownTheoremEntry {
    id: "euclid_infinitude_of_primes",
    method: ProofMethod::Contradiction,
    match_keywords: &[
        "infinitely many primes",
        "infinitude of primes",
        "euclid",
        "бесконечно много прост",
        "бесконечности прост",
        "евклид",
        "अनंत अभाज्य",
        "无穷多素数",
        "素数无穷",
        "欧几里得",
    ],
    statement_en: "There are infinitely many prime numbers.",
    statement_ru: "Простых чисел бесконечно много.",
    statement_hi: "अभाज्य संख्याएँ अनंत हैं।",
    statement_zh: "素数有无穷多个。",
    steps: &[
        LocalizedStep {
            kind: StepKind::Hypothesis,
            en: "Assume for contradiction that only finitely many primes exist; call them \
                 p₁, p₂, …, pₙ.",
            ru: "Предположим противное: простых чисел конечное число; обозначим их \
                 p₁, p₂, …, pₙ.",
            hi: "विरोधाभास हेतु मान लीजिए कि अभाज्य संख्याएँ केवल सीमित संख्या में हैं: \
                 p₁, p₂, …, pₙ।",
            zh: "假设素数仅有有限多个,记为 p₁、p₂、…、pₙ。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en: "Form the number N = p₁·p₂·…·pₙ + 1. Then N is an integer greater than 1.",
            ru: "Рассмотрим число N = p₁·p₂·…·pₙ + 1. Это целое число, большее единицы.",
            hi: "संख्या N = p₁·p₂·…·pₙ + 1 लीजिए। N एक से बड़ा पूर्णांक है।",
            zh: "构造数 N = p₁·p₂·…·pₙ + 1。N 是大于 1 的整数。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en: "By the fundamental theorem of arithmetic, N has a prime divisor q. \
                 If q = pᵢ for some i, then pᵢ divides both p₁·p₂·…·pₙ and N, so pᵢ divides their \
                 difference, which is 1 — impossible.",
            ru: "По основной теореме арифметики у N есть простой делитель q. Если q = pᵢ для \
                 некоторого i, то pᵢ делит и p₁·p₂·…·pₙ, и N, а значит делит их разность, равную 1 \
                 — противоречие.",
            hi: "अंकगणित की मूल प्रमेय से N का कोई अभाज्य भाजक q है। यदि किसी i के लिए q = pᵢ \
                 हो, तो pᵢ संख्या p₁·p₂·…·pₙ और N दोनों को विभाजित करेगा, अर्थात उनका अंतर 1 \
                 भी विभाजित करेगा — असंभव।",
            zh: "由算术基本定理,N 有一个素因数 q。若 q = pᵢ,则 pᵢ 同时整除 p₁·p₂·…·pₙ 与 N,\
                 因而整除二者之差 1,矛盾。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en: "Hence q is a prime not in the list p₁, …, pₙ, contradicting the assumption \
                 that the list was complete.",
            ru: "Значит, q — простое число, не входящее в список p₁, …, pₙ, что противоречит \
                 предположению о полноте списка.",
            hi: "अतः q एक ऐसा अभाज्य है जो सूची p₁, …, pₙ में नहीं है, जो सूची के पूर्ण होने की \
                 परिकल्पना का खंडन करता है।",
            zh: "因此 q 是不在 p₁, …, pₙ 中的素数,与假设矛盾。",
        },
    ],
    conclusion_en: "The assumption fails, so there are infinitely many primes. ∎",
    conclusion_ru: "Предположение несостоятельно, следовательно простых чисел бесконечно много. ∎",
    conclusion_hi: "अतः परिकल्पना असत्य है और अभाज्य संख्याएँ अनंत हैं। ∎",
    conclusion_zh: "假设不成立,故素数有无穷多个。∎",
};

const SQRT_TWO_IRRATIONAL: KnownTheoremEntry = KnownTheoremEntry {
    id: "sqrt_two_irrational",
    method: ProofMethod::Contradiction,
    match_keywords: &[
        "square root of two",
        "square root of 2",
        "sqrt(2)",
        "√2",
        "корень из двух",
        "корень из 2",
        "иррацион",
        "irrational",
        "दो का वर्गमूल",
        "मूल दो",
        "अपरिमेय",
        "根号二",
        "根号 2",
        "无理",
    ],
    statement_en: "√2 is irrational: there are no integers p, q with q ≠ 0 such that p/q = √2.",
    statement_ru: "√2 иррационально: не существует целых p, q (q ≠ 0), для которых p/q = √2.",
    statement_hi: "√2 अपरिमेय है: कोई पूर्णांक p, q (q ≠ 0) ऐसे नहीं हैं जिनके लिए p/q = √2 हो।",
    statement_zh: "√2 是无理数:不存在整数 p、q(q ≠ 0)使得 p/q = √2。",
    steps: &[
        LocalizedStep {
            kind: StepKind::Hypothesis,
            en: "Assume for contradiction that √2 = p/q with integers p, q ≠ 0 and gcd(p, q) = 1 \
                 (we can always cancel common factors).",
            ru: "Предположим противное: √2 = p/q при целых p, q ≠ 0 и НОД(p, q) = 1 (общие \
                 множители всегда можно сократить).",
            hi: "विरोधाभास हेतु मान लीजिए कि √2 = p/q, जहाँ p, q पूर्णांक हैं, q ≠ 0 तथा \
                 gcd(p, q) = 1 (सामान्य गुणनखंडों को रद्द किया जा सकता है)।",
            zh: "假设 √2 = p/q,其中 p、q 为整数,q ≠ 0 且 gcd(p, q) = 1(可消去公因数)。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en: "Square both sides: 2 = p²/q², so p² = 2·q². Hence p² is even, and therefore p \
                 is even (the square of an odd integer is odd). Write p = 2·k.",
            ru: "Возведём в квадрат: 2 = p²/q², откуда p² = 2·q². Значит p² чётно, и потому p \
                 чётно (квадрат нечётного нечётен). Запишем p = 2·k.",
            hi: "दोनों ओर का वर्ग लीजिए: 2 = p²/q², अतः p² = 2·q²। इसलिए p² सम है और \
                 परिणामतः p भी सम है (विषम पूर्णांक का वर्ग विषम होता है)। p = 2·k लिखिए।",
            zh: "两边平方:2 = p²/q²,即 p² = 2·q²。故 p² 为偶数,从而 p 为偶数\
                 (奇数的平方为奇数),写作 p = 2·k。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en: "Substitute: (2·k)² = 2·q², i.e. 4·k² = 2·q², i.e. q² = 2·k². So q² is even and q \
                 is even.",
            ru: "Подставим: (2·k)² = 2·q², то есть 4·k² = 2·q², откуда q² = 2·k². Значит q² \
                 чётно, и q чётно.",
            hi: "प्रतिस्थापन: (2·k)² = 2·q², यानी 4·k² = 2·q², अर्थात q² = 2·k²। अतः q² \
                 सम है और q भी सम है।",
            zh: "代入:(2·k)² = 2·q²,即 4·k² = 2·q²,故 q² = 2·k²。所以 q² 为偶数,q 也为偶数。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en: "Both p and q are even, contradicting gcd(p, q) = 1.",
            ru: "Получили, что p и q оба чётны — противоречие с НОД(p, q) = 1.",
            hi: "p और q दोनों सम हैं, जो gcd(p, q) = 1 का खंडन करता है।",
            zh: "p 与 q 均为偶数,与 gcd(p, q) = 1 矛盾。",
        },
    ],
    conclusion_en: "The assumption fails, so √2 is irrational. ∎",
    conclusion_ru: "Предположение несостоятельно, поэтому √2 иррационально. ∎",
    conclusion_hi: "अतः परिकल्पना असत्य है और √2 अपरिमेय है। ∎",
    conclusion_zh: "假设不成立,故 √2 是无理数。∎",
};

const FERMAT_LITTLE: KnownTheoremEntry = KnownTheoremEntry {
    id: "fermat_little_theorem",
    method: ProofMethod::Induction,
    match_keywords: &[
        "fermat's little",
        "fermat little",
        "малая теорема ферма",
        "малой теоремы ферма",
        "फर्मा की लघु",
        "फर्मा लघु",
        "费马小定理",
        "費馬小定理",
    ],
    statement_en:
        "For every prime p and every integer a, aᵖ ≡ a (mod p). Equivalently, if gcd(a, p) = 1, \
         then aᵖ⁻¹ ≡ 1 (mod p).",
    statement_ru:
        "Для любого простого p и любого целого a выполнено aᵖ ≡ a (mod p). Эквивалентно, при \
         НОД(a, p) = 1 имеем aᵖ⁻¹ ≡ 1 (mod p).",
    statement_hi: "हर अभाज्य p तथा हर पूर्णांक a के लिए aᵖ ≡ a (mod p)। यदि gcd(a, p) = 1 हो, \
         तो aᵖ⁻¹ ≡ 1 (mod p)।",
    statement_zh: "对任意素数 p 与任意整数 a,有 aᵖ ≡ a (mod p)。\
                   等价地,若 gcd(a, p) = 1,则 aᵖ⁻¹ ≡ 1 (mod p)。",
    steps: &[
        LocalizedStep {
            kind: StepKind::Hypothesis,
            en: "Fix a prime p. We prove aᵖ ≡ a (mod p) for every non-negative integer a by \
                 induction on a; the result for negative a follows by parity / sign.",
            ru: "Зафиксируем простое p. Докажем aᵖ ≡ a (mod p) для каждого неотрицательного \
                 целого a индукцией по a; для отрицательных случай сводится знаком.",
            hi: "एक अभाज्य p तय कीजिए। हम हर अऋणात्मक पूर्णांक a के लिए aᵖ ≡ a (mod p) को \
                 a पर आगमन द्वारा सिद्ध करते हैं; ऋणात्मक a का मामला चिह्न से अनुसरण करता है।",
            zh: "固定素数 p。对非负整数 a 用数学归纳法证 aᵖ ≡ a (mod p);负整数情形按符号化归。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en: "Base case a = 0: 0ᵖ = 0 ≡ 0 (mod p). The base case holds.",
            ru: "База a = 0: 0ᵖ = 0 ≡ 0 (mod p). База выполнена.",
            hi: "आधार स्थिति a = 0: 0ᵖ = 0 ≡ 0 (mod p)। आधार सिद्ध है।",
            zh: "归纳基础 a = 0:0ᵖ = 0 ≡ 0 (mod p),成立。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en: "Inductive step: assume aᵖ ≡ a (mod p). Use the binomial expansion \
                 (a + 1)ᵖ = Σ C(p, k)·aᵏ. For 1 ≤ k ≤ p − 1, the binomial coefficient C(p, k) is \
                 divisible by p (because p is prime and appears in the numerator but not in the \
                 denominator). Hence (a + 1)ᵖ ≡ aᵖ + 1 (mod p).",
            ru: "Шаг индукции: пусть aᵖ ≡ a (mod p). Воспользуемся биномом Ньютона \
                 (a + 1)ᵖ = Σ C(p, k)·aᵏ. При 1 ≤ k ≤ p − 1 биномиальный коэффициент C(p, k) \
                 делится на p (p — простое, входит в числитель, но не в знаменатель). Поэтому \
                 (a + 1)ᵖ ≡ aᵖ + 1 (mod p).",
            hi: "आगमन-चरण: मान लीजिए aᵖ ≡ a (mod p)। द्विपद विस्तार \
                 (a + 1)ᵖ = Σ C(p, k)·aᵏ का उपयोग करें। 1 ≤ k ≤ p − 1 के लिए C(p, k), p से \
                 विभाज्य है (p अभाज्य अंश में आता है पर हर में नहीं)। अतः \
                 (a + 1)ᵖ ≡ aᵖ + 1 (mod p)।",
            zh: "归纳步:设 aᵖ ≡ a (mod p)。由二项式展开 (a + 1)ᵖ = Σ C(p, k)·aᵏ,\
                 当 1 ≤ k ≤ p − 1 时 C(p, k) 被 p 整除(p 为素数,出现在分子而不在分母)。\
                 故 (a + 1)ᵖ ≡ aᵖ + 1 (mod p)。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en: "Combining with the inductive hypothesis: (a + 1)ᵖ ≡ aᵖ + 1 ≡ a + 1 (mod p). \
                 The inductive step is established.",
            ru: "Совмещая с предположением: (a + 1)ᵖ ≡ aᵖ + 1 ≡ a + 1 (mod p). Шаг индукции \
                 доказан.",
            hi: "आगमन-परिकल्पना के साथ संयोजन: (a + 1)ᵖ ≡ aᵖ + 1 ≡ a + 1 (mod p)। \
                 आगमन-चरण सिद्ध हुआ।",
            zh: "结合归纳假设:(a + 1)ᵖ ≡ aᵖ + 1 ≡ a + 1 (mod p)。归纳步完成。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en:
                "By induction, aᵖ ≡ a (mod p) for every non-negative integer a. When gcd(a, p) = 1 \
                 we may cancel one factor of a (it is invertible modulo p) to get aᵖ⁻¹ ≡ 1 (mod p).",
            ru: "По индукции aᵖ ≡ a (mod p) для всех a ≥ 0. Если НОД(a, p) = 1, можно сократить \
                 один множитель a (он обратим по модулю p), получив aᵖ⁻¹ ≡ 1 (mod p).",
            hi: "आगमन से, हर अऋणात्मक a के लिए aᵖ ≡ a (mod p)। gcd(a, p) = 1 पर a का एक \
                 गुणनखंड रद्द कर सकते हैं (वह mod p में व्युत्क्रमणीय है), जिससे \
                 aᵖ⁻¹ ≡ 1 (mod p) प्राप्त होता है।",
            zh: "由归纳,对所有非负整数 a 都有 aᵖ ≡ a (mod p)。当 gcd(a, p) = 1 时,a 在 mod p \
                 下可逆,可消去得到 aᵖ⁻¹ ≡ 1 (mod p)。",
        },
    ],
    conclusion_en: "Therefore aᵖ ≡ a (mod p) for every integer a and every prime p. ∎",
    conclusion_ru: "Следовательно, aᵖ ≡ a (mod p) для всякого целого a и всякого простого p. ∎",
    conclusion_hi: "अतः हर पूर्णांक a और हर अभाज्य p के लिए aᵖ ≡ a (mod p)। ∎",
    conclusion_zh: "故对一切整数 a 与素数 p,皆有 aᵖ ≡ a (mod p)。∎",
};

const GODEL_FIRST_INCOMPLETENESS: KnownTheoremEntry = KnownTheoremEntry {
    id: "godel_first_incompleteness",
    method: ProofMethod::AxiomReduction,
    match_keywords: &[
        "godel",
        "gödel",
        "godels",
        "gödels",
        "godel's",
        "gödel's",
        "incompleteness",
        "теорем гёдел",
        "теорема гёдел",
        "теоремы гёдел",
        "теоремы гедел",
        "теорема гедел",
        "теорем гедел",
        "गोडेल",
        "अपूर्णता",
        "哥德尔",
        "不完备",
        "不完备性",
    ],
    statement_en:
        "Any consistent, recursively axiomatised formal system F that interprets Peano arithmetic \
         admits a true arithmetical sentence G_F that F neither proves nor refutes (Gödel's first \
         incompleteness theorem).",
    statement_ru:
        "Всякая непротиворечивая, рекурсивно аксиоматизированная формальная система F, \
         интерпретирующая арифметику Пеано, имеет истинное арифметическое утверждение G_F, \
         которое F не доказывает и не опровергает (первая теорема Гёделя о неполноте).",
    statement_hi:
        "हर सुसंगत, पुनरावर्ती रूप से अभिगृहीत औपचारिक तंत्र F, जो Peano अंकगणित को निरूपित \
         करता है, में एक सत्य अंकगणितीय कथन G_F मौजूद है जिसे F न तो सिद्ध करता है न खंडित \
         (गोडेल का प्रथम अपूर्णता प्रमेय)।",
    statement_zh: "任意一个一致、可递归公理化且可表达 Peano 算术的形式系统 F,\
                   存在一个真的算术语句 G_F,F 既不能证明也不能否证(哥德尔第一不完备性定理)。",
    steps: &[
        LocalizedStep {
            kind: StepKind::Axiom,
            en: "Fix a formal system F that satisfies (i) consistency, (ii) a decidable axiom \
                 set, and (iii) enough arithmetic to define primitive recursive functions \
                 (e.g. F ⊇ Peano arithmetic).",
            ru: "Зафиксируем формальную систему F, удовлетворяющую: (i) непротиворечивость, \
                 (ii) разрешимое множество аксиом, (iii) достаточно арифметики для определения \
                 примитивно-рекурсивных функций (например, F ⊇ арифметика Пеано).",
            hi: "एक औपचारिक तंत्र F लीजिए जो (i) सुसंगत हो, (ii) निर्णायक अभिगृहीत-समुच्चय रखे, \
                 (iii) आदिम पुनरावर्ती फलन परिभाषित करने योग्य अंकगणित (उदा. F ⊇ Peano अंकगणित) \
                 रखे।",
            zh: "取一个形式系统 F:(i) 一致,(ii) 公理集可判定,(iii) 表达原始递归函数所需的算术\
                 (例如 F ⊇ Peano 算术)。",
        },
        LocalizedStep {
            kind: StepKind::Definition,
            en: "Gödel-numbering: assign each formula φ a unique natural number ⌜φ⌝. Provability \
                 in F becomes a primitive-recursive predicate Prov_F(x, y) meaning \"x codes a \
                 proof in F of the formula coded by y\".",
            ru: "Гёделева нумерация: каждой формуле φ ставится в соответствие уникальное \
                 натуральное число ⌜φ⌝. Доказуемость в F представляется примитивно-рекурсивным \
                 предикатом Prov_F(x, y), означающим: «x кодирует доказательство в F формулы, \
                 кодируемой y».",
            hi: "गोडेल-संख्यांकन: हर सूत्र φ को एक अद्वितीय प्राकृत संख्या ⌜φ⌝ दीजिए। F में \
                 साध्यता एक आदिम-पुनरावर्ती विधेय Prov_F(x, y) बन जाती है, जिसका अर्थ है \
                 \"x द्वारा कोडित प्रमाण F में y द्वारा कोडित सूत्र को सिद्ध करता है\"।",
            zh: "哥德尔编号:为每个公式 φ 指派唯一自然数 ⌜φ⌝。F 中的可证性化为原始递归谓词 \
                 Prov_F(x, y),意为 \"x 编码一个 F 中的证明,证明的目标公式编号为 y\"。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en: "Diagonal lemma: for the formula ψ(y) ≔ ¬∃x Prov_F(x, y) (\"y is not provable in \
                 F\") there exists a sentence G_F with ⌜G_F⌝ = n such that F ⊢ G_F ↔ ψ(n). \
                 Intuitively G_F says \"I am not provable in F\".",
            ru: "Диагональная лемма: для формулы ψ(y) ≔ ¬∃x Prov_F(x, y) («y недоказуемо в F») \
                 существует утверждение G_F с ⌜G_F⌝ = n, для которого F ⊢ G_F ↔ ψ(n). \
                 По существу G_F утверждает: «Я недоказуемо в F».",
            hi: "विकर्ण लेम्मा: सूत्र ψ(y) ≔ ¬∃x Prov_F(x, y) (\"y, F में साध्य नहीं है\") के \
                 लिए एक कथन G_F है, ⌜G_F⌝ = n, ऐसा कि F ⊢ G_F ↔ ψ(n)। तात्पर्य: G_F कहता है \
                 \"मैं F में साध्य नहीं हूँ\"।",
            zh: "对角引理:对公式 ψ(y) ≔ ¬∃x Prov_F(x, y)(\"y 在 F 中不可证\"),\
                 存在句子 G_F 使得 ⌜G_F⌝ = n 且 F ⊢ G_F ↔ ψ(n)。直观上 G_F 表示 \"我在 F 中不可证\"。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en: "Suppose F ⊢ G_F. Then there exists a proof code m with Prov_F(m, n), so by the \
                 equivalence F ⊢ ¬G_F too, contradicting the consistency of F. Hence F ⊬ G_F.",
            ru: "Предположим F ⊢ G_F. Тогда найдётся код доказательства m с Prov_F(m, n), и по \
                 эквивалентности F ⊢ ¬G_F, что противоречит непротиворечивости F. Значит \
                 F ⊬ G_F.",
            hi: "मान लीजिए F ⊢ G_F। तब किसी प्रमाण कोड m के लिए Prov_F(m, n) होगा, और \
                 तुल्यता से F ⊢ ¬G_F भी होगा, जो F की सुसंगति का विरोध करता है। अतः F ⊬ G_F।",
            zh: "若 F ⊢ G_F,则存在证明编码 m 使 Prov_F(m, n) 成立,根据等价 F ⊢ ¬G_F,\
                 与 F 的一致性矛盾。故 F ⊬ G_F。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en: "Suppose F ⊢ ¬G_F. Then F ⊢ ∃x Prov_F(x, n), yet by the previous step no actual \
                 proof of G_F exists in F. A standard ω-consistency (or 1-consistency, in \
                 Rosser's strengthening) argument turns this into another contradiction; hence \
                 F ⊬ ¬G_F.",
            ru: "Предположим F ⊢ ¬G_F. Тогда F ⊢ ∃x Prov_F(x, n), однако из предыдущего шага \
                 настоящего доказательства G_F в F нет. Стандартный аргумент ω-непротиворечивости \
                 (или 1-непротиворечивости в усилении Россера) превращает это во второе \
                 противоречие; следовательно F ⊬ ¬G_F.",
            hi: "मान लीजिए F ⊢ ¬G_F। तब F ⊢ ∃x Prov_F(x, n) होगा, परन्तु पिछले चरण के अनुसार \
                 F में G_F का वास्तविक प्रमाण नहीं है। मानक ω-संगति (या रोसर-वर्धित \
                 1-संगति) तर्क इसे एक दूसरे विरोधाभास में बदलता है; अतः F ⊬ ¬G_F।",
            zh: "若 F ⊢ ¬G_F,则 F ⊢ ∃x Prov_F(x, n),然而由上一步,在 F 中并不存在 G_F 的实际证明。\
                 标准 ω-一致性(或 Rosser 加强的 1-一致性)论证将其转为又一矛盾,故 F ⊬ ¬G_F。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en: "G_F is therefore independent of F. Since the metatheory sees that G_F holds \
                 (because every actual proof in F would be visible to the metatheory and none \
                 exists), G_F is a true arithmetical sentence that F cannot decide.",
            ru: "Значит, G_F независимо от F. Метатеория видит, что G_F истинно (любое реальное \
                 доказательство в F было бы заметно метатеории, а его нет), поэтому G_F — \
                 истинное арифметическое утверждение, не разрешаемое в F.",
            hi: "अतः G_F, F से स्वतंत्र है। मेटा-सिद्धांत में दिखता है कि G_F सत्य है \
                 (F का कोई भी वास्तविक प्रमाण मेटा-सिद्धांत में दिखाई देगा, परंतु ऐसा कोई नहीं है), \
                 इसलिए G_F एक सत्य अंकगणितीय कथन है जिसे F निर्णीत नहीं कर सकता।",
            zh: "故 G_F 独立于 F。元理论可见 G_F 为真(F 内任何真实证明均会显现于元理论中,\
                 但并不存在),所以 G_F 是 F 无法判定的真算术语句。",
        },
    ],
    conclusion_en: "F is incomplete: a true sentence about natural numbers escapes its proof \
                    system. ∎",
    conclusion_ru: "F неполна: истинное утверждение о натуральных числах ускользает от её системы \
                    доказательств. ∎",
    conclusion_hi: "F अपूर्ण है: प्राकृतिक संख्याओं के बारे में एक सत्य कथन उसकी प्रमाण-व्यवस्था से \
                    बच निकलता है। ∎",
    conclusion_zh: "故 F 不完备:存在关于自然数的真语句逸出其证明系统。∎",
};

const LAPLACIAN_DETERMINISM: KnownTheoremEntry = KnownTheoremEntry {
    id: "laplacian_determinism",
    method: ProofMethod::AxiomReduction,
    match_keywords: &[
        "determinism",
        "deterministic",
        "детерминизм",
        "детерминирован",
        "决定论",
        "निर्धारणवाद",
    ],
    statement_en:
        "Within the Newtonian axiom set N = (Euclidean space, smooth time, Newton's second law \
         F = m·ẍ, Lipschitz-bounded forces), the future trajectory of every closed mechanical \
         system is uniquely determined by its present state (Laplacian determinism).",
    statement_ru:
        "В аксиоматике Ньютона N = (евклидово пространство, гладкое время, второй закон Ньютона \
         F = m·ẍ, силы с ограничением Липшица) будущая траектория каждой замкнутой механической \
         системы однозначно определена её текущим состоянием (лапласовский детерминизм).",
    statement_hi:
        "न्यूटनीय अभिगृहीत समुच्चय N = (यूक्लिडीय आकाश, सतत काल, न्यूटन का द्वितीय नियम \
         F = m·ẍ, लिप्शिट्ज़-सीमित बल) के अंतर्गत हर बंद यांत्रिक तंत्र की भविष्य प्रक्षेपवक्र \
         उसकी वर्तमान अवस्था से अद्वितीय रूप से निर्धारित होती है (Laplace का निर्धारणवाद)।",
    statement_zh: "在牛顿公理集 N =(欧氏空间、光滑时间、牛顿第二定律 F = m·ẍ、\
                   Lipschitz 受限力场)下,任意闭合力学系统的未来轨道由其当前状态唯一决定\
                   (拉普拉斯式决定论)。",
    steps: &[
        LocalizedStep {
            kind: StepKind::Axiom,
            en: "Take the axiom set N: configuration space ℝᵈ with the standard Euclidean \
                 structure, time ∈ ℝ, mass m > 0, and a force field F: ℝᵈ × ℝᵈ × ℝ → ℝᵈ that is \
                 Lipschitz-continuous in position and velocity.",
            ru: "Возьмём аксиоматику N: конфигурационное пространство ℝᵈ с евклидовой \
                 структурой, время ∈ ℝ, масса m > 0 и силовое поле \
                 F: ℝᵈ × ℝᵈ × ℝ → ℝᵈ, липшицевое по координатам и скоростям.",
            hi: "अभिगृहीत समुच्चय N: कॉन्फ़िगरेशन स्पेस ℝᵈ यूक्लिडीय संरचना के साथ, समय ∈ ℝ, \
                 द्रव्यमान m > 0, और बल क्षेत्र F: ℝᵈ × ℝᵈ × ℝ → ℝᵈ जो स्थिति और वेग में \
                 लिप्शिट्ज़-संतत है।",
            zh: "取公理集 N:位形空间 ℝᵈ 配欧氏结构、时间 ∈ ℝ、质量 m > 0,以及在位置与速度上\
                 Lipschitz 连续的力场 F: ℝᵈ × ℝᵈ × ℝ → ℝᵈ。",
        },
        LocalizedStep {
            kind: StepKind::Definition,
            en: "A state of the system at time t₀ is the pair s₀ = (x(t₀), ẋ(t₀)). Newton's \
                 second law turns the dynamics into the first-order ODE \
                 (ẋ, v̇) = (v, F(x, v, t)/m).",
            ru: "Состояние системы в момент t₀ — это пара s₀ = (x(t₀), ẋ(t₀)). Второй закон \
                 Ньютона превращает динамику в систему ОДУ первого порядка \
                 (ẋ, v̇) = (v, F(x, v, t)/m).",
            hi: "समय t₀ पर तंत्र की अवस्था युग्म s₀ = (x(t₀), ẋ(t₀)) है। न्यूटन का द्वितीय \
                 नियम गतिकी को प्रथम-कोटि ODE (ẋ, v̇) = (v, F(x, v, t)/m) में बदलता है।",
            zh: "系统在 t₀ 时刻的状态为 s₀ = (x(t₀), ẋ(t₀))。牛顿第二定律将动力学化为一阶常微分方程组 \
                 (ẋ, v̇) = (v, F(x, v, t)/m)。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en: "Apply the Picard–Lindelöf theorem: a Lipschitz right-hand side on an open \
                 neighbourhood of (s₀, t₀) gives a unique maximal solution s(t) through that \
                 initial condition.",
            ru: "Применим теорему Пикара–Линделёфа: липшицева правая часть в окрестности \
                 (s₀, t₀) даёт единственное максимальное решение s(t), проходящее через это \
                 начальное условие.",
            hi: "Picard–Lindelöf प्रमेय लागू करें: (s₀, t₀) के एक खुले प्रांत में लिप्शिट्ज़ \
                 दायाँ पक्ष उस आरंभिक शर्त से होकर गुजरने वाला एक अद्वितीय अधिकतम हल s(t) देता है।",
            zh: "应用 Picard–Lindelöf 定理:在 (s₀, t₀) 的开邻域上 Lipschitz 的右端项确保过该初值\
                 存在唯一的极大解 s(t)。",
        },
        LocalizedStep {
            kind: StepKind::Inference,
            en: "Hence two trajectories that agree at t₀ agree on the entire common domain of \
                 existence; equivalently, the time-t evolution Φ_t : (s₀, t₀) ↦ s(t₀ + t) is a \
                 well-defined function on the state space.",
            ru: "Следовательно, две траектории, совпадающие в t₀, совпадают на всей общей \
                 области существования; иначе говоря, эволюция за время t \
                 Φ_t : (s₀, t₀) ↦ s(t₀ + t) — корректно определённая функция на пространстве \
                 состояний.",
            hi: "अतः जो दो प्रक्षेपवक्र t₀ पर मेल खाते हैं, वे संपूर्ण सामान्य अस्तित्व-प्रांत पर \
                 मेल खाते हैं; तुल्य रूप से, समय-t विकास Φ_t : (s₀, t₀) ↦ s(t₀ + t) \
                 अवस्था-स्थान पर सुपरिभाषित फलन है।",
            zh: "故凡在 t₀ 时刻重合的两条轨道在共同存在域上完全一致;\
                 等价地,时间 t 演化 Φ_t : (s₀, t₀) ↦ s(t₀ + t) 在状态空间上是良定义的函数。",
        },
        LocalizedStep {
            kind: StepKind::SubProof,
            en: "Note (Gödel-style limit): the proof above is reductive — it transfers \
                 determinism to existence and uniqueness of solutions of an ODE. The statement \
                 \"physical reality is deterministic\" is not formally decidable inside N; it \
                 becomes decidable only after fixing both the axioms of physics and the \
                 metalanguage. Inside a richer axiom set (e.g. one that interprets PA), Gödel's \
                 first incompleteness theorem forbids a complete internal certificate of \
                 determinism.",
            ru: "Замечание (граница в духе Гёделя): доказательство сведено — детерминизм \
                 переведён в вопрос существования и единственности решений ОДУ. Утверждение \
                 «физическая реальность детерминирована» формально не разрешимо внутри N; оно \
                 становится разрешимым только после фиксации аксиом физики и металогики. В более \
                 богатой системе (например, интерпретирующей арифметику Пеано) первая теорема \
                 Гёделя запрещает полный внутренний сертификат детерминизма.",
            hi: "टिप्पणी (गोडेल-शैली सीमा): उपरोक्त प्रमाण निरूपण-मूलक है — निर्धारणवाद को ODE \
                 के समाधान के अस्तित्व और अद्वितीयता पर स्थानांतरित किया गया है। \"भौतिक यथार्थ \
                 निर्धारित है\" कथन N के भीतर औपचारिक रूप से निर्णीत नहीं है; यह केवल भौतिकी \
                 के अभिगृहीत और मेटा-भाषा तय कर लेने पर निर्णीत होता है। अधिक समृद्ध तंत्र (जो \
                 PA का अर्थ करे) में गोडेल का प्रथम अपूर्णता प्रमेय निर्धारणवाद के पूर्ण आंतरिक \
                 प्रमाणपत्र को रोक देता है।",
            zh: "注(哥德尔式界限):以上证明是化归式的——把决定论化归为常微分方程解的存在唯一性。\
                 \"物理现实是决定论的\" 这一断言在 N 内部并非形式可判定,只有在固定物理公理与元语言之后\
                 才能讨论。在更丰富的公理系统(可表达 PA)中,哥德尔第一不完备定理禁止给出关于\
                 决定论的完全内部证书。",
        },
    ],
    conclusion_en: "Under the axiom set N, Laplacian determinism holds for every closed \
                    mechanical system; outside N (or inside any system interpreting PA), the \
                    statement is not formally complete in the sense of Gödel. ∎",
    conclusion_ru: "В аксиоматике N лапласовский детерминизм выполнен для любой замкнутой \
                    механической системы; вне N (или в системе, интерпретирующей PA) утверждение \
                    формально неполно по Гёделю. ∎",
    conclusion_hi: "अभिगृहीत समुच्चय N के अंतर्गत हर बंद यांत्रिक तंत्र के लिए Laplace का \
                    निर्धारणवाद सिद्ध है; N के बाहर (या PA का अर्थ करने वाले किसी तंत्र में) \
                    यह कथन गोडेल के अर्थ में औपचारिक रूप से पूर्ण नहीं है। ∎",
    conclusion_zh: "在公理集 N 下,任意闭合力学系统的拉普拉斯式决定论成立;在 N 之外\
                    (或任一可表达 PA 的系统中),该断言按哥德尔意义并非形式完备。∎",
};

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn pythagoras_matches_english() {
        assert!(PYTHAGOREAN.matches("can you prove the pythagorean theorem"));
    }

    #[test]
    fn pythagoras_matches_russian() {
        assert!(PYTHAGOREAN.matches("докажите теорему пифагора"));
    }

    #[test]
    fn fermat_little_matches_chinese() {
        assert!(FERMAT_LITTLE.matches("证明费马小定理"));
    }

    #[test]
    fn euclid_primes_matches_english() {
        assert!(EUCLID_INFINITUDE_OF_PRIMES
            .matches("demonstrate that there are infinitely many primes"));
    }

    #[test]
    fn sqrt_two_matches_english() {
        assert!(SQRT_TWO_IRRATIONAL.matches("show that the square root of two is irrational"));
    }

    #[test]
    fn godel_matches_english() {
        assert!(GODEL_FIRST_INCOMPLETENESS.matches("godel's incompleteness"));
    }

    #[test]
    fn determinism_matches_english() {
        assert!(LAPLACIAN_DETERMINISM.matches("prove determinism"));
    }

    #[test]
    fn build_proof_returns_localized_text() {
        let proof = PYTHAGOREAN.build_proof("ru");
        assert!(proof.statement.contains("прямоугольном"));
        assert!(proof.conclusion.contains("∎"));
        assert!(!proof.steps.is_empty());
    }

    #[test]
    fn registry_lookup_is_first_match_wins() {
        // The Gödel entry should match when both Gödel and determinism appear, ensuring the
        // engine handles the issue-185 prompt deterministically.
        let prompt =
            "prove determinism the way logic can handle paradoxes like godel's math incompleteness";
        let mut godel_index = None;
        let mut determinism_index = None;
        for (index, entry) in REGISTRY.iter().enumerate() {
            if entry.matches(prompt) {
                if entry.id == "godel_first_incompleteness" && godel_index.is_none() {
                    godel_index = Some(index);
                }
                if entry.id == "laplacian_determinism" && determinism_index.is_none() {
                    determinism_index = Some(index);
                }
            }
        }
        assert!(
            godel_index.is_some(),
            "godel entry should match the issue prompt"
        );
        assert!(
            determinism_index.is_some(),
            "determinism entry should match the issue prompt"
        );
        assert!(
            godel_index < determinism_index,
            "godel entry must precede determinism in REGISTRY"
        );
    }
}