README.md
COS Method
README.md
1 # Quadratic-Form Engine / K-COS Lean companion
2
3 This project checks 26 exact finite-real algebra and enclosure/error-budget
4 theorems, with 8 definitions. It is the scoped formal companion to the final
5 traditional manuscript and visual guide. Gaussian and spectral reduction,
6 COS/tilting analysis, remainder bounds, and numerical interval-library
7 correctness are not formalized by these modules.
8
9 Read `Quadratic_Form_KCOS_Lean_Guide.pdf` or its `.md`/`.tex` source for exact
10 hypotheses and remaining obligations. `Declaration_Inventory.json` lists every
11 project declaration and signature. `Claim_Lean_Concordance.json` maps only the
12 proved component of each manuscript claim to its declaration.
13
14 On a normal Lean installation, from this directory:
15
16 ```sh
17 lake update
18 lake exe cache get
19 python3 verify.py
20 ```
21
22 The toolchain and Mathlib dependency are pinned. `verify.py` runs the project
23 build, fresh direct source checks, declaration/axiom audit and positive and
24 negative compiler controls. It fails if counts, source admissions, axiom sets,
25 compiler version or Mathlib revision differ from the recorded contract.
26
27 The accepted mathematical modules are `KomorebiQCOS/FiniteGram.lean` and
28 `KomorebiQCOS/Certificates.lean`. `verification/controls/FalseArithmetic.lean`
29 and `verification/controls/MissingBudget.lean` intentionally fail. Do not import
30 them into the mathematical library. Their rejection is evidence that a false
31 arithmetic statement and a missing acceptance premise are not silently proved.
32
33 Fresh producer evidence is in `verification/BUILD_AUDIT.json` and companion
34 logs. `verification/runtime/RUNTIME.md` explains runtime retrieval and the
35 narrow process-self-location adapter used in this environment. Compiler and
36 Mathlib binaries are omitted from the publication package.