Apache License
                        Version 2.0, January 2004
                     http://www.apache.org/licenses/

TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION

1. Definitions.

   "License" shall mean the terms and conditions for use, reproduction,
   and distribution as defined by Sections 1 through 9 of this document.

   "Licensor" shall mean the copyright owner or entity authorized by the
   copyright owner that is granting the License.

   "Legal Entity" shall mean the union of the acting entity and all other
   entities that control, are controlled by, or are under common control
   with that entity.

   "You" (or "Your") shall mean an individual or Legal Entity exercising
   permissions granted by this License.

   "Source" form shall mean the preferred form for making modifications.

   "Object" form shall mean any form resulting from mechanical transformation
   or translation of a Source form.

   "Work" shall mean the work of authorship made available under the License.

   "Derivative Works" shall mean any work that is based on the Work.

   "Contribution" shall mean any work of authorship submitted to the Licensor
   for inclusion in the Work.

   "Contributor" shall mean Licensor and any Legal Entity on behalf of whom
   a Contribution has been received by the Licensor.

2. Grant of Copyright License. Subject to the terms and conditions of this
   License, each Contributor hereby grants to You a perpetual, worldwide,
   non-exclusive, no-charge, royalty-free, irrevocable copyright license to
   reproduce, prepare Derivative Works of, publicly display, publicly
   perform, sublicense, and distribute the Work and such Derivative Works
   in Source or Object form.

3. Grant of Patent License. Subject to the terms and conditions of this
   License, each Contributor hereby grants to You a perpetual, worldwide,
   non-exclusive, no-charge, royalty-free, irrevocable patent license to
   make, have made, use, offer to sell, sell, import, and otherwise transfer
   the Work.

4. Redistribution. You may reproduce and distribute copies of the Work or
   Derivative Works thereof in any medium, with or without modifications,
   and in Source or Object form, provided that You meet the following
   conditions:

   (a) You must give any other recipients of the Work or Derivative Works
       a copy of this License; and

   (b) You must cause any modified files to carry prominent notices stating
       that You changed the files; and

   (c) You must retain, in the Source form of any Derivative Works that You
       distribute, all copyright, patent, trademark, and attribution notices
       from the Source form of the Work; and

   (d) If the Work includes a "NOTICE" text file, You must include a
       readable copy of the attribution notices contained within such
       NOTICE file.

5. Submission of Contributions. Unless You explicitly state otherwise, any
   Contribution intentionally submitted for inclusion in the Work by You to
   the Licensor shall be under the terms and conditions of this License.

6. Trademarks. This License does not grant permission to use the trade
   names, trademarks, service marks, or product names of the Licensor.

7. Disclaimer of Warranty. The Work is provided on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND.

8. Limitation of Liability. In no event shall any Contributor be liable to
   You for damages, including any direct, indirect, special, incidental, or
   consequential damages of any character arising as a result of this
   License or out of the use or inability to use the Work.

9. Accepting Warranty or Additional Liability. While redistributing the
   Work or Derivative Works thereof, You may choose to offer, and charge a
   fee for, acceptance of support, warranty, indemnity, or other liability
   obligations consistent with this License.

END OF TERMS AND CONDITIONS

Copyright (c) 2026 Dhruv Gupta

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
implied. See the License for the specific language governing
permissions and limitations under the License.

===========================================================================
NOTICE: PRIOR ART DISCLOSURE AND CITATION REQUEST
===========================================================================

This repository constitutes prior art in the following domains as of the
dates recorded in the git history (earliest commit: March 18, 2026):

1. FORMAL VERIFICATION OF LEARNING THEORY
   Machine-checked proofs of the Fundamental Theorem of Statistical
   Learning (5-way equivalence), the Littlestone characterization of
   online learnability, Gold's theorem on identification in the limit,
   and all paradigm separation theorems with constructive witnesses.

2. TYPE-THEORETIC STRUCTURE OF COMPUTATIONAL LEARNING
   Discovery and formal documentation of structural fractures and
   design tradeoffs in the type theory of computational learning,
   revealed by forcing the field through a dependently typed proof
   assistant.

3. MEASURE-THEORETIC CORRECTIONS TO TEXTBOOK LEARNING THEORY
   Formal proofs that: (a) the No-Free-Lunch theorem is provably false
   for finite domains; (b) the standard branch-wise Littlestone tree
   definition admits a counterexample; (c) uniform convergence for
   uncountable concept classes requires NullMeasurableSet, not
   MeasurableSet; (d) quantifier ordering in uniform convergence is
   load-bearing for distribution-free guarantees.

4. AI-ASSISTED FORMAL MATHEMATICS METHODOLOGY
   The methodology of type-architecture-first proof discovery using
   frontier language models (premise creation followed by supervised
   proof search within a pre-validated type structure).

5. FORMALIZATION TECHNIQUES FOR UNCOUNTABLE STRUCTURES
   The measurable inner event pattern, NullMeasurableSet integration
   lemmas, 7/12-fraction Chebyshev boosting, doubled-count arithmetic
   normalization, and three-step pullback chains for product-space
   measure transport.

CITATION: If you use, adapt, or build upon this work in any publication,
software, or derivative work, please cite:

  Gupta, D. (2026). Formal Learning Theory Kernel: Lean4 Formalization
  of the Fundamental Theorem of Statistical Learning.
  https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel

  @software{gupta2026flt_kernel,
    author = {Gupta, Dhruv},
    title  = {Formal Learning Theory Kernel: {Lean4} Formalization
              of the Fundamental Theorem of Statistical Learning},
    year   = {2026},
    url    = {https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel}
  }