OAI/Computability/Superstring/Main.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Superstring.bitsList_eq_encodeList line 8
2. theorem OAI.Superstring.bitsSymbol_eq line 16
3. theorem OAI.Superstring.bitsWord_eq line 19
4. theorem OAI.Superstring.bitsInstance_eq line 22
5. def OAI.Superstring.answer line 25
6. theorem OAI.Superstring.answer_poly line 27
7. theorem OAI.Superstring.answer_implementation line 34
8. theorem OAI.Superstring.weight_le_opt_with line 42
9. theorem OAI.Superstring.answer_spec line 48
10. theorem OAI.Superstring.main line 57

    Source documentation

    The deterministic algorithm with its exact finite-alphabet bit-machine certificate, contiguous coverage, and factor-two bound in symbols.

    Distinct definitions of this name: ComparatorChallenges/Superstring.lean:36 (same statement text; different proof or body). Qualify references as OAI.Superstring.main@path.

    theorem main : ∃ f : Instance → Word,
        HasPolynomialImplementation f ∧
        ∀ S, IsCommonSuperstring S (f S) ∧ (f S).length ≤ 2 * opt S :=
    …

    Mentions: OAI.Superstring.Instance, OAI.Superstring.Word, OAI.Superstring.HasPolynomialImplementation, OAI.Superstring.IsCommonSuperstring, OAI.Superstring.opt