feat: expand verified runtime and numerical foundations

Author: Robertboy18

CONTRIBUTING.md

@@ -237,30 +237,6 @@ Project conventions:
 - Keep executable examples and proof code separate when they have different trust assumptions.
 - Avoid introducing axioms. If one is unavoidable, quarantine and document it.
 
-## Checking Untrusted Proofs
-
-TorchLean includes a wrapper for `leanprover/comparator`, which can compare a trusted
-`Challenge.lean` against an untrusted `Solution.lean` inside a `landrun` sandbox.
-
-Prerequisite:
-
-- Install `landrun` and make sure it is on `PATH`: https://github.com/Zouuup/landrun
-
-Typical workflow:
-
-1. Create a separate small Lake project with `Challenge.lean`, `Solution.lean`, and a comparator
-   JSON config.
-2. Make that project depend on TorchLean, for example:
-   `require TorchLean from "/path/to/TorchLean"`.
-3. Run:
-
-```bash
-python3 /path/to/TorchLean/scripts/sandbox/run_comparator.py ./config.json --project .
-```
-
-See `https://github.com/leanprover/comparator` for the JSON schema and default axiom allowlist
-pattern.
-
 ## PR Checklist
 
 - `lake build` succeeds from a clean checkout.

NN/API.lean

@@ -6,21 +6,34 @@ Authors: TorchLean Team
 
 module
 
-public import NN.API.Public.Facade
 public import NN.API.Adapters
-public import NN.API.Models.Generative
+public import NN.API.CLI
+public import NN.API.Checkpoint
+public import NN.API.Scalar
+public import NN.API.Data
+public import NN.API.Json
+public import NN.API.Loss
+public import NN.API.Module
+public import NN.API.Neural
+public import NN.API.Optim
+public import NN.API.RL
+public import NN.API.Runtime
 public import NN.API.SelfSupervised
+public import NN.API.Tensor
+public import NN.API.TensorPack
+public import NN.API.Text
+public import NN.API.Trainer
+public import NN.API.Verification
+public import NN.Spec.Models
 
 /-!
-# TorchLean API
+# TorchLean
 
-The focused import for applications that want TorchLean's concise `TorchLean.*` interface without
-loading the proof, verification, floating-point, and widget subsystems.
+Neural-network construction, training, runtime execution, datasets, automatic differentiation,
+verification, and mathematical model specifications.
 
-The main namespaces are `TorchLean.nn` for neural networks, `TorchLean.classical` for classical
-and statistical models, `TorchLean.Trainer` for training, `TorchLean.optim` for optimizers, and
-`TorchLean.Data` for datasets. Use `import NN` when the same file also needs specifications,
-proofs, verification, or backend internals.
+Import `NN.API` for model code. Import `NN` when a file also uses the specification, proof,
+floating-point, or backend libraries.
 -/
 
 @[expose] public section

NN/API/Adapters.lean

@@ -6,11 +6,61 @@ Authors: TorchLean Team
 
 module
 
-public import NN.API.Adapters.LoRA
+public import NN.Spec.Core.Tensor
+public import NN.Spec.Core.Tensor.Linalg
+public import NN.Spec.Core.TensorOps
 
 /-!
-# Adapter APIs
+# Low-Rank Adapters
 
-Small reusable adapters that can be attached to existing models without changing the model
-definition itself.
+LoRA represents a linear-weight update as two smaller matrices. For a base weight
+$W : \mathbb{R}^{d_{in}\times d_{out}}$, an adapter of rank $r$ uses
+$A : \mathbb{R}^{d_{in}\times r}$ and $B : \mathbb{R}^{r\times d_{out}}$:
+
+$$W_{eff}=W+sAB.$$
+
+The matrix orientation agrees with TorchLean's row-batch linear layers. This module defines the
+typed update and its action on a batch; the training code decides which parameters to optimize.
+
+Reference: Hu et al., “LoRA: Low-Rank Adaptation of Large Language Models” (2021),
+https://arxiv.org/abs/2106.09685.
 -/
+
+@[expose] public section
+
+namespace TorchLean.Adapters.LoRA
+
+open _root_.Spec
+open _root_.Spec.Tensor
+
+/-- LoRA factors for a linear weight of shape `inDim × outDim`. -/
+structure Params (α : Type) (inDim rank outDim : Nat) where
+  /-- Projection from the input dimension to the adapter rank. -/
+  A : Tensor α (.dim inDim (.dim rank .scalar))
+  /-- Projection from the adapter rank to the output dimension. -/
+  B : Tensor α (.dim rank (.dim outDim .scalar))
+
+/-- The scaled low-rank update $sAB$. -/
+def delta {α : Type} [Add α] [Mul α] [Zero α]
+    {inDim rank outDim : Nat} (p : Params α inDim rank outDim) (scale : α) :
+    Tensor α (.dim inDim (.dim outDim .scalar)) :=
+  scaleSpec (matMulSpec p.A p.B) scale
+
+/-- Add a LoRA update to a base linear weight. -/
+def effectiveWeight {α : Type} [Add α] [Mul α] [Sub α] [Zero α]
+    {inDim rank outDim : Nat}
+    (base : Tensor α (.dim inDim (.dim outDim .scalar)))
+    (p : Params α inDim rank outDim) (scale : α) :
+    Tensor α (.dim inDim (.dim outDim .scalar)) :=
+  addSpec base (delta p scale)
+
+/-- Apply a linear map whose weight is augmented by a LoRA update. -/
+def linear {α : Type} [Add α] [Mul α] [Sub α] [Zero α]
+    {batch inDim rank outDim : Nat}
+    (x : Tensor α (.dim batch (.dim inDim .scalar)))
+    (base : Tensor α (.dim inDim (.dim outDim .scalar)))
+    (p : Params α inDim rank outDim) (scale : α) :
+    Tensor α (.dim batch (.dim outDim .scalar)) :=
+  matMulSpec x (effectiveWeight base p scale)
+
+end TorchLean.Adapters.LoRA