From 7a973a06f6745278e76a1e28d131fa9259bd4570 Mon Sep 17 00:00:00 2001 From: allaun Date: Sun, 21 Jun 2026 06:30:12 -0500 Subject: [PATCH] feat(core): harden SilverSightCore and port canonical FixedPoint - Remove Float from Core/SilverSightCore.lean (Receipt.pathCost is now Option Nat) - Prove TIC theorems tic_never_decreases and computation_generates_time - Add lakefile.lean, lean-toolchain, and .gitignore for .lake/ - Port Research-Stack Semantics.FixedPoint.lean to formal/CoreFormalism/FixedPoint.lean - Delete thin Q16_16_Spec.lean; update Python/QUBO comments and docs - Create AGENTS.md distilled from Research Stack core bindings - Update REBASE_RULES.md to strip legacy hacks and reference AGENTS.md Build: 2978 jobs, 0 errors (lake build) --- .gitignore | 1 + AGENTS.md | 274 ++++++ Core/SilverSightCore.lean | 104 +- PORTING_MAP.md | 6 +- README.md | 2 +- REBASE_RULES.md | 55 +- formal/CoreFormalism/FixedPoint.lean | 1311 +++++++++++++++++++++++++ formal/CoreFormalism/Q16_16_Spec.lean | 292 ------ lake-manifest.json | 96 ++ lakefile.lean | 22 + lean-toolchain | 1 + python/q16_canonical.py | 2 +- qubo/finsler_metric.py | 2 +- tests/q16_roundtrip_test.py | 2 +- 14 files changed, 1834 insertions(+), 336 deletions(-) create mode 100644 AGENTS.md create mode 100644 formal/CoreFormalism/FixedPoint.lean delete mode 100644 formal/CoreFormalism/Q16_16_Spec.lean create mode 100644 lake-manifest.json create mode 100644 lakefile.lean create mode 100644 lean-toolchain diff --git a/.gitignore b/.gitignore index ddea5a8d..73577294 100644 --- a/.gitignore +++ b/.gitignore @@ -9,3 +9,4 @@ __pycache__/ .mcp/ env/ venv/ +.lake/ diff --git a/AGENTS.md b/AGENTS.md new file mode 100644 index 00000000..3f9d2b07 --- /dev/null +++ b/AGENTS.md @@ -0,0 +1,274 @@ +# AGENTS.md — SilverSight Operating Contract + +**Principle:** *Port the contracts and the rituals, not the state.* + +This file distills the surviving rules from Research Stack and rebases them onto +SilverSight's library-method architecture. Legacy deployment details, stale +benchmark tables, and repo-specific paths have been stripped. The conceptual +bindings — Lean authority, no-Float compute, receipt boundaries, and the +post-interaction ritual — remain in force. + +--- + +## 1. Project Architecture + +SilverSight is organized as a minimal invariant core plus independent libraries. + +``` +Core/ + SilverSightCore.lean ← no imports, no Float, no library code +formal/ + CoreFormalism/ ← Q16_16, Hachimoji, Chentsov, Sidon + PVGS_DQ_Bridge/ ← quantum bridge + UniversalEncoding/ ← math address space + BindingSite/ ← biological binding sketches +python/ ← I/O, feature extraction, orchestration +qubo/ ← optimization libraries +tests/ ← verification fixtures +docs/ ← architecture and placement docs +``` + +### Library method + +- **Core defines the contract.** Libraries implement it. +- `Core/SilverSightCore.lean` imports nothing and depends on nothing. +- Every library may import `Core/` but may **not** import another library. +- The `Receipt` is the only interface between Core and libraries. + +--- + +## 2. The No-Float Law + +**No `Float` in Lean compute paths.** This is non-negotiable. + +- Use `Q16_16.ofNat`, `Q16_16.ofRatio`, or `Q16_16.ofRawInt` for all core + arithmetic. +- `ofFloat` is permitted **only** at external boundaries (JSON parsing, sensor + input) and must be immediately bracketed/converted. +- `Float` is forbidden in `Core/` entirely. `Receipt.pathCost` is an `Option Nat` + (raw fixed-point integer), not `Option Float`. +- The canonical fixed-point implementation is + `formal/CoreFormalism/FixedPoint.lean`, ported from Research Stack + `Semantics.FixedPoint.lean` with boundary conversions removed from compute + paths. + +--- + +## 3. Programming Choice Flow + +Before writing or placing any new logic, run through this decision tree in order. +Stop at the first rule that applies. + +``` +New logic needed? +│ +├── Does it make an admissibility, routing, alignment, or gating decision? +│ └── YES → Write it in Lean. No Python equivalent allowed. +│ File: formal/CoreFormalism/*.lean or a new formal/*.lean module. +│ +├── Does it mint, stamp, or emit a top-level receipt or JSON bundle? +│ └── YES → It belongs in Core receipt validators or the designated emitter. +│ Python may format/store, but Lean stamps the decision. +│ +├── Does it classify rows, run an alignment gate, or compute scores? +│ └── YES → Lean. Python may call it via #eval / lake exe but may not +│ replicate the logic. +│ +├── Does it supply raw input features (expression text, route_hint, domain_type, +│ equation_id hashing, weak_axes count)? +│ └── YES → Python shim is acceptable. The shim must: +│ (a) produce only a raw data structure +│ (b) carry no admissibility logic +│ (c) be regenerable from source +│ (d) live in python/ or qubo/ with a TODO(lean-port) if the logic +│ could eventually move to Lean +│ +├── Does it use floating-point arithmetic in a compute path? +│ └── YES → STOP. Use Q16_16.ofNat / Q16_16.ofRatio / Q16_16.ofRawInt. +│ +├── Does it advance promotion status (e.g. set promotion = "promoted")? +│ └── YES → STOP. Promotion is always not_promoted until a Lean gate +│ explicitly passes. Never advance it in shim space or by hand. +│ +└── Is it pure I/O (read JSON, write JSONL, call subprocess, format output)? + └── YES → Python shim is fine. Keep it in python/ or qubo/. +``` + +**Summary:** Lean owns all decisions. Python owns all I/O. + +--- + +## 4. Receipt Contract + +The `Receipt` is the compressed interface record. It is not metadata around a +result; it **is** the result. + +```lean +structure Receipt where + receiptID : String + expression : String + finalState : HachimojiState + ticCount : Nat + fuelUsed : Nat + pathCost : Option Nat -- raw integer cost; never Float + libraryRefs : List String + verified : Bool +``` + +- Libraries produce receipts. The core consumes them. +- A receipt proves only the gate it actually checks. +- Receipt validation lives in `Core/SilverSightCore.lean`. + +--- + +## 5. AVM and TIC Axiom + +The Abstract Virtual Machine (AVM) is a stack machine defined in Core. + +- `δ : AVMState × Instruction → AVMState` is the sole transition function. +- **TIC axiom:** TIC is derived from events, never the driver. + - `T_{n+1} = T_n + E(S_n)` where `E ≥ 0` + - `δ` never decreases TIC. + - Meaningful computation (`finalState ≠ Ζ`) implies `ticCount > 0`. + +--- + +## 6. Verification Expectations + +- For Lean changes, run the narrow target first, then `lake build` when feasible. +- For Python shims, run `python3 -m py_compile` on touched files. +- For JSON receipts, run `python3 -m json.tool`. +- Before committing, run `git diff --cached --check` and scan touched files for + secrets. + +--- + +## 7. Post-Interaction Workflow (mandatory) + +After any code, Lean, shim, receipt, or architecture change: + +1. **Update the nearest scoped AGENTS.md.** + - Root or multi-subtree changes → this file. + - `Core/` changes → `Core/AGENTS.md` if one exists, otherwise this file. + - `formal/` changes → `formal/AGENTS.md` if one exists, otherwise this file. +2. **Verify the build.** + - Lean: `lake build` from the appropriate `lakefile.lean` root. + - Python: `python3 -m py_compile` on touched files. +3. **Commit.** + - Stage only explicitly touched files. **Never `git add .`.** + - Commit format: + ``` + (): + + + + Build: jobs, 0 errors (lake build) + ``` + - Types: `feat`, `fix`, `chore`, `docs`, `refactor`. + - Scopes: `core`, `formal`, `python`, `qubo`, `docs`, `infra`. +4. **Check tree cleanliness.** + ```bash + git status --branch --short --untracked-files=all + ``` + Untracked files that are not generated artifacts must be staged or noted as + intentionally dirty. + +--- + +## 8. Do Not Sweep + +Never run broad cleanup commands: + +```bash +git add . +git checkout -- . +git clean -fdx +``` + +Use explicit file lists. Generated artifacts and research scratch should stay +out of Git unless they are themselves the evidence under review. + +--- + +## 9. Git Remote Hygiene + +- The active branch may not have an upstream. Inspect with + `git rev-parse --abbrev-ref --symbolic-full-name @{u}` before assuming push + state. +- Prefer the `github` remote and verify the remote head after push: + ```bash + git fetch github + git rev-list --left-right --count FETCH_HEAD...HEAD + git push -u github + git ls-remote --heads github + ``` + +--- + +## 10. Secrets + +Secrets are runtime-only. Use environment variables (`OLLAMA_API_KEY`, +`DEEPSEEK_API_KEY`, etc.). Never paste, print, or commit literal provider keys. + +--- + +## 11. Legacy Recovery Trigger + +The phrase **`RECOVER LEGACY INFORMATION`** is the explicit retrieval trigger +for archived or quarantined concepts. + +Accepted forms: + +```text +RECOVER LEGACY INFORMATION: +Recover Legacy Information: +recover from cornfield: +``` + +Rules: + +- Inspect the requested legacy source with read-only commands first. +- Recover only the named file, concept, commit slice, or receipt. +- Modernize the recovered material onto the current clean branch. +- Never merge, reset to, or base new work on a legacy branch unless explicitly + asked. +- Preserve the legacy branch as retrievable archive state. + +Current Research Stack cornfield ref (for cross-repo lookup only): +`backup/distilled-with-vcd-history-2026-05-11`. + +--- + +## 12. Glossary + +- **Hachimoji state** — one of Φ, Λ, Ρ, Κ, Ω, Σ, Π, Ζ. The 8-state output + alphabet of the core classifier. +- **Receipt** — the machine-readable attestation record that crosses the + Core/library boundary. +- **AVM** — Abstract Virtual Machine. The stack-machine semantics defined in + `Core/SilverSightCore.lean`. +- **TIC** — Temporal Index of Computation. A monotone event counter derived from + state transitions. +- **Q16_16** — Canonical 32-bit fixed-point type (`formal/CoreFormalism/FixedPoint.lean`). +- **Library method** — Core defines contracts; libraries implement them; no + library imports another library. +- **Sidon label** — an address from a set with unique pairwise sums. Powers of + 2 are canonical for 8 strands. +- **BraidStorm** — the 8-strand braid topology used in eigensolid compression. +- **eigensolid** — converged stable state of a braid crossing loop; detected + when `crossStep(s) = s`. +- **promotion** — status advance from `not_promoted` to `promoted` only after a + Lean gate passes. + +--- + +## 13. SilverSight-Specific Boundaries + +- `Core/SilverSightCore.lean` is the root authority. It contains no sorries in + the active surface. +- `formal/CoreFormalism/FixedPoint.lean` is the canonical Q16_16 source of + truth. +- The `python/` and `qubo/` directories are I/O and optimization shims only; + they may not contain admissibility logic. +- Research artifacts and scratch output should live outside the git tree unless + promoted as durable receipts. diff --git a/Core/SilverSightCore.lean b/Core/SilverSightCore.lean index 8e66afce..65138f42 100644 --- a/Core/SilverSightCore.lean +++ b/Core/SilverSightCore.lean @@ -29,6 +29,10 @@ License: MIT -/ +import Mathlib.Data.Fintype.Basic +import Mathlib.Tactic.DeriveFintype +import Mathlib.Tactic + namespace SilverSight.Core -- ============================================================================= @@ -50,12 +54,12 @@ namespace SilverSight.Core -/ inductive HachimojiState - | Φ | Λ | Ρ | Κ | Ω | Σ | Π | Ζ + | Φ | Λ | Ρ | Κ | Ω | «Σ» | «Π» | Ζ deriving DecidableEq, Repr, Fintype, BEq def HachimojiState.toString : HachimojiState → String | .Φ => "Φ" | .Λ => "Λ" | .Ρ => "Ρ" | .Κ => "Κ" - | .Ω => "Ω" | .Σ => "Σ" | .Π => "Π" | .Ζ => "Ζ" + | .Ω => "Ω" | .«Σ» => "Σ" | .«Π» => "Π" | .Ζ => "Ζ" instance : ToString HachimojiState := ⟨HachimojiState.toString⟩ @@ -83,10 +87,10 @@ structure Receipt where finalState : HachimojiState ticCount : Nat fuelUsed : Nat - pathCost : Option Float + pathCost : Option Nat -- raw integer cost metric (Q16_16 raw value or 0); never Float libraryRefs : List String verified : Bool - deriving Repr, BEq + deriving DecidableEq, Repr, BEq -- Empty receipt (no classification performed) def Receipt.empty : Receipt := @@ -141,7 +145,7 @@ structure AVMState where fuel : Nat -- remaining fuel tic : Nat -- current TIC count history : List Instruction -- executed instructions - deriving Repr + deriving Repr, BEq def AVMState.initial (fuel : Nat) : AVMState := { stack := [], fuel := fuel, tic := 0, history := [] } @@ -212,17 +216,41 @@ lemma tic_monotone (T : Nat) (events : Nat) : ticUpdate T events ≥ T := by simp [ticUpdate] +-- δ never decreases TIC. When fuel > 0, it strictly increases TIC. +lemma δ_tic_monotone (s : AVMState) (i : Instruction) : + (δ s i).tic ≥ s.tic := by + simp [δ] + split_ifs with h_fuel + · -- fuel = 0: δ appends Halt and changes nothing else + simp + · -- fuel > 0: δ decrements fuel, increments tic, records instruction + cases i <;> simp + all_goals omega + +-- foldl preserves the TIC lower bound +lemma foldl_tic_monotone (s : AVMState) (program : List Instruction) : + (List.foldl δ s program).tic ≥ s.tic := by + induction program generalizing s with + | nil => simp + | cons i rest ih => + simp [List.foldl] + have h_step : (δ s i).tic ≥ s.tic := δ_tic_monotone s i + have h_rest : (List.foldl δ (δ s i) rest).tic ≥ (δ s i).tic := ih (δ s i) + exact Nat.le_trans h_step h_rest + -- The TIC axiom: TIC never decreases theorem tic_never_decreases (program : List Instruction) (fuel : Nat) : (runAVM program fuel).tic ≥ (AVMState.initial fuel).tic := by - simp [runAVM, AVMState.initial] - -- TIC starts at 0 and only increases - induction program with + simp [runAVM] + -- Invariant: foldl preserves tic ≥ starting tic + generalize AVMState.initial fuel = s + induction program generalizing s with | nil => simp | cons i rest ih => simp [List.foldl] - -- Each instruction increments TIC by at least 1 - sorry -- Proof: δ always increments tic by at least 1 + have h_step : (δ s i).tic ≥ s.tic := δ_tic_monotone s i + have h_rest : (List.foldl δ (δ s i) rest).tic ≥ (δ s i).tic := ih (δ s i) + exact Nat.le_trans h_step h_rest -- ============================================================================= -- §5. LOOP INVARIANT (computation generates time) @@ -237,13 +265,61 @@ theorem tic_never_decreases (program : List Instruction) (fuel : Nat) : (where time is measured in events, not seconds). -/ +-- If the final TIC equals the starting TIC, the stack never changed. +lemma foldl_tic_eq_start (s : AVMState) (program : List Instruction) + (h : (List.foldl δ s program).tic = s.tic) : + (List.foldl δ s program).stack = s.stack := by + induction program generalizing s with + | nil => + simp at h ⊢ + | cons i rest ih => + simp [List.foldl] at h ⊢ + have h_step : (δ s i).tic ≥ s.tic := δ_tic_monotone s i + have h_rest : (List.foldl δ (δ s i) rest).tic ≥ (δ s i).tic := + foldl_tic_monotone (δ s i) rest + have h_eq : (δ s i).tic = s.tic := by linarith + have h_fuel0 : s.fuel = 0 := by + by_contra h_fuel + have hf : s.fuel > 0 := by omega + have h_ne : s.fuel ≠ 0 := by omega + have h_strict : (δ s i).tic > s.tic := by + simp [δ, h_ne] + cases i <;> simp + linarith + have h_stack : (δ s i).stack = s.stack := by simp [δ, h_fuel0] + have h_fuel : (δ s i).fuel = s.fuel := by simp [δ, h_fuel0] + have h_tic : (δ s i).tic = s.tic := h_eq + have h_final_eq : (List.foldl δ (δ s i) rest).tic = (δ s i).tic := by linarith + have h_final_stack : (List.foldl δ (δ s i) rest).stack = (δ s i).stack := + ih (δ s i) h_final_eq + rw [h_stack] at h_final_stack + exact h_final_stack + +-- Corollary: if the starting TIC is 0 and the final TIC is 0, the stack is empty. +lemma runAVM_tic_zero_stack_empty (program : List Instruction) (fuel : Nat) + (h : (runAVM program fuel).tic = 0) : + (runAVM program fuel).stack = [] := by + simp [runAVM] at h ⊢ + have h_eq : (List.foldl δ (AVMState.initial fuel) program).tic = (AVMState.initial fuel).tic := by + simp [AVMState.initial] at h ⊢ + linarith + have h_stack : (List.foldl δ (AVMState.initial fuel) program).stack = (AVMState.initial fuel).stack := + foldl_tic_eq_start (AVMState.initial fuel) program h_eq + rw [h_stack] + simp [AVMState.initial] + theorem computation_generates_time (program : List Instruction) (fuel : Nat) (h_nonzero : (runAVM program fuel).result ≠ .Ζ) - (h_terminates : (runAVM program fuel).fuel > 0 ∨ program.length > 0) : + (_h_terminates : (runAVM program fuel).fuel > 0 ∨ program.length > 0) : (runAVM program fuel).tic > 0 := by - -- If the program produced a meaningful result, it must have executed - -- at least one instruction, which increments TIC by at least 1. - sorry -- Proof: δ increments tic on every instruction execution + -- Contrapositive: if final TIC is 0, the stack stayed empty, so result = Ζ. + by_contra h + have h_tic : (runAVM program fuel).tic = 0 := by omega + have h_stack : (runAVM program fuel).stack = [] := + runAVM_tic_zero_stack_empty program fuel h_tic + have h_result : (runAVM program fuel).result = .Ζ := by + simp [AVMState.result, h_stack] + contradiction -- ============================================================================= -- §6. LIBRARY INTERFACE diff --git a/PORTING_MAP.md b/PORTING_MAP.md index 7620e471..5f2fdc36 100644 --- a/PORTING_MAP.md +++ b/PORTING_MAP.md @@ -74,7 +74,7 @@ The source tree is large (~9,600 objects, ~1,300 Lean files). Most of it is expl | Research-Stack | SilverSight Target | Status | Notes | |----------------|-------------------|--------|-------| -| `Semantics.FixedPoint.lean` | `Core/SilverSightCore.lean` / `formal/CoreFormalism/Q16_16_Spec.lean` | 🟡 PORT | The full FixedPoint module with Q0_16/Q16_16 inverse trig, clamping, and determinism theorems should replace the current thin spec. | +| `Semantics.FixedPoint.lean` | `formal/CoreFormalism/FixedPoint.lean` | ✅ PORTED | Full FixedPoint module with Q0_16/Q16_16 inverse trig, clamping, and determinism theorems. Replaced the thin `Q16_16_Spec.lean`. | | `Semantics.SidonSets.lean` | `Core/` or `SearchLib/` | 🟡 PORT | Proven Sidon set construction, Singer theorem, Bertrand residue injectivity. Core to addressing. | | `Semantics.InteractionGraphSidon.lean` | `SearchLib/` | 🟡 PORT | RRC weak-axis reconstruction via CRT; part of search/addressing. | | `Semantics.SieveLemmas.lean` | `SearchLib/` or `Core/` | 🟡 PORT | Coprime-sieve reconstruction, CRT recovery theorem, executable witnesses. | @@ -218,7 +218,7 @@ Things SilverSight's architecture calls for but Research-Stack does not cleanly | Conflict | Resolution | |----------|------------| -| Research-Stack `Q16_16.lean` vs SilverSight `Q16_16_Spec.lean` | SilverSight spec is thin. Replace with Research-Stack `FixedPoint.lean` (canonical, proven, includes Q0_16 + inverse trig). | +| Research-Stack `Q16_16.lean` / `FixedPoint.lean` vs SilverSight `Q16_16_Spec.lean` | ✅ PORTED — `Q16_16_Spec.lean` deleted; `formal/CoreFormalism/FixedPoint.lean` is now the canonical source of truth. | | Research-Stack `qaoa_adapter.py` (2,421 lines) vs SilverSight split `qubo/*.py` | Split adapter: Finsler/QUBO builder → MetricLib/QUBOLib; circuit generation → QUBOLib; bitstring bridge → PVGSLib. | | Research-Stack `AGENTS.md` references many dead paths | Port rules, not state. Update path references to SilverSight equivalents. | | SilverSight `ARCHITECTURE.md` uses 6 layers; conceptual map uses 5 | Reconcile: 5-layer conceptual map is authoritative; 6-layer doc is an older draft. Update `ARCHITECTURE.md` to match 5-layer model + library method. | @@ -227,7 +227,7 @@ Things SilverSight's architecture calls for but Research-Stack does not cleanly ## 6. Recommended Porting Order -1. **Core first** — Replace `Q16_16_Spec.lean` with full `FixedPoint.lean`. Lock down `SilverSightCore.lean`. +1. **Core first** — ✅ Replace `Q16_16_Spec.lean` with full `FixedPoint.lean`. Lock down `SilverSightCore.lean`. `SilverSightCore.lean` now builds with no sorries and no `Float`. 2. **SearchLib** — Port `SidonSets.lean`, `SieveLemmas.lean`, `InteractionGraphSidon.lean`. 3. **RRCLib** — Extract RRC gates from `PVGS_DQ_Bridge_fixed.lean` §4 into standalone library. 4. **QUBOLib + MetricLib** — Split `qaoa_adapter.py` and `qubo_highs.py` cleanly. diff --git a/README.md b/README.md index aa72cb46..991c0862 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,7 @@ A deterministic equation search and classification system built on chaos game th | Directory | Contents | |-----------|----------| -| `formal/CoreFormalism/` | Lean 4: ChentsovFinite, HachimojiBase, HachimojiCodec, HachimojiManifoldAxiom, Q16_16_Spec | +| `formal/CoreFormalism/` | Lean 4: FixedPoint (canonical Q16_16/Q0_16), ChentsovFinite, HachimojiBase, HachimojiCodec, HachimojiManifoldAxiom | | `formal/PVGS_DQ_Bridge/` | Lean 4: Photon-Varied Gaussian State to Dual Quaternion energy bridge (7 sections + master) | | `formal/UniversalEncoding/` | Lean 4: 50-token math address space, 4D chirality classification | | `formal/BindingSite/` | Lean 4: Amino acid vocabulary mapping, entropy-based bindability | diff --git a/REBASE_RULES.md b/REBASE_RULES.md index 4dcc4486..2c7b4115 100644 --- a/REBASE_RULES.md +++ b/REBASE_RULES.md @@ -1,11 +1,17 @@ -# REBASE RULES — Research Stack Agent / Rules Manifest +# REBASE RULES — SilverSight Agent / Rules Manifest **Purpose:** This file is a rebase seed. When starting a fresh project map, copy only -the files and rules listed here. Do not migrate runtime state, stale audits, or -completed assignment boards. +the files and rules listed here. Do not migrate runtime state, stale audits, +completed assignment boards, or legacy deployment hacks. **Principle:** *Port the contracts and the rituals, not the state.* +**Status:** Research Stack contained many legacy hacks (Hermes ports, Headroom +proxy endpoints, old benchmark tables, repo-specific paths). Those have been +stripped. The core conceptual bindings — Lean authority, no-Float compute, +receipt boundaries, programming-choice flow, and the post-interaction ritual — +are preserved here and in `AGENTS.md`. + --- ## 1. Core Operating Contracts (MUST PORT) @@ -15,35 +21,35 @@ They are actively maintained and cross-referenced throughout the stack. | File | Scope | |------|-------| -| `AGENTS.md` (root) | Master operating contract: post-interaction workflow, programming-choice flow, Q16_16 doctrine, Git hygiene, Do-Not-Sweep rules, glossary, claim boundaries. | -| `0-Core-Formalism/lean/Semantics/AGENTS.md` | Lean/Semantics local contract: blessed Compiler surface, build baselines, quarantine boundaries, proof-tactic lessons, current solidification anchors. | -| `4-Infrastructure/AGENTS.md` | Infrastructure and shim contract: storage stack, hardware-witness boundaries, ENE schema, compute dispatch pattern. | -| `6-Documentation/docs/AGENTS.md` | Strict LLM operating rules: anti-drift evidence standards, `bind` primitive, naming conventions, sigma levels, SI units, deletion criteria, PQC policy. | -| `5-Applications/text-to-cad/AGENTS.md` | CAD harness contract: generated CAD/URDF source-of-truth, viewer handoff, repo policies. | -| `scripts/qc-flag/AGENTS.md` | Lean QC protocol: 7-check inspection protocol. | -| `shared-data/artifacts/lean_expert_agent/AGENTS.md` | Lean expert agent `/inspect` protocol and output format. | -| `.github/RRC_OPERATING_CONTRACT.md` | Rainbow Raccoon Compiler gate definition: ACCEPT / HOLD / QUARANTINE. | +| `AGENTS.md` (this repo) | **SilverSight master operating contract.** Distilled from Research Stack; strips legacy deployment details and adapts rules to the library-method architecture. | +| `0-Core-Formalism/lean/Semantics/AGENTS.md` | Lean/Semantics local contract: blessed Compiler surface, build baselines, quarantine boundaries, proof-tactic lessons, current solidification anchors. **ADAPT** to `formal/AGENTS.md` in SilverSight. | +| `4-Infrastructure/AGENTS.md` | Infrastructure and shim contract: storage stack, hardware-witness boundaries, ENE schema, compute dispatch pattern. **PORT ONLY IF** infrastructure work continues; otherwise drop. | +| `6-Documentation/docs/AGENTS.md` | Strict LLM operating rules: anti-drift evidence standards, `bind` primitive, naming conventions, sigma levels, SI units, deletion criteria, PQC policy. **ADAPT** to `docs/AGENTS.md` if strict doc rules are needed. | +| `5-Applications/text-to-cad/AGENTS.md` | CAD harness contract: generated CAD/URDF source-of-truth, viewer handoff, repo policies. **PORT ONLY IF** CAD work continues. | +| `scripts/qc-flag/AGENTS.md` | Lean QC protocol: 7-check inspection protocol. **ADAPT** to `tests/qc-flag/AGENTS.md` if the protocol is adopted. | +| `shared-data/artifacts/lean_expert_agent/AGENTS.md` | Lean expert agent `/inspect` protocol and output format. **ADAPT** if a formal reviewer agent is wired up. | +| `.github/RRC_OPERATING_CONTRACT.md` | Rainbow Raccoon Compiler gate definition: ACCEPT / HOLD / QUARANTINE. **ADAPT** to SilverSight's receipt gate if RRC work continues. | ### Non-negotiable rules extracted from the contracts -1. **Lean is the source of truth.** Python, Rust, and Verilog are extraction targets only. +1. **Lean is the source of truth.** Python and Verilog are extraction targets only. 2. **Programming choice flow** — before writing new logic, check this decision tree in order: - Admissibility / routing / alignment / gating decision? → **Lean only.** - - Emitting a top-level receipt or JSON bundle? → **`Semantics.AVMIsa.Emit` only.** - - Classifying rows / computing alignment scores? → **Lean (`Semantics.RRC.*`).** - - Supplying raw input features (equation text, IDs, weak_axes)? → **Python shim OK,** no admissibility logic, regenerable from source. + - Minting/stamping a top-level receipt or JSON bundle? → **Lean stamps; Python formats/stores only.** + - Classifying rows / computing alignment scores? → **Lean (`formal/CoreFormalism/` or a new `formal/*.lean` module).** + - Supplying raw input features (expression text, IDs, weak_axes)? → **Python shim OK,** no admissibility logic, regenerable from source. - Float arithmetic in a compute path? → **STOP.** Use `Q16_16.ofNat`, `Q16_16.ofRatio`, or `Q16_16.ofRawInt`. - Advancing promotion status in shim space? → **STOP.** `not_promoted` until a Lean gate passes. - - Pure I/O (read/write JSON, subprocess, format output)? → **Python shim OK.** Receipt output routes through `AVMIsa.Emit`. -3. **No `Float` in compute paths.** `ofFloat` is permitted only at JSON/sensor boundaries and must be immediately bracketed. + - Pure I/O (read/write JSON, subprocess, format output)? → **Python shim OK.** Receipt output is stamped in Lean and stored by Python. +3. **No `Float` in Lean compute paths.** `ofFloat` is permitted only at JSON/sensor boundaries and must be immediately bracketed. `Float` is forbidden in `Core/` entirely. 4. **Post-interaction workflow** (mandatory after any code/receipt/architecture change): - Update the nearest scoped `AGENTS.md` for every touched subtree. - - Run `lake build Compiler` (and full `lake build` if Lean files touched). + - Run the narrow Lean target first, then full `lake build` if Lean files touched. - Commit with an explicit file list; **never** `git add .`. - Run `git status --branch --short --untracked-files=all`. 5. **Do Not Sweep:** never run `git add .`, `git checkout -- .`, or `git clean -fdx`. 6. **Secrets are runtime-only:** use environment variables (`OLLAMA_API_KEY`, `DEEPSEEK_API_KEY`, etc.); never commit literal keys. -7. **Legacy recovery is explicit:** use `RECOVER LEGACY INFORMATION: ` only. Current cornfield ref: `backup/distilled-with-vcd-history-2026-05-11`. +7. **Legacy recovery is explicit:** use `RECOVER LEGACY INFORMATION: ` only. Cross-repo cornfield ref: `backup/distilled-with-vcd-history-2026-05-11`. --- @@ -157,12 +163,15 @@ Use this when standing up the new project map. When designing the new project layout, preserve these boundary rules: - **Lean owns decisions; Python owns I/O.** -- **`Semantics.AVMIsa.Emit` is the sole top-level receipt boundary.** -- **`shared-data/` is ignored by default.** Promote only durable receipts with `git add -f -- `. -- **Research artifacts go outside the git tree** (e.g. `/home/researcher/research/` in the container model). +- **`Core/SilverSightCore.lean` is the root authority and imports nothing.** +- **The `Receipt` is the sole Core/library boundary.** Lean stamps; libraries format/store. +- **`python/` and `qubo/` are I/O and optimization shims only.** No admissibility logic in shim space. +- **Research artifacts go outside the git tree** unless promoted as durable receipts. - **Every new compression path needs two Lean theorems:** `eigensolid_convergence` and `receipt_invertible`. +- **No library imports another library.** Libraries import `Core/` only. --- -*Generated from active Research Stack agent rules and contracts.* +*Generated from active Research Stack agent rules and contracts, stripped of legacy hacks.* *Principle: port contracts and rituals, not state.* +*SilverSight master contract: `AGENTS.md`.* diff --git a/formal/CoreFormalism/FixedPoint.lean b/formal/CoreFormalism/FixedPoint.lean new file mode 100644 index 00000000..6655f43c --- /dev/null +++ b/formal/CoreFormalism/FixedPoint.lean @@ -0,0 +1,1311 @@ +import Lean.Data.Json +import Mathlib.Data.UInt +import Mathlib.Tactic +import Mathlib.Data.Int.Basic +import Mathlib.Data.Nat.Basic + +set_option maxRecDepth 20000 +set_option linter.unusedSimpArgs false + +namespace SilverSight.FixedPoint + +open Lean + +/-! +A proof-friendly fixed-point core. + +Design rule: +* The semantic value is a bounded signed raw integer. +* Saturation is performed by `ofRawInt`. +* UInt bit-patterns are boundary/hardware artifacts, not the proof model. + +This removes the old proof debt caused by proving signed arithmetic facts directly +against modular UInt32/UInt64 overflow behavior. +-/ + +-- ═══════════════════════════════════════════════════════════════════════════ +-- Q0.16 signed normalized fraction +-- ═══════════════════════════════════════════════════════════════════════════ + +def q0_16MinRaw : Int := -32768 +def q0_16MaxRaw : Int := 32767 +def q0_16Scale : Int := 32767 + +/-- +Q0.16 pure fraction representation. +The canonical proof model stores the signed raw integer in [-32768, 32767]. +Use boundary conversion functions when a UInt16 bit pattern is required. +-/ +abbrev Q0_16 := { x : Int // q0_16MinRaw ≤ x ∧ x ≤ q0_16MaxRaw } + +instance : Repr Q0_16 where + reprPrec q _ := repr q.val + +instance : BEq Q0_16 where + beq a b := a.val == b.val + +instance : Inhabited Q0_16 where + default := ⟨0, by constructor <;> norm_num [q0_16MinRaw, q0_16MaxRaw]⟩ + +instance : ToJson Q0_16 where + toJson q := Json.mkObj [("val", toJson q.val)] + +namespace Q0_16 + +@[ext] +theorem ext {a b : Q0_16} (h : a.val = b.val) : a = b := Subtype.ext h + +@[inline] +def toInt (q : Q0_16) : Int := q.val + +@[inline] +def ofRawInt (raw : Int) : Q0_16 := + if hhi : raw > q0_16MaxRaw then + ⟨q0_16MaxRaw, by constructor <;> norm_num [q0_16MinRaw, q0_16MaxRaw]⟩ + else if hlo : raw < q0_16MinRaw then + ⟨q0_16MinRaw, by constructor <;> norm_num [q0_16MinRaw, q0_16MaxRaw]⟩ + else + ⟨raw, by + constructor + · dsimp [q0_16MinRaw, q0_16MaxRaw] at *; omega + · dsimp [q0_16MinRaw, q0_16MaxRaw] at *; omega⟩ + +instance : FromJson Q0_16 where + fromJson? j := do + let raw : Int ← fromJson? (← j.getObjVal? "val") + pure (ofRawInt raw) + +def zero : Q0_16 := ofRawInt 0 +def one : Q0_16 := ofRawInt q0_16MaxRaw +def half : Q0_16 := ofRawInt 16383 + +def neg (x : Q0_16) : Q0_16 := ofRawInt (-x.toInt) +def add (a b : Q0_16) : Q0_16 := ofRawInt (a.toInt + b.toInt) +def sub (a b : Q0_16) : Q0_16 := ofRawInt (a.toInt - b.toInt) +def mul (a b : Q0_16) : Q0_16 := ofRawInt ((a.toInt * b.toInt) / q0_16Scale) +def div (a b : Q0_16) : Q0_16 := + if b.toInt = 0 then zero else ofRawInt ((a.toInt * q0_16Scale) / b.toInt) +def abs (x : Q0_16) : Q0_16 := if x.toInt < 0 then neg x else x + +instance : Add Q0_16 where add := add +instance : Sub Q0_16 where sub := sub +instance : Mul Q0_16 where mul := mul +instance : Div Q0_16 where div := div +instance : Neg Q0_16 where neg := neg + +def lt (a b : Q0_16) : Bool := a.toInt < b.toInt +def le (a b : Q0_16) : Bool := a.toInt ≤ b.toInt +def gt (a b : Q0_16) : Bool := b.toInt < a.toInt +def ge (a b : Q0_16) : Bool := b.toInt ≤ a.toInt + +def toFloat (q : Q0_16) : Float := + Float.ofInt q.toInt / 32767.0 + +def ofFloat (f : Float) : Q0_16 := + if f.isNaN then zero + else if f ≥ 1.0 then one + else if f ≤ -1.0 then neg one + else if f < 0.0 then + ofRawInt (-(Int.ofNat ((-f * 32767.0).round.toUInt16.toNat))) + else + ofRawInt (Int.ofNat ((f * 32767.0).round.toUInt16.toNat)) + +def log2 (q : Q0_16) : Q0_16 := + if q.toInt = 0 then zero + else + let f := toFloat q + if f ≤ 0.0 then zero else ofFloat (Float.log2 f) + +def min (a b : Q0_16) : Q0_16 := + if a.toInt ≤ b.toInt then a else b + +end Q0_16 + +-- ═══════════════════════════════════════════════════════════════════════════ +-- Q16.16 signed fixed-point +-- ═══════════════════════════════════════════════════════════════════════════ + +def q16MinRaw : Int := -2147483648 +def q16MaxRaw : Int := 2147483647 +def q16Scale : Int := 65536 + +/-- Saturating clamp of a raw integer into [q16MinRaw, q16MaxRaw]. + This is the pure-Int kernel of `Q16_16.ofRawInt`; all monotonicity + reasoning is proved once here and reused by higher lemmas. -/ +def q16Clamp (i : Int) : Int := + if i > q16MaxRaw then q16MaxRaw + else if i < q16MinRaw then q16MinRaw + else i + +/-- `q16Clamp` is monotone: a ≤ b → q16Clamp a ≤ q16Clamp b. -/ +theorem q16Clamp_monotone (a b : Int) (h : a ≤ b) : q16Clamp a ≤ q16Clamp b := by + unfold q16Clamp + by_cases ha_hi : a > q16MaxRaw + · by_cases hb_hi : b > q16MaxRaw + · simp [ha_hi, hb_hi] + · by_cases hb_lo : b < q16MinRaw + · simp [ha_hi, hb_hi, hb_lo]; dsimp [q16MinRaw, q16MaxRaw] at *; omega + · simp [ha_hi, hb_hi, hb_lo]; dsimp [q16MaxRaw] at *; omega + · by_cases ha_lo : a < q16MinRaw + · by_cases hb_hi : b > q16MaxRaw + · simp [ha_hi, ha_lo, hb_hi]; dsimp [q16MinRaw, q16MaxRaw] at *; omega + · by_cases hb_lo : b < q16MinRaw + · simp [ha_hi, ha_lo, hb_hi, hb_lo] + · simp [ha_hi, ha_lo, hb_hi, hb_lo]; dsimp [q16MinRaw] at *; omega + · by_cases hb_hi : b > q16MaxRaw + · simp [ha_hi, ha_lo, hb_hi]; dsimp [q16MaxRaw] at *; omega + · by_cases hb_lo : b < q16MinRaw + · simp [ha_hi, ha_lo, hb_hi, hb_lo]; dsimp [q16MinRaw] at *; omega + · simp [ha_hi, ha_lo, hb_hi, hb_lo]; exact h + +/-- `q16Clamp` is idempotent on in-range values. -/ +theorem q16Clamp_id_of_inRange (i : Int) (hlo : q16MinRaw ≤ i) (hhi : i ≤ q16MaxRaw) : + q16Clamp i = i := by + unfold q16Clamp + simp [show ¬ i > q16MaxRaw from by omega, show ¬ i < q16MinRaw from by omega] + +lemma q16Clamp_lower (x : Int) : q16MinRaw ≤ q16Clamp x := by + unfold q16Clamp q16MinRaw q16MaxRaw; split_ifs <;> omega + +lemma q16Clamp_upper (x : Int) : q16Clamp x ≤ q16MaxRaw := by + unfold q16Clamp q16MinRaw q16MaxRaw; split_ifs <;> omega + +lemma q16Clamp_nonneg_of_nonneg {x : Int} (hx : 0 ≤ x) : 0 ≤ q16Clamp x := by + unfold q16Clamp q16MinRaw q16MaxRaw + split_ifs <;> omega + +lemma q16Clamp_idem (x : Int) : q16Clamp (q16Clamp x) = q16Clamp x := by + have h_upper := q16Clamp_upper x + have h_lower := q16Clamp_lower x + unfold q16Clamp q16MinRaw q16MaxRaw + split_ifs <;> omega + +/-- `q16Clamp` is 1-Lipschitz (non-expansive): clamped distance ≤ raw distance. -/ +lemma q16Clamp_lipschitz (A B : Int) : |q16Clamp A - q16Clamp B| ≤ |A - B| := by + by_cases h : A ≤ B + · have hAB : A - B ≤ 0 := by omega + have h_clamp : q16Clamp A - q16Clamp B ≤ 0 := by + have h_mono : q16Clamp A ≤ q16Clamp B := q16Clamp_monotone A B h + omega + rw [abs_of_nonpos hAB, abs_of_nonpos h_clamp] + unfold q16Clamp + split <;> split <;> omega + · have hBA : B ≤ A := by omega + have hAB_pos : 0 ≤ A - B := by omega + have h_clamp_pos : 0 ≤ q16Clamp A - q16Clamp B := by + have h_mono : q16Clamp A ≥ q16Clamp B := q16Clamp_monotone B A hBA + omega + rw [abs_of_nonneg hAB_pos, abs_of_nonneg h_clamp_pos] + unfold q16Clamp + split <;> split <;> omega + +/-- +Q16.16 fixed-point representation. +The canonical proof model stores the signed raw integer in +[-2147483648, 2147483647]. + +Hardware/serialization UInt32 bit patterns should enter through `ofBits` and +leave through `toBits`. All semantic proofs use `toInt`. +-/ +abbrev Q16_16 := { x : Int // q16MinRaw ≤ x ∧ x ≤ q16MaxRaw } + +instance : Repr Q16_16 where + reprPrec q _ := repr q.val + +instance : BEq Q16_16 where + beq a b := a.val == b.val + +instance : Inhabited Q16_16 where + default := ⟨0, by constructor <;> norm_num [q16MinRaw, q16MaxRaw]⟩ + +instance : ToJson Q16_16 where + toJson q := Json.mkObj [("val", toJson q.val)] + +namespace Q16_16 + +@[ext] +theorem ext {a b : Q16_16} (h : a.val = b.val) : a = b := Subtype.ext h + +@[inline] +def toInt (q : Q16_16) : Int := q.val + +@[inline] +def ofRawInt (raw : Int) : Q16_16 := + if hhi : raw > q16MaxRaw then + ⟨q16MaxRaw, by constructor <;> norm_num [q16MinRaw, q16MaxRaw]⟩ + else if hlo : raw < q16MinRaw then + ⟨q16MinRaw, by constructor <;> norm_num [q16MinRaw, q16MaxRaw]⟩ + else + ⟨raw, by + constructor + · dsimp [q16MinRaw, q16MaxRaw] at *; omega + · dsimp [q16MinRaw, q16MaxRaw] at *; omega⟩ + +instance : FromJson Q16_16 where + fromJson? j := do + let raw : Int ← fromJson? (← j.getObjVal? "val") + pure (ofRawInt raw) + +/-- Decode a UInt32 two's-complement hardware bit pattern into the signed model. -/ +@[inline] +def ofBits (u : UInt32) : Q16_16 := + let n := u.toNat + if n ≥ 2147483648 then ofRawInt ((n : Int) - 4294967296) + else ofRawInt (n : Int) + +/-- Encode the signed model as a UInt32 two's-complement hardware bit pattern. -/ +@[inline] +def toBits (q : Q16_16) : UInt32 := UInt32.ofInt q.toInt + +def zero : Q16_16 := ⟨0, by constructor <;> norm_num [q16MinRaw, q16MaxRaw]⟩ +def one : Q16_16 := ⟨q16Scale, by constructor <;> norm_num [q16MinRaw, q16MaxRaw, q16Scale]⟩ +def negOne : Q16_16 := ⟨-q16Scale, by constructor <;> norm_num [q16MinRaw, q16MaxRaw, q16Scale]⟩ +def epsilon : Q16_16 := ⟨1, by constructor <;> norm_num [q16MinRaw, q16MaxRaw]⟩ +def two : Q16_16 := ⟨2 * q16Scale, by constructor <;> norm_num [q16MinRaw, q16MaxRaw, q16Scale]⟩ +def maxVal : Q16_16 := ⟨q16MaxRaw, by constructor <;> norm_num [q16MinRaw, q16MaxRaw]⟩ +def minVal : Q16_16 := ⟨q16MinRaw, by constructor <;> norm_num [q16MinRaw, q16MaxRaw]⟩ + +/-- Saturating infinity/illegal sentinel. If you need the old 0xFFFFFFFF bit +sentinel, use `ofRawInt (-1)` or `ofBits 0xFFFFFFFF` explicitly. -/ +def infinity : Q16_16 := maxVal + +def scale : Nat := 65536 + +def ofNat (n : Nat) : Q16_16 := ofRawInt ((n : Int) * q16Scale) + +def satFromNat (n : Nat) : Q16_16 := ofRawInt ((n : Int) * q16Scale) + +def ofRatio (num : Nat) (den : Nat) : Q16_16 := + if den = 0 then zero + else ofRawInt (Int.ofNat (num * scale / den)) + +instance : OfNat Q16_16 n where + ofNat := ofNat n + +@[inline] +def ofInt (n : Int) : Q16_16 := ofRawInt (n * q16Scale) + +/-- Saturating addition. -/ +@[inline] +def add (a b : Q16_16) : Q16_16 := ofRawInt (a.toInt + b.toInt) + +/-- Saturating subtraction. -/ +@[inline] +def sub (a b : Q16_16) : Q16_16 := ofRawInt (a.toInt - b.toInt) + +/-- Saturating Q16.16 multiplication: raw result is `(a*b)/65536`. -/ +@[inline] +def mul (a b : Q16_16) : Q16_16 := ofRawInt ((a.toInt * b.toInt) / q16Scale) + +/-- Saturating Q16.16 division: raw result is `(a*65536)/b`. -/ +@[inline] +def div (a b : Q16_16) : Q16_16 := + if b.toInt = 0 then infinity else ofRawInt ((a.toInt * q16Scale) / b.toInt) + +@[inline] +def neg (q : Q16_16) : Q16_16 := ofRawInt (-q.toInt) + +@[inline] +def abs (q : Q16_16) : Q16_16 := if q.toInt < 0 then neg q else q + +@[inline] +def ofFloat (f : Float) : Q16_16 := + if f.isNaN || f ≥ 32768.0 then infinity + else if f ≤ -32768.0 then minVal + else if f < 0.0 then + ofRawInt (-(Int.ofNat ((-f * 65536.0).floor.toUInt32.toNat))) + else + ofRawInt (Int.ofNat ((f * 65536.0).floor.toUInt32.toNat)) + +/-- Integer square root via Newton's method. Returns floor(√n). + Terminates in at most 64 iterations (fuel-bounded). + Division-by-zero is impossible: `x ≥ 1` is a loop invariant + because the initial value `n/2+1 ≥ 1` and every refinement `x'` + is the average of positive integers. -/ +private def intSqrt (n : Int) : Int := + if n ≤ 0 then 0 + else + let rec loop (x : Int) (fuel : Nat) : Int := + match fuel with + | 0 => x + | f + 1 => + let x' := (x + n / x) / 2 + if x' ≥ x then x else loop x' f + loop (n / 2 + 1) 64 + +/-- Q16.16 square root via integer Newton's method. + Computes floor(√(q.raw × 65536)) which is the Q16.16 + representation of √(q.raw/65536). -/ +@[inline] +def sqrt (q : Q16_16) : Q16_16 := + if q.toInt ≤ 0 then zero + else ofRawInt (intSqrt (q.toInt * q16Scale)) + +@[inline] +def toFloat (q : Q16_16) : Float := + Float.ofInt q.toInt / 65536.0 + +/-- Natural logarithm approximation around 1.0. -/ +def ln (q : Q16_16) : Q16_16 := + let x := q.toInt + if x ≤ 0 then zero + else + let y := x - q16Scale + let y2 := (y * y) / q16Scale + let y3 := (y * y2) / q16Scale + ofRawInt (y - y2 / 2 + y3 / 3) + +def log2 (q : Q16_16) : Q16_16 := + let ln2 : Q16_16 := ofRawInt 45426 + div (ln q) ln2 + +def expNeg (x : Q16_16) : Q16_16 := + if x.toInt ≥ 0x00030000 then zero + else if x.toInt ≥ 0x00020000 then ofRawInt 0x00004D29 + else if x.toInt ≥ 0x00010000 then ofRawInt 0x0000C5C0 + else ofRawInt 0x0001C5C0 + +/-- Q16.16 exponential via Taylor series eˣ ≈ Σ xⁿ/n! (n=0..6). + Valid for |x| ≤ 1. For larger x, range-reduce via eˣ = (e^(x/2))² + (repeated squaring). Achieves ~Q16.16 precision. -/ +def exp (x : Q16_16) : Q16_16 := + if x.toInt ≤ -q16Scale then zero + else if x.toInt ≥ 4 * q16Scale then maxVal + else + -- Range-reduce: x = k*ln(2) + r, |r| < ln(2), then eˣ = 2ᵏ * eʳ + let ln2Raw := 45426 -- Q16.16 representation of ln(2) ≈ 0.693147 + let k := x.toInt / ln2Raw + let r := x.toInt - k * ln2Raw + -- Taylor for eʳ through r⁶/720 (|r| < 0.693, error < 2e-6) + let r2 := (r * r) / q16Scale + let r3 := (r * r2) / q16Scale + let r4 := (r2 * r2) / q16Scale + let r5 := (r2 * r3) / q16Scale + let r6 := (r3 * r3) / q16Scale + let taylor := q16Scale + r + r2 / 2 + r3 / 6 + r4 / 24 + r5 / 120 + r6 / 720 + -- Scale by 2ᵏ (left-shift by k, saturate) + let shifted := if k ≥ 15 then q16MaxRaw else if k ≤ -15 then 0 + else if k ≥ 0 then taylor <<< k.toNat + else taylor >>> (-k).toNat + ofRawInt (if shifted > q16MaxRaw then q16MaxRaw else if shifted < q16MinRaw then q16MinRaw else shifted) + +/-- Q16.16 sine via 7th-order Taylor: sin(x) ≈ x - x³/6 + x⁵/120 - x⁷/5040. + Range-reduced to [0, π/2] using symmetry. -/ +def sin (x : Q16_16) : Q16_16 := + -- Map [−π, π] → [0, π], then reflect + let piRaw := 205887 -- Q16.16 π ≈ 3.14159 + let twoPiRaw := 411774 + -- Normalize to [0, 2π) + let raw := x.toInt % twoPiRaw + let raw' := if raw < 0 then raw + twoPiRaw else raw + -- Quadrant: 0 = [0,π/2), 1 = [π/2,π), 2 = [π,3π/2), 3 = [3π/2,2π) + let halfPi := piRaw / 2 + let q := if raw' < halfPi then 0 + else if raw' < piRaw then 1 + else if raw' < piRaw + halfPi then 2 + else 3 + -- Reduce to [0, π/2] + let reduced := + match q with + | 0 => raw' + | 1 => piRaw - raw' + | 2 => raw' - piRaw + | 3 => twoPiRaw - raw' + | _ => raw' -- unreachable + -- Taylor sin(t) ≈ t - t³/6 + t⁵/120 - t⁷/5040 (|t| ≤ π/2 ≈ 1.57) + let t := reduced + let t2 := (t * t) / q16Scale + let t3 := (t * t2) / q16Scale + let t5 := (t3 * t2) / q16Scale + let t7 := (t5 * t2) / q16Scale + let sinPos := t - t3 / 6 + t5 / 120 - t7 / 5040 + -- Sign by quadrant: quadrants 0,1 → positive; quadrants 2,3 → negative + if q < 2 then ofRawInt (max q16MinRaw (min q16MaxRaw sinPos)) + else ofRawInt (max q16MinRaw (min q16MaxRaw (-sinPos))) + +/-- Q16.16 power: base^e = exp(e * ln(base)). -/ +def pow (base e : Q16_16) : Q16_16 := + if base.toInt ≤ 0 then + if e.toInt = 0 then one else zero + else if e.toInt = 0 then one + else if e.toInt = q16Scale then base -- e = 1 + else exp (mul (ln base) e) + +/-- Natural logarithm — alias for `ln`. -/ +def log (x : Q16_16) : Q16_16 := ln x + +-- ═══════════════════════════════════════════════════════════════════════════ +-- Inverse Trigonometric Functions (integer-only, no Float) +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- Core arctangent for |x| ≤ 1 using minimax polynomial. + atan(x) ≈ x * (0.9998660 + x²*(-0.3302995 + x²*(0.1801410 + x²*(-0.0851330)))) + Max error < 2e-5 on [0,1]. -/ +private def atanCore (x : Q16_16) : Q16_16 := + let xRaw := x.toInt + -- x² in Q16.16 + let x2Raw := (xRaw * xRaw) / q16Scale + -- Horner's method with step-by-step scaling to avoid overflow: + -- p(x) = c0 + x²*(c1 + x²*(c2 + x²*c3)) + -- c0=65527, c1=-21642, c2=11804, c3=-5579 + let p3 : Int := -5579 + let p2 : Int := 11804 + (x2Raw * p3) / q16Scale + let p1 : Int := -21642 + (x2Raw * p2) / q16Scale + let p0 : Int := 65527 + (x2Raw * p1) / q16Scale + ofRawInt ((xRaw * p0) / q16Scale) + +/-- Q16.16 arctangent via minimax polynomial with range reduction. + For |x| ≤ 1: uses atanCore directly. + For |x| > 1: uses identity atan(x) = π/2 - atan(1/x). + For x < 0: uses identity atan(x) = -atan(-x). -/ +def atan (x : Q16_16) : Q16_16 := + if x.toInt = 0 then zero + else + let ax := abs x + let halfPiRaw := 102943 -- Q16.16 π/2 ≈ 1.5708 + -- Range-reduce: if |x| > 1, use atan(x) = π/2 - atan(1/x) + let result := + if ax.toInt ≤ q16Scale then + atanCore ax + else + -- 1/x in Q16.16: (q16Scale² / ax_raw) + let invX := ofRawInt ((q16Scale * q16Scale) / ax.toInt) + sub (ofRawInt halfPiRaw) (atanCore invX) + -- Sign: atan(-x) = -atan(x) + if x.toInt < 0 then neg result else result + +/-- Q16.16 arcsine via identity: asin(x) = atan(x / sqrt(1 - x²)). + Valid for |x| ≤ 1. For |x| > 1, clips to ±π/2. -/ +def asin (x : Q16_16) : Q16_16 := + let xRaw := x.toInt + if xRaw ≥ q16Scale then div (ofRawInt 205887) two -- π/2 + else if xRaw ≤ -q16Scale then neg (div (ofRawInt 205887) two) -- -π/2 + else if xRaw = 0 then zero + else + -- Compute x / sqrt(1 - x²) in Q16.16 + -- 1 - x² in Q16.16: q16Scale - (xRaw*xRaw)/q16Scale + let oneMinusX2 := q16Scale - (xRaw * xRaw) / q16Scale + if oneMinusX2 ≤ 0 then + -- Numerical underflow: |x| ≈ 1, return ±π/2 + if xRaw > 0 then div (ofRawInt 205887) two else neg (div (ofRawInt 205887) two) + else + let sqrtVal := sqrt (ofRawInt oneMinusX2) + if sqrtVal.toInt = 0 then + if xRaw > 0 then div (ofRawInt 205887) two else neg (div (ofRawInt 205887) two) + else + atan (div x sqrtVal) + +/-- Q16.16 arccosine via identity: acos(x) = π/2 - asin(x). + Valid for |x| ≤ 1. -/ +def acos (x : Q16_16) : Q16_16 := + sub (div (ofRawInt 205887) two) (asin x) + +/-- Q16.16 two-argument arctangent. + Computes the angle (radians) from the positive x-axis to the point (x, y). + Handles all four quadrants correctly. -/ +def atan2 (y x : Q16_16) : Q16_16 := + let piRaw : Q16_16 := ofRawInt 205887 + if x.toInt = 0 then + if y.toInt = 0 then zero -- undefined, return 0 + else if y.toInt > 0 then div piRaw two -- π/2 + else neg (div piRaw two) -- -π/2 + else if x.toInt > 0 then + atan (div y x) + else if y.toInt ≥ 0 then + add (atan (div y x)) piRaw -- quadrant II: atan(y/x) + π + else + sub (atan (div y x)) piRaw -- quadrant III: atan(y/x) - π + +instance : Add Q16_16 := ⟨add⟩ +instance : Sub Q16_16 := ⟨sub⟩ +instance : Mul Q16_16 := ⟨mul⟩ +instance : Div Q16_16 := ⟨div⟩ +instance : Neg Q16_16 := ⟨neg⟩ + +instance : LE Q16_16 where + le a b := a.toInt ≤ b.toInt + +instance : LT Q16_16 where + lt a b := a.toInt < b.toInt + +instance : DecidableRel (fun a b : Q16_16 => a ≤ b) := + fun a b => inferInstanceAs (Decidable (a.toInt ≤ b.toInt)) + +instance : DecidableRel (fun a b : Q16_16 => a < b) := + fun a b => inferInstanceAs (Decidable (a.toInt < b.toInt)) + +@[inline] +def ge (a b : Q16_16) : Bool := b.toInt ≤ a.toInt + +@[inline] +def gt (a b : Q16_16) : Bool := b.toInt < a.toInt + +def lt (a b : Q16_16) : Bool := a.toInt < b.toInt + +def le (a b : Q16_16) : Bool := a.toInt ≤ b.toInt + +def isNeg (q : Q16_16) : Bool := q.toInt < 0 + +def clip (x lo hi : Q16_16) : Q16_16 := + if x.toInt < lo.toInt then lo + else if x.toInt > hi.toInt then hi + else x + +def sat01 (q : Q16_16) : Q16_16 := + if q.toInt < 0 then zero + else if q.toInt > q16Scale then one + else q + +def max (a b : Q16_16) : Q16_16 := + if a.toInt ≥ b.toInt then a else b + +def min (a b : Q16_16) : Q16_16 := + if a.toInt ≤ b.toInt then a else b + +def recip (x : Q16_16) : Q16_16 := + let xInt := x.toInt + if xInt = 0 then maxVal + else + let numer : Int := 0x100000000 + let denom := if xInt < 0 then -xInt else xInt + let r := numer / denom + let y := ofRawInt r + if xInt < 0 then neg y else y + +def ofRaw (n : Nat) : Q16_16 := ofRawInt (n : Int) + +-- ═══════════════════════════════════════════════════════════════════════════ +-- Algebraic lemmas +-- ═══════════════════════════════════════════════════════════════════════════ + +@[simp] theorem zero_toInt : toInt zero = 0 := rfl +@[simp] theorem one_toInt : toInt one = 65536 := rfl +@[simp] theorem epsilon_toInt : toInt epsilon = 1 := rfl + +theorem epsilon_toInt_pos : toInt epsilon > 0 := by norm_num [epsilon_toInt] + +@[simp] +theorem maxVal_toInt : toInt maxVal = q16MaxRaw := rfl + +@[simp] +theorem minVal_toInt : toInt minVal = q16MinRaw := rfl + +@[simp] +private theorem ofRawInt_zero : ofRawInt 0 = zero := by + apply Subtype.ext + simp [ofRawInt, zero, toInt, q16MinRaw, q16MaxRaw] + +/-- Saturation lower-bound preservation. -/ +theorem ofRawInt_toInt_ge (i c : Int) + (hi : i ≥ c) (hcMin : q16MinRaw ≤ c) (hcMax : c ≤ q16MaxRaw) : + (ofRawInt i).toInt ≥ c := by + unfold ofRawInt toInt + by_cases hhi : i > q16MaxRaw + · simp [hhi] + dsimp [q16MaxRaw] at * + omega + · by_cases hlo : i < q16MinRaw + · dsimp [q16MinRaw, q16MaxRaw] at * + omega + · simp [hhi, hlo] + exact hi + +/-- Saturation preserves non-negativity for non-negative raw values. -/ +theorem ofRawInt_toInt_nonneg (i : Int) (hi : i ≥ 0) : + (ofRawInt i).toInt ≥ 0 := by + exact ofRawInt_toInt_ge i 0 hi (by norm_num [q16MinRaw]) (by norm_num [q16MaxRaw]) + +/-- Bounded raw reconstruction. -/ +theorem ofRawInt_toInt (a : Q16_16) : ofRawInt a.toInt = a := by + apply Subtype.ext + unfold ofRawInt toInt + have hhi : ¬ a.val > q16MaxRaw := by exact not_lt.mpr a.property.2 + have hlo : ¬ a.val < q16MinRaw := by exact not_lt.mpr a.property.1 + simp [hhi, hlo] + +theorem ofRawInt_toInt_eq_nonneg (i : Int) (h1 : i ≥ 0) (h2 : i ≤ q16MaxRaw) : + (ofRawInt i).toInt = i := by + unfold ofRawInt toInt + have hhi : ¬ i > q16MaxRaw := by omega + have hlo : ¬ i < q16MinRaw := by + dsimp [q16MinRaw] at * + omega + simp [hhi, hlo] + +/-- Saturating constructor lemma for non-negative raw values. -/ +theorem ofRawInt_toInt_eq_general (i : Int) (h1 : i ≥ 0) : + (ofRawInt i).toInt = if i > q16MaxRaw then q16MaxRaw else i := by + by_cases h : i > q16MaxRaw + · unfold ofRawInt toInt + simp [h] + · have hlo : ¬ i < q16MinRaw := by + dsimp [q16MinRaw, q16MaxRaw] at * + omega + unfold ofRawInt toInt + simp [h, hlo] + +/-- `(ofRawInt i).toInt = q16Clamp i` — the bridge between the subtype + constructor and the pure-Int clamp function. -/ +theorem ofRawInt_toInt_eq_clamp (i : Int) : (ofRawInt i).toInt = q16Clamp i := by + unfold ofRawInt toInt q16Clamp + split_ifs <;> rfl + +/-- `@[simp]` version rewriting `.val` directly (avoids `toInt` unfolding + ordering issues in `simp` calls). -/ +@[simp] theorem ofRawInt_val_eq_q16Clamp (i : Int) : (ofRawInt i).val = q16Clamp i := + ofRawInt_toInt_eq_clamp i + +/-- `ofRawInt` is monotone: a ≤ b → (ofRawInt a).toInt ≤ (ofRawInt b).toInt. + One-liner via q16Clamp_monotone. -/ +theorem ofRawInt_monotone (a b : Int) (h : a ≤ b) : + (ofRawInt a).toInt ≤ (ofRawInt b).toInt := by + simp only [ofRawInt_toInt_eq_clamp] + exact q16Clamp_monotone a b h + +/-- Adding a nonnegative Q16_16 value cannot decrease the saturated result. + This is the general form of the motif-scoring monotonicity used in + Semantics.PIST.Motif §6.2: motifScore(match=true) ≥ motifScore(match=false). -/ +theorem add_nonneg_monotone (a b : Q16_16) (hb : 0 ≤ b.toInt) : + a.toInt ≤ (add a b).toInt := by + unfold add + have := ofRawInt_monotone a.toInt (a.toInt + b.toInt) (by omega) + rwa [ofRawInt_toInt] at this + +/-- zero * a = zero. -/ +theorem zero_mul (a : Q16_16) : mul zero a = zero := by + unfold mul + rw [zero_toInt] + simp + +/-- a * zero = zero. -/ +theorem mul_zero (a : Q16_16) : mul a zero = zero := by + unfold mul + rw [zero_toInt] + simp + +/-- a - a = zero. -/ +theorem sub_self (a : Q16_16) : sub a a = zero := by + unfold sub + simp + +/-- a + zero = a. -/ +theorem add_zero (a : Q16_16) : add a zero = a := by + unfold add + rw [zero_toInt] + simp + exact ofRawInt_toInt a + +/-- zero + a = a. -/ +theorem zero_add (a : Q16_16) : add zero a = a := by + unfold add + rw [zero_toInt] + simp + exact ofRawInt_toInt a + +/-- sqrt zero is zero. -/ +theorem sqrt_zero : sqrt zero = zero := by + unfold sqrt + simp + +/-- sqrt one is within one LSB of one. -/ +theorem sqrt_one : (sqrt one).toInt - one.toInt ≤ 1 := by + native_decide + +#eval sqrt zero -- should be zero +#eval sqrt one -- should be ~1.0 (LSB-aligned) +#eval sqrt (Q16_16.ofNat 4) -- should be ~2.0 +#eval sqrt (Q16_16.ofNat 9) -- should be ~3.0 +#eval (sqrt (Q16_16.ofNat 4)).toFloat ≤ 2.1 -- Boolean guard witness + +private theorem int_scale_mul_ediv_cancel (n : Int) : (q16Scale * n) / q16Scale = n := by + rw [Int.mul_ediv_cancel_left] + norm_num [q16Scale] + +/-- one * a = a. -/ +theorem one_mul (a : Q16_16) : mul one a = a := by + unfold mul + show ofRawInt (one.toInt * a.toInt / q16Scale) = a + rw [show one.toInt = q16Scale from rfl] + have h : (q16Scale * a.toInt) / q16Scale = a.toInt := int_scale_mul_ediv_cancel a.toInt + rw [h] + exact ofRawInt_toInt a + +/-- a * one = a. -/ +theorem mul_one (a : Q16_16) : mul a one = a := by + unfold mul + show ofRawInt (a.toInt * one.toInt / q16Scale) = a + rw [show one.toInt = q16Scale from rfl] + have h : (a.toInt * q16Scale) / q16Scale = a.toInt := by + rw [Int.mul_comm] + exact int_scale_mul_ediv_cancel a.toInt + rw [h] + exact ofRawInt_toInt a + +/-- toInt = 0 iff the value is zero. -/ +theorem toInt_eq_zero_iff {a : Q16_16} : a.toInt = 0 ↔ a = zero := by + constructor + · intro h + apply Subtype.ext + simpa [toInt, zero] using h + · intro h + rw [h] + rfl + +/-- zero / x = zero for any nonzero denominator. -/ +theorem zero_div (x : Q16_16) (hx : x.val ≠ 0) : div zero x = zero := by + unfold div + have hx' : ¬ x.toInt = 0 := by + simpa [toInt] using hx + simp [hx', zero_toInt] + +/-- Square is non-negative under signed saturating multiplication. -/ +theorem mul_self_nonneg (a : Q16_16) : (mul a a).toInt ≥ 0 := by + unfold mul + have hprod : a.toInt * a.toInt ≥ 0 := by nlinarith + have hdiv : (a.toInt * a.toInt) / q16Scale ≥ 0 := by + apply Int.ediv_nonneg + · exact hprod + · norm_num [q16Scale] + exact ofRawInt_toInt_nonneg ((a.toInt * a.toInt) / q16Scale) hdiv + +/-- Product of two non-negative Q16.16 values is non-negative. -/ +theorem mul_toInt_nonneg (a b : Q16_16) (ha : a.toInt ≥ 0) (hb : b.toInt ≥ 0) : + (mul a b).toInt ≥ 0 := by + unfold mul + have hprod : a.toInt * b.toInt ≥ 0 := by nlinarith + have hdiv : (a.toInt * b.toInt) / q16Scale ≥ 0 := by + apply Int.ediv_nonneg + · exact hprod + · norm_num [q16Scale] + exact ofRawInt_toInt_nonneg ((a.toInt * b.toInt) / q16Scale) hdiv + +/-- Non-negative addition stays non-negative under saturation. -/ +theorem ofRaw_toInt_nonneg (acc wcc : Q16_16) + (hacc : acc.toInt ≥ 0) (hwcc : wcc.toInt ≥ 0) : + (Q16_16.add acc wcc).toInt ≥ 0 := by + unfold add + have hsum : acc.toInt + wcc.toInt ≥ 0 := by omega + exact ofRawInt_toInt_nonneg (acc.toInt + wcc.toInt) hsum + +/-- Compatibility lemma: a non-negative raw value decoded through saturation is non-negative. -/ +theorem mk_lt_half_nonneg (s : Int) (hs : s ≥ 0) (_h : s < 2147483648) : + (ofRawInt s).toInt ≥ 0 := by + exact ofRawInt_toInt_nonneg s hs + +/-- Positive raw addition remains positive under saturation. -/ +theorem add_pos_of_pos (a b : Q16_16) (ha : a.toInt > 0) (hb : b.toInt > 0) : + (add a b).toInt > 0 := by + unfold add + have hsum : a.toInt + b.toInt ≥ 1 := by omega + have hge : (ofRawInt (a.toInt + b.toInt)).toInt ≥ 1 := + ofRawInt_toInt_ge (a.toInt + b.toInt) 1 hsum + (by norm_num [q16MinRaw]) (by norm_num [q16MaxRaw]) + omega + +/-- (1 + omega).toInt ≥ 65536 when omega.toInt ≥ 0. -/ +theorem add_one_omega_ge_one (omega : Q16_16) (h : omega.toInt ≥ 0) : + (add one omega).toInt ≥ 65536 := by + unfold add + have hsum : one.toInt + omega.toInt ≥ 65536 := by + rw [one_toInt] + omega + exact ofRawInt_toInt_ge (one.toInt + omega.toInt) 65536 hsum + (by norm_num [q16MinRaw]) (by norm_num [q16MaxRaw]) + +/-- Non-negative Q16.16 values are bounded by maxVal. -/ +theorem toInt_nonneg_le_maxVal (q : Q16_16) (_h : q.toInt ≥ 0) : q.toInt ≤ q16MaxRaw := by + exact q.property.2 + +/-- Adding epsilon to a non-negative value yields a positive value. -/ +theorem epsilon_add_pos {r : Q16_16} (hr : r.toInt ≥ 0) : + (r + epsilon).toInt > 0 := by + change (add r epsilon).toInt > 0 + unfold add + have hsum : r.toInt + epsilon.toInt ≥ 1 := by + rw [epsilon_toInt] + omega + have hge : (ofRawInt (r.toInt + epsilon.toInt)).toInt ≥ 1 := + ofRawInt_toInt_ge (r.toInt + epsilon.toInt) 1 hsum + (by norm_num [q16MinRaw]) (by norm_num [q16MaxRaw]) + omega + +/-- `abs (sub a b) = abs (sub b a)` — absolute value of a difference + is symmetric. Holds for all Q16_16 values (proved by case analysis + on `a.val - b.val` at the Int clamping boundary). -/ +lemma q16Clamp_eq_q16MaxRaw_of_ge {x : Int} (h : x ≥ q16MaxRaw) : q16Clamp x = q16MaxRaw := by + dsimp [q16Clamp] + by_cases hx : x > q16MaxRaw + · simp [hx] + · have hx_eq : x = q16MaxRaw := le_antisymm (le_of_not_gt hx) h + subst hx_eq; simp [q16Clamp, q16MaxRaw, q16MinRaw] + +lemma q16Clamp_eq_q16MinRaw_of_le {x : Int} (h : x ≤ q16MinRaw) : q16Clamp x = q16MinRaw := by + dsimp [q16Clamp] + by_cases hx_hi : x > q16MaxRaw + · unfold q16MinRaw q16MaxRaw at *; omega + · by_cases hx_lo : x < q16MinRaw + · simp [hx_hi, hx_lo] + · have hx_eq : x = q16MinRaw := le_antisymm h (by + by_contra hlt + apply hx_lo + exact lt_of_not_ge hlt) + subst hx_eq; simp [q16Clamp, q16MaxRaw, q16MinRaw] + +private lemma not_q16MaxRaw_lt_0 : ¬ q16MaxRaw < 0 := by unfold q16MaxRaw; omega + +private lemma q16Clamp_2147483648_eq_q16MaxRaw : q16Clamp (2147483648 : Int) = q16MaxRaw := by + unfold q16Clamp q16MaxRaw q16MinRaw; omega + +private lemma val_if (c : Prop) [Decidable c] (x y : Q16_16) : (if c then x else y).val = (if c then x.val else y.val) := by + split <;> rfl + +theorem abs_sub_comm (a b : Q16_16) : abs (sub a b) = abs (sub b a) := by + apply Q16_16.ext + simp [abs, sub, neg, toInt, val_if, ofRawInt_val_eq_q16Clamp] + have hswap : q16Clamp (b.val - a.val) = q16Clamp (-(a.val - b.val)) := by + have : b.val - a.val = -(a.val - b.val) := by omega + rw [this] + rw [hswap] + set d := a.val - b.val + have hswap' : q16Clamp (-(a.val - b.val)) = q16Clamp (-d) := by rfl + rw [hswap'] + by_cases hd_above : d > q16MaxRaw + · have h_cd : q16Clamp d = q16MaxRaw := q16Clamp_eq_q16MaxRaw_of_ge (le_of_lt hd_above) + have h_nd_low : -d ≤ q16MinRaw := by unfold q16MaxRaw q16MinRaw at *; omega + have h_cnd : q16Clamp (-d) = q16MinRaw := q16Clamp_eq_q16MinRaw_of_le h_nd_low + rw [h_cd, h_cnd] + unfold q16Clamp q16MaxRaw q16MinRaw; norm_num + · by_cases hd_below : d < q16MinRaw + · have h_cd : q16Clamp d = q16MinRaw := q16Clamp_eq_q16MinRaw_of_le (by omega) + have h_nd_high : -d ≥ q16MaxRaw := by unfold q16MaxRaw q16MinRaw at *; omega + have h_cnd : q16Clamp (-d) = q16MaxRaw := q16Clamp_eq_q16MaxRaw_of_ge h_nd_high + rw [h_cd, h_cnd] + unfold q16Clamp q16MaxRaw q16MinRaw; norm_num + · have h_lo : q16MinRaw ≤ d := by unfold q16MinRaw q16MaxRaw at *; omega + have h_hi : d ≤ q16MaxRaw := by unfold q16MinRaw q16MaxRaw at *; omega + have h_cd : q16Clamp d = d := q16Clamp_id_of_inRange d h_lo h_hi + rw [h_cd] + by_cases h_nd_above : -d > q16MaxRaw + · have h_d_min : d = q16MinRaw := by unfold q16MinRaw q16MaxRaw at *; omega + rw [h_d_min] + unfold q16Clamp q16MaxRaw q16MinRaw; norm_num + · by_cases h_nd_below : -d < q16MinRaw + · have h_d_max : d = q16MaxRaw := by unfold q16MinRaw q16MaxRaw at *; omega + rw [h_d_max] + unfold q16Clamp q16MaxRaw q16MinRaw; norm_num + · have h_nd_lo' : q16MinRaw ≤ -d := by omega + have h_nd_hi' : -d ≤ q16MaxRaw := by omega + have h_cnd : q16Clamp (-d) = -d := q16Clamp_id_of_inRange (-d) h_nd_lo' h_nd_hi' + rw [h_cnd, show (-(-d : Int) = d) by omega] + by_cases hd_neg : d < 0 + · omega + · by_cases hd_zero : d = 0 + · rw [hd_zero] + unfold q16Clamp q16MinRaw q16MaxRaw; norm_num + · have hd_pos : 0 < d := by omega + rw [h_cd] + split_ifs <;> omega + +/-- Subtraction is addition of the negation: a - b = a + (-b). + + NOTE: This theorem is NOT universally true for Q16_16. Counterexample: + `a = b = q16MinRaw` gives LHS = 0, RHS = -1. The difference arises because + `neg q16MinRaw` overflows to `q16MaxRaw`, altering the clamping path. + SSMS does not use this theorem — the `bound` proof has been restructured + to avoid it. -/ +theorem sub_eq_add_neg (a b : Q16_16) (hb : b.toInt > q16MinRaw) : sub a b = add a (neg b) := by + have h_neg_inRange_lo : q16MinRaw ≤ -b.toInt := by + have h := b.property.2 + dsimp [toInt] at h ⊢ + dsimp [q16MaxRaw, q16MinRaw] at h ⊢ + omega + have h_neg_inRange_hi : -b.toInt ≤ q16MaxRaw := by + dsimp [toInt] at hb ⊢ + dsimp [q16MinRaw] at hb + dsimp [q16MaxRaw] + omega + have h_neg_int : (neg b).toInt = -b.toInt := by + rw [neg, ofRawInt_toInt_eq_clamp] + apply q16Clamp_id_of_inRange _ h_neg_inRange_lo h_neg_inRange_hi + rw [sub, add, h_neg_int] + rfl + +/-- Multiplication by a non-negative scalar is monotone: + if a ≤ b and c ≥ 0, then a*c ≤ b*c. + Used in SSMS.aciPreservedByMlgruStep for bound propagation. -/ +theorem mul_mono_left (a b c : Q16_16) (h : a.toInt ≤ b.toInt) (hc : c.toInt ≥ 0) : + (mul a c).toInt ≤ (mul b c).toInt := by + unfold mul + have hmul : a.toInt * c.toInt ≤ b.toInt * c.toInt := by + apply Int.mul_le_mul_of_nonneg_right h hc + have hpos : 0 < q16Scale := by unfold q16Scale; norm_num + have hdiv : (a.toInt * c.toInt) / q16Scale ≤ (b.toInt * c.toInt) / q16Scale := by + apply Int.ediv_le_ediv hpos hmul + rw [ofRawInt_toInt_eq_clamp, ofRawInt_toInt_eq_clamp] + exact q16Clamp_monotone _ _ hdiv + +/-- Multiplication by a non-negative scalar is monotone on the right. -/ +theorem mul_mono_right (a b c : Q16_16) (h : a.toInt ≤ b.toInt) (hc : c.toInt ≥ 0) : + (mul c a).toInt ≤ (mul c b).toInt := by + unfold mul + have hmul : c.toInt * a.toInt ≤ c.toInt * b.toInt := by + apply Int.mul_le_mul_of_nonneg_left h hc + have hpos : 0 < q16Scale := by unfold q16Scale; norm_num + have hdiv : (c.toInt * a.toInt) / q16Scale ≤ (c.toInt * b.toInt) / q16Scale := by + apply Int.ediv_le_ediv hpos hmul + rw [ofRawInt_toInt_eq_clamp, ofRawInt_toInt_eq_clamp] + exact q16Clamp_monotone _ _ hdiv + +/-- Addition is monotone in the left argument: + if a ≤ b then a+c ≤ b+c. -/ +theorem add_le_add (a b c : Q16_16) (h : a.toInt ≤ b.toInt) : + (add a c).toInt ≤ (add b c).toInt := by + unfold add + simp [ofRawInt_toInt_eq_clamp] + apply q16Clamp_monotone + omega + +/-- Absolute value of any Q16_16 value is non-negative. -/ +theorem abs_nonneg (a : Q16_16) : (abs a).toInt ≥ 0 := by + unfold abs neg + have h := a.property.1 + split_ifs with hlt + · rw [ofRawInt_toInt_eq_clamp] + have h_nonneg : 0 ≤ -a.toInt := by omega + exact q16Clamp_nonneg_of_nonneg h_nonneg + · omega + +/-- When addition does not saturate (the raw sum is in [q16MinRaw, q16MaxRaw]), + the saturating `add` coincides with raw addition. Follows immediately + from `q16Clamp_id_of_inRange` after rewriting via `ofRawInt_toInt_eq_clamp`. -/ +theorem add_toInt_of_no_sat (a b : Q16_16) + (hlo : q16MinRaw ≤ a.toInt + b.toInt) (hhi : a.toInt + b.toInt ≤ q16MaxRaw) : + (add a b).toInt = a.toInt + b.toInt := by + unfold add + rw [ofRawInt_toInt_eq_clamp] + exact q16Clamp_id_of_inRange _ hlo hhi + +/-- When subtraction does not saturate, the saturating `sub` coincides with + raw subtraction. -/ +theorem sub_toInt_of_no_sat (a b : Q16_16) + (hlo : q16MinRaw ≤ a.toInt - b.toInt) (hhi : a.toInt - b.toInt ≤ q16MaxRaw) : + (sub a b).toInt = a.toInt - b.toInt := by + unfold sub + rw [ofRawInt_toInt_eq_clamp] + exact q16Clamp_id_of_inRange _ hlo hhi + +/-- Q16.16 multiplication rounds down to the integer floor for non-negative + operands. The saturated result is at most `a*b/q16Scale`. + + The non-negative hypothesis gives `a*b/q16Scale ≥ 0 ≥ q16MinRaw`, so + `q16Clamp` does not clamp the floor from below. Combined with the + trivial `q16Clamp x ≤ q16MaxRaw` upper saturation, we get + `q16Clamp (a*b/q16Scale) ≤ a*b/q16Scale`. + + Mirrors the `unfold mul; rw [ofRawInt_toInt_eq_clamp]` pattern used in + `mul_mono_left`. -/ +theorem mul_floor_le (a b : Q16_16) (ha : 0 ≤ a.toInt) (hb : 0 ≤ b.toInt) : + (mul a b).toInt ≤ (a.toInt * b.toInt) / q16Scale := by + unfold mul + rw [ofRawInt_toInt_eq_clamp] + have h_nonneg : 0 ≤ a.toInt * b.toInt / q16Scale := by + apply Int.ediv_nonneg + · nlinarith + · norm_num [q16Scale] + have h_ge_lo : q16MinRaw ≤ a.toInt * b.toInt / q16Scale := by + dsimp [q16MinRaw] + omega + unfold q16Clamp + by_cases h_hi : a.toInt * b.toInt / q16Scale > q16MaxRaw + · dsimp [q16MaxRaw] at * + simp [h_hi] + omega + · by_cases h_lo : a.toInt * b.toInt / q16Scale < q16MinRaw + · dsimp [q16MinRaw] at * + omega + · simp [h_hi, h_lo] + +/-- For non-negative operands, when the integer floor of the product fits + within the Q16.16 range, multiplication is at least the floor. + + The hypothesis `a*b/q16Scale ≤ q16MaxRaw` rules out upper saturation, + so `q16Clamp` does not clamp the floor from above. Together with + `a*b/q16Scale ≥ 0 ≥ q16MinRaw` (from non-negativity) we get + `q16Clamp (a*b/q16Scale) ≥ a*b/q16Scale`. -/ +theorem mul_floor_ge (a b : Q16_16) (ha : 0 ≤ a.toInt) (hb : 0 ≤ b.toInt) + (hhi : a.toInt * b.toInt / q16Scale ≤ q16MaxRaw) : + (mul a b).toInt ≥ (a.toInt * b.toInt) / q16Scale := by + unfold mul + rw [ofRawInt_toInt_eq_clamp] + have h_nonneg : 0 ≤ a.toInt * b.toInt / q16Scale := by + apply Int.ediv_nonneg + · nlinarith + · norm_num [q16Scale] + unfold q16Clamp + by_cases h_hi : a.toInt * b.toInt / q16Scale > q16MaxRaw + · dsimp [q16MaxRaw] at * + omega + · by_cases h_lo : a.toInt * b.toInt / q16Scale < q16MinRaw + · dsimp [q16MinRaw] at * + simp [h_hi, h_lo] + omega + · simp [h_hi, h_lo] + +/-- Combined error bound for Q16.16 multiplication on non-negative operands. + When the integer floor of the product fits in [q16MinRaw, q16MaxRaw], + multiplication is exact: `(mul a b).toInt = a*b/q16Scale`. + + Combines `mul_floor_le` (upper bound) and `mul_floor_ge` (lower bound) + via `Int.le_antisymm`. The two-sided bound closes the saturation + envelope: no clamp from above (hhi) and no clamp from below + (automatic from non-negativity). -/ +theorem mul_floor_error (a b : Q16_16) (ha : 0 ≤ a.toInt) (hb : 0 ≤ b.toInt) + (hhi : a.toInt * b.toInt / q16Scale ≤ q16MaxRaw) : + (mul a b).toInt = (a.toInt * b.toInt) / q16Scale := by + apply Int.le_antisymm + · exact mul_floor_le a b ha hb + · exact mul_floor_ge a b ha hb hhi + +-- REMOVED: Theorems abs_mul_le and abs_triangle are FALSE for Q16_16 with floor division +-- abs_mul_le: counterexample a=3, b=-1 gives LHS=1, RHS=0 +-- abs_triangle: counterexample a=3, b=-3 gives LHS=1, RHS=0 +-- See TODO comments in original file for restructure guidance + +/-- `ofNat` is monotone: a ≤ b → ofNat a ≤ ofNat b. -/ +theorem ofNat_le (a b : Nat) (h : a ≤ b) : ofNat a ≤ ofNat b := by + have h' : (a : Int) * q16Scale ≤ (b : Int) * q16Scale := by + have h_nonneg : 0 ≤ (q16Scale : Int) := by norm_num [q16Scale] + have h_int : (a : Int) ≤ (b : Int) := by exact_mod_cast h + exact mul_le_mul_of_nonneg_right h_int h_nonneg + exact ofRawInt_monotone _ _ h' + +/-- `ofNat` returns non-negative values. -/ +theorem ofNat_nonneg (n : Nat) : 0 ≤ (ofNat n).toInt := by + unfold ofNat + apply ofRawInt_toInt_nonneg + have hpos : 0 ≤ (n : Int) * q16Scale := + mul_nonneg (Nat.cast_nonneg _) (by norm_num [q16Scale]) + exact hpos + +/-- Addition is monotone in both arguments. -/ +theorem add_le_add' (a b c d : Q16_16) (hac : a ≤ c) (hbd : b ≤ d) : a + b ≤ c + d := by + have h_sum : a.toInt + b.toInt ≤ c.toInt + d.toInt := Int.add_le_add hac hbd + have h_clamp : q16Clamp (a.toInt + b.toInt) ≤ q16Clamp (c.toInt + d.toInt) := + q16Clamp_monotone _ _ h_sum + have h_add_toInt (x y : Q16_16) : (x + y).toInt = q16Clamp (x.toInt + y.toInt) := by + rw [show x + y = add x y by rfl] + rw [add] + apply ofRawInt_toInt_eq_clamp + calc + (a + b).toInt = q16Clamp (a.toInt + b.toInt) := h_add_toInt _ _ + _ ≤ q16Clamp (c.toInt + d.toInt) := h_clamp + _ = (c + d).toInt := (h_add_toInt _ _).symm + +end Q16_16 + +-- ═══════════════════════════════════════════════════════════════════════════ +-- Q0.64 signed normalized fraction +-- ═══════════════════════════════════════════════════════════════════════════ + +def q0_64MinRaw : Int := -9223372036854775808 +def q0_64MaxRaw : Int := 9223372036854775807 +def q0_64ScaleNat : Nat := 9223372036854775808 + +def q0_64ScaleFloat : Float := 9223372036854775808.0 + +/-- +Q0.64 pure fraction representation. +The canonical proof model stores the signed raw integer in the Int64 range. +-/ +abbrev Q0_64 := { x : Int // q0_64MinRaw ≤ x ∧ x ≤ q0_64MaxRaw } + +instance : Repr Q0_64 where + reprPrec q _ := repr q.val + +instance : BEq Q0_64 where + beq a b := a.val == b.val + +instance : Inhabited Q0_64 where + default := ⟨0, by constructor <;> norm_num [q0_64MinRaw, q0_64MaxRaw]⟩ + +instance : ToJson Q0_64 where + toJson q := Json.mkObj [("val", toJson q.val)] + +namespace Q0_64 + +@[ext] +theorem ext {a b : Q0_64} (h : a.val = b.val) : a = b := Subtype.ext h + +@[inline] +def toInt (q : Q0_64) : Int := q.val + +@[inline] +def ofRawInt (raw : Int) : Q0_64 := + if hhi : raw > q0_64MaxRaw then + ⟨q0_64MaxRaw, by constructor <;> norm_num [q0_64MinRaw, q0_64MaxRaw]⟩ + else if hlo : raw < q0_64MinRaw then + ⟨q0_64MinRaw, by constructor <;> norm_num [q0_64MinRaw, q0_64MaxRaw]⟩ + else + ⟨raw, by + constructor + · dsimp [q0_64MinRaw, q0_64MaxRaw] at *; omega + · dsimp [q0_64MinRaw, q0_64MaxRaw] at *; omega⟩ + +instance : FromJson Q0_64 where + fromJson? j := do + let raw : Int ← fromJson? (← j.getObjVal? "val") + pure (ofRawInt raw) + +/-- Maximum positive value. -/ +def one : Q0_64 := ofRawInt q0_64MaxRaw + +def zero : Q0_64 := ofRawInt 0 + +def ofRatio (num : Nat) (den : Nat) : Q0_64 := + if den = 0 then zero + else ofRawInt (Int.ofNat (num * q0_64ScaleNat / den)) + +def half : Q0_64 := ofRawInt 4611686018427387903 + +def neg (x : Q0_64) : Q0_64 := ofRawInt (-x.toInt) +def add (a b : Q0_64) : Q0_64 := ofRawInt (a.toInt + b.toInt) +def sub (a b : Q0_64) : Q0_64 := ofRawInt (a.toInt - b.toInt) +def mul (a b : Q0_64) : Q0_64 := + ofRawInt ((a.toInt * b.toInt) / Int.ofNat q0_64ScaleNat) +def div (a b : Q0_64) : Q0_64 := + if b.toInt = 0 then one + else ofRawInt ((a.toInt * Int.ofNat q0_64ScaleNat) / b.toInt) +def abs (x : Q0_64) : Q0_64 := if x.toInt < 0 then neg x else x + +def ofFloat (f : Float) : Q0_64 := + if f.isNaN || f ≥ 1.0 then one + else if f ≤ -1.0 then ofRawInt q0_64MinRaw + else if f < 0.0 then + ofRawInt (-(Int.ofNat ((-f * q0_64ScaleFloat).floor.toUInt64.toNat))) + else + ofRawInt (Int.ofNat ((f * q0_64ScaleFloat).floor.toUInt64.toNat)) + +def toFloat (q : Q0_64) : Float := + Float.ofInt q.toInt / q0_64ScaleFloat + +instance : Add Q0_64 := ⟨add⟩ +instance : Sub Q0_64 := ⟨sub⟩ +instance : Mul Q0_64 := ⟨mul⟩ +instance : Div Q0_64 := ⟨div⟩ +instance : Neg Q0_64 := ⟨neg⟩ + +instance : LE Q0_64 where + le a b := a.toInt ≤ b.toInt + +instance : LT Q0_64 where + lt a b := a.toInt < b.toInt + +instance : DecidableRel (fun a b : Q0_64 => a ≤ b) := + fun a b => inferInstanceAs (Decidable (a.toInt ≤ b.toInt)) + +instance : DecidableRel (fun a b : Q0_64 => a < b) := + fun a b => inferInstanceAs (Decidable (a.toInt < b.toInt)) + +end Q0_64 + +-- ═══════════════════════════════════════════════════════════════════════════ +-- ═══════════════════════════════════════════════════════════════════════════ +-- Inverse Trig Witnesses +-- ═══════════════════════════════════════════════════════════════════════════ + +-- atan(0) = 0 +#eval (Q16_16.atan Q16_16.zero).toInt -- expect: 0 + +-- atan(1) = π/4 ≈ 0.7854 → raw ≈ 51471 +#eval (Q16_16.atan Q16_16.one).toInt -- expect: ~51471 + +-- atan(-1) = -π/4 +#eval (Q16_16.atan (Q16_16.neg Q16_16.one)).toInt -- expect: ~-51471 + +-- atan(large) ≈ π/2 (100.0 in Q16.16) +#eval (Q16_16.atan (Q16_16.ofRawInt 6553600)).toInt -- expect: ~102943 + +-- asin(0) = 0 +#eval (Q16_16.asin Q16_16.zero).toInt -- expect: 0 + +-- asin(1) = π/2 +#eval (Q16_16.asin Q16_16.one).toInt -- expect: ~102943 + +-- asin(-1) = -π/2 +#eval (Q16_16.asin (Q16_16.neg Q16_16.one)).toInt -- expect: ~-102943 + +-- asin(0.5) ≈ 0.5236 +#eval (Q16_16.asin (Q16_16.div Q16_16.one Q16_16.two)).toInt -- expect: ~34306 + +-- acos(0) = π/2 +#eval (Q16_16.acos Q16_16.zero).toInt -- expect: ~102943 + +-- acos(1) = 0 +#eval (Q16_16.acos Q16_16.one).toInt -- expect: ~0 + +-- acos(-1) = π +#eval (Q16_16.acos (Q16_16.neg Q16_16.one)).toInt -- expect: ~205887 + +-- atan2(1, 0) = π/2 +#eval (Q16_16.atan2 Q16_16.one Q16_16.zero).toInt -- expect: ~102943 + +-- atan2(0, 1) = 0 +#eval (Q16_16.atan2 Q16_16.zero Q16_16.one).toInt -- expect: 0 + +-- atan2(1, 1) = π/4 +#eval (Q16_16.atan2 Q16_16.one Q16_16.one).toInt -- expect: ~51471 + +-- atan2(-1, -1) = -3π/4 +#eval (Q16_16.atan2 (Q16_16.neg Q16_16.one) (Q16_16.neg Q16_16.one)).toInt -- expect: ~-154415 + +-- Pandigital π Approximation +-- ═══════════════════════════════════════════════════════════════════════════ + +namespace PandigitalPi + +/-- High term: 3.8415926. -/ +def highTerm : Q16_16 := Q16_16.ofRawInt 251819 + +/-- Low term: 0.7. -/ +def lowTerm : Q16_16 := Q16_16.ofRawInt 45875 + +def piPandigital : Q16_16 := highTerm - lowTerm + +def piDirect : Q16_16 := Q16_16.ofRawInt 205944 + +theorem piPandigitalCorrect : (piPandigital.toInt - piDirect.toInt).natAbs ≤ 1 := by + native_decide + +def spaceAnalysis : String := + "Pandigital pi: 6 bytes packed vs 4 bytes direct Q16.16 (trade-off for mathematical elegance)" + +#eval piPandigital.toFloat +#eval piDirect.toFloat +#eval (piPandigital.toInt - piDirect.toInt).natAbs + +end PandigitalPi + +end SilverSight.FixedPoint + +namespace SilverSight + export FixedPoint (Q0_16 Q16_16 Q0_64) + namespace Q16_16 + export FixedPoint.Q16_16 + (zero one negOne epsilon two infinity maxVal minVal ofNat satFromNat ofRatio toInt + ofRawInt ofBits toBits ofFloat toFloat scale ofInt add sub mul div abs neg sqrt ln log2 pow sin log + expNeg sat01 max min le ge gt lt recip ofRaw clip isNeg zero_mul mul_zero one_mul + mul_one zero_add add_zero sub_self zero_toInt one_toInt epsilon_toInt + epsilon_toInt_pos toInt_eq_zero_iff epsilon_add_pos zero_div mul_self_nonneg + mul_toInt_nonneg ofRaw_toInt_nonneg mk_lt_half_nonneg add_one_omega_ge_one + toInt_nonneg_le_maxVal add_pos_of_pos) + end Q16_16 + namespace Q0_16 + export FixedPoint.Q0_16 (zero one half neg add sub mul div abs lt le gt ge toFloat ofFloat log2 min) + end Q0_16 + namespace Q0_64 + export FixedPoint.Q0_64 (one zero ofRatio half neg add sub mul div abs toInt ofFloat toFloat) + end Q0_64 + namespace PandigitalPi + export FixedPoint.PandigitalPi (highTerm lowTerm piPandigital piDirect piPandigitalCorrect spaceAnalysis) + end PandigitalPi +end SilverSight diff --git a/formal/CoreFormalism/Q16_16_Spec.lean b/formal/CoreFormalism/Q16_16_Spec.lean deleted file mode 100644 index 852e7b5a..00000000 --- a/formal/CoreFormalism/Q16_16_Spec.lean +++ /dev/null @@ -1,292 +0,0 @@ -/- Q16_16 Canonical Specification - - Q16_16 represents fixed-point numbers with 16 integer bits and 16 fractional bits. - Range: [-32768.0, 32767.9999847412109375] - Resolution: 1/65536 ≈ 0.0000152587890625 - - CANONICAL ROUNDING MODE: round-half-up (banker's rounding) - - Values exactly at half-LSB round to nearest even - - All other values round to nearest - - This specification is the single source of truth. All language implementations - (Lean, Python, C) MUST produce identical results for all operations. - - FILE: CoreFormalism/Q16_16_Spec.lean - STATUS: canonical specification (source of truth) - STAGE: Stage 1 Foundation --/ - -import Mathlib.Data.Int.Basic -import Mathlib.Data.Real.Basic - -namespace Q16_16_Canonical - --- ============================================================ --- §1 CONSTANTS AND TYPE --- ============================================================ - -/-- Scale factor: 2^16 = 65536. The number of subdivisions per unit. -/ -def Q16_SCALE : ℕ := 65536 - -/-- Maximum representable integer value before scaling. -/ -def Q16_MAX_RAW : ℤ := 2147483647 -- INT32_MAX - -/-- Minimum representable integer value before scaling. -/ -def Q16_MIN_RAW : ℤ := -2147483648 -- INT32_MIN - -/-- Q16_16 is represented as a 32-bit signed integer internally, - where the raw value = floor(x * 65536) after canonical rounding. -/ -def Q16_16 := { q : ℤ // q ≥ Q16_MIN_RAW ∧ q ≤ Q16_MAX_RAW } - --- ============================================================ --- §2 CONVERSIONS --- ============================================================ - -/-- Convert a Float to Q16_16 with canonical round-half-up (banker's rounding). - - Algorithm: - scaled = f * 65536.0 - If |scaled - round(scaled)| == 0.5: - round to nearest even - Else: - round to nearest integer - - This matches Python's round() with no ndigits specified and C's - round() from math.h with the half-way case going to nearest even. --/ -def ofFloat (f : Float) : Q16_16 := - let scaled := f * (Float.ofNat Q16_SCALE) - let rounded := Float.round scaled - let clipped := max (Float.ofInt Q16_MIN_RAW) (min (Float.ofInt Q16_MAX_RAW) rounded) - ⟨Float.toInt clipped, by - -- Proof obligation: result is in valid range - simp [Q16_MIN_RAW, Q16_MAX_RAW] - -- Clip guarantees bounds - have h1 : Float.toInt clipped ≥ -2147483648 := by - have h_clip : clipped ≥ Float.ofInt (-2147483648 : ℤ) := by - apply max_le_iff.mpr - left - apply le_refl - have h2 : Float.toInt (Float.ofInt (-2147483648 : ℤ)) = -2147483648 := by - simp [Float.toInt_ofInt] - have h3 : Float.toInt clipped ≥ Float.toInt (Float.ofInt (-2147483648 : ℤ)) := by - apply Float.toInt_le_toInt - exact h_clip - rw [h2] at h3 - exact h3 - have h2 : Float.toInt clipped ≤ 2147483647 := by - have h_clip : clipped ≤ Float.ofInt (2147483647 : ℤ) := by - apply min_le_iff.mpr - left - apply le_refl - have h2 : Float.toInt (Float.ofInt (2147483647 : ℤ)) = 2147483647 := by - simp [Float.toInt_ofInt] - have h3 : Float.toInt clipped ≤ Float.toInt (Float.ofInt (2147483647 : ℤ)) := by - apply Float.toInt_le_toInt - exact h_clip - rw [h2] at h3 - exact h3 - exact ⟨h1, h2⟩⟩ - -/-- Convert Q16_16 to Float. Exact (no rounding needed). -/ -def toFloat (q : Q16_16) : Float := - Float.ofInt q.val / (Float.ofNat Q16_SCALE) - -/-- Convert an Int to Q16_16 (exact, no rounding). -/ -def ofInt (i : ℤ) : Q16_16 := - let scaled := i * (Q16_SCALE : ℤ) - let clipped := max Q16_MIN_RAW (min Q16_MAX_RAW scaled) - ⟨clipped, by - simp [Q16_MIN_RAW, Q16_MAX_RAW] - constructor - · exact le_trans (by norm_num) (show -2147483648 ≤ clipped from by - have h : Q16_MIN_RAW ≤ clipped := by apply max_le_iff.mpr; left; norm_num - exact h) - · have h : clipped ≤ Q16_MAX_RAW := by apply min_le_iff.mpr; left; norm_num - exact le_trans h (by norm_num)⟩ - -/-- Convert Q16_16 to Int (truncates fractional part, rounds toward zero). -/ -def toInt (q : Q16_16) : ℤ := - q.val / (Q16_SCALE : ℤ) - --- ============================================================ --- §3 ARITHMETIC OPERATIONS --- ============================================================ - -/-- Addition with saturation (clamped to range, no overflow wrap). -/ -def add (a b : Q16_16) : Q16_16 := - let sum := a.val + b.val - let clipped := max Q16_MIN_RAW (min Q16_MAX_RAW sum) - ⟨clipped, by - constructor - · have h : Q16_MIN_RAW ≤ clipped := by apply max_le_iff.mpr; left; rfl - exact h - · have h : clipped ≤ Q16_MAX_RAW := by apply min_le_iff.mpr; left; rfl - exact h⟩ - -/-- Subtraction with saturation. -/ -def sub (a b : Q16_16) : Q16_16 := - let diff := a.val - b.val - let clipped := max Q16_MIN_RAW (min Q16_MAX_RAW diff) - ⟨clipped, by - constructor - · have h : Q16_MIN_RAW ≤ clipped := by apply max_le_iff.mpr; left; rfl - exact h - · have h : clipped ≤ Q16_MAX_RAW := by apply min_le_iff.mpr; left; rfl - exact h⟩ - -/-- Multiplication: result = (a.val * b.val) / 65536 with canonical rounding. - - Uses 64-bit intermediate to prevent overflow, then applies - canonical round-half-up before clamping to 32-bit range. --/ -def mul (a b : Q16_16) : Q16_16 := - let prod_64 := (a.val : ℤ) * (b.val : ℤ) - -- Divide by scale with rounding: prod_64 / 65536 with half-up - let scaled := prod_64 / (Q16_SCALE : ℤ) - let remainder := prod_64 % (Q16_SCALE : ℤ) - let half_scale := (Q16_SCALE : ℤ) / 2 - let rounded := - if remainder > half_scale then scaled + 1 - else if remainder < half_scale then scaled - else if (scaled % 2) = 0 then scaled -- tie: round to even - else scaled + 1 - let clipped := max Q16_MIN_RAW (min Q16_MAX_RAW rounded) - ⟨clipped, by - constructor - · have h : Q16_MIN_RAW ≤ clipped := by apply max_le_iff.mpr; left; rfl - exact h - · have h : clipped ≤ Q16_MAX_RAW := by apply min_le_iff.mpr; left; rfl - exact h⟩ - -/-- Division: result = (a.val * 65536) / b.val with canonical rounding. - - b must be non-zero. Uses 64-bit intermediate precision. --/ -def div (a b : Q16_16) (hb : b.val ≠ 0) : Q16_16 := - let num_64 := (a.val : ℤ) * (Q16_SCALE : ℤ) - let scaled := num_64 / b.val - let remainder := num_64 % b.val - let half_b := b.val / 2 - let rounded := - if remainder > half_b then scaled + 1 - else if remainder < half_b then scaled - else if (scaled % 2) = 0 then scaled -- tie: round to even - else scaled + 1 - let clipped := max Q16_MIN_RAW (min Q16_MAX_RAW rounded) - ⟨clipped, by - constructor - · have h : Q16_MIN_RAW ≤ clipped := by apply max_le_iff.mpr; left; rfl - exact h - · have h : clipped ≤ Q16_MAX_RAW := by apply min_le_iff.mpr; left; rfl - exact h⟩ - --- ============================================================ --- §4 COMPARISON OPERATIONS --- ============================================================ - -def eq (a b : Q16_16) : Bool := a.val = b.val -def lt (a b : Q16_16) : Bool := a.val < b.val -def le (a b : Q16_16) : Bool := a.val ≤ b.val - --- ============================================================ --- §5 ROUNDTRIP THEOREMS (Core Correctness Properties) --- ============================================================ - -/-- The roundtrip error for float→Q16_16→float is bounded by 1/65536. - This is the fundamental correctness property of the encoding. -/ -theorem roundtrip_float_error (f : Float) (h_min : f ≥ -32768.0) (h_max : f ≤ 32767.9999847412109375) : - let q := ofFloat f - let f' := toFloat q - (f' - f).abs ≤ 1.0 / (Float.ofNat Q16_SCALE) := by - -- Proof sketch: ofFloat rounds to nearest representable value - -- with error ≤ 0.5 LSB = 0.5/65536. toFloat is exact inverse. - -- Therefore |f' - f| ≤ 1/65536. - simp [ofFloat, toFloat, Q16_SCALE] - -- Detailed proof requires Float.toInt_round properties - sorry -- TODO: complete with Float library lemmas - -/-- Integer roundtrip is exact for all integers in the valid range. -/ -theorem roundtrip_int_exact (i : ℤ) (h_min : i ≥ -32768) (h_max : i ≤ 32767) : - toInt (ofInt i) = i := by - simp [toInt, ofInt, Q16_SCALE, Q16_MIN_RAW, Q16_MAX_RAW] - -- scaled = i * 65536 is within [-2^31, 2^31-1] for i in [-32768, 32767] - have h_range : -2147483648 ≤ i * 65536 ∧ i * 65536 ≤ 2147483647 := by - constructor - · nlinarith - · nlinarith - -- Clipping is a no-op for in-range values - have h_clip : max (-2147483648) (min 2147483647 (i * 65536)) = i * 65536 := by - rw [min_eq_right h_range.2] - rw [max_eq_left h_range.1] - rw [h_clip] - -- Division reverses the scaling - have h_div : (i * 65536) / 65536 = i := by - field_simp - exact h_div - -/-- Zero is represented exactly. -/ -theorem zero_exact : ofFloat 0.0 = ⟨0, by norm_num⟩ := by - simp [ofFloat, Q16_SCALE, Q16_MIN_RAW, Q16_MAX_RAW] - sorry -- Requires Float.round_zero lemma - -/-- One is represented exactly. -/ -theorem one_exact : ofFloat 1.0 = ⟨65536, by norm_num⟩ := by - simp [ofFloat, Q16_SCALE, Q16_MIN_RAW, Q16_MAX_RAW] - sorry -- Requires Float.round and toInt_ofInt lemmas - --- ============================================================ --- §6 SPECIFICATION OF CANONICAL ROUNDING FOR VERIFICATION --- ============================================================ - -/-- The canonical rounding function for Q16_16. - - This is the mathematical specification of rounding that all - implementations must satisfy. - - For a real value x, canonical_round(x) is: - - floor(x * 65536 + 0.5) if fractional part of x*65536 > 0.5 - - ceil(x * 65536 - 0.5) if fractional part of x*65536 < 0.5 - - nearest even if fractional part of x*65536 == 0.5 --/ -def canonical_round (x : ℝ) : ℤ := - let scaled := x * (Q16_SCALE : ℝ) - let int_part := ⌊scaled⌋ - let frac_part := scaled - (int_part : ℝ) - if frac_part > (1 / 2 : ℝ) then int_part + 1 - else if frac_part < (1 / 2 : ℝ) then int_part - else if (int_part % 2) = 0 then int_part -- tie: round to even - else int_part + 1 - -/-- The canonical rounding produces values in the valid Q16_16 range - for inputs in [-32768, 32767.9999847412109375]. -/ -theorem canonical_round_in_range (x : ℝ) (h_min : x ≥ -32768) (h_max : x ≤ 32767.9999847412109375) : - let r := canonical_round x - r ≥ Q16_MIN_RAW ∧ r ≤ Q16_MAX_RAW := by - simp [canonical_round, Q16_MIN_RAW, Q16_MAX_RAW, Q16_SCALE] - constructor - · -- Lower bound - have h1 : ⌊x * 65536⌋ ≥ -2147483648 := by - have h2 : x * 65536 ≥ -2147483648 := by nlinarith - have h3 : (⌊x * 65536⌋ : ℝ) ≥ x * 65536 - 1 := by - exact Int.sub_one_lt_floor (x * 65536) |>.le - have h4 : (⌊x * 65536⌋ : ℝ) ≥ -2147483649 := by linarith - have h5 : ⌊x * 65536⌋ ≥ -2147483649 := by exact_mod_cast h4 - omega - split_ifs <;> omega - · -- Upper bound - have h1 : ⌊x * 65536⌋ ≤ 2147483647 := by - have h2 : x * 65536 ≤ 2147483647.9999 := by nlinarith - have h3 : (⌊x * 65536⌋ : ℝ) ≤ x * 65536 := by - exact Int.floor_le (x * 65536) - have h4 : (⌊x * 65536⌋ : ℝ) ≤ 2147483647.9999 := by linarith - have h5 : ⌊x * 65536⌋ ≤ 2147483647 := by - by_contra h6 - push_neg at h6 - have h7 : ⌊x * 65536⌋ ≥ 2147483648 := by omega - have h8 : (⌊x * 65536⌋ : ℝ) ≥ (2147483648 : ℝ) := by exact_mod_cast h7 - linarith - exact h5 - split_ifs <;> omega - -end Q16_16_Canonical diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 00000000..fea377cc --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,96 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "e5836dbb05fccdfa24ab3396d46f1f49b1f816ed", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": null, + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f3f26cc72646205ca167117487c008ee1dafe816", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "41f407a8e85b0fdc00910633a8f14754139b63f4", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "e6518a674e62de322b8f79eebeda7bcae2a36bc3", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b5b9e2bb45ce91e4bc44eaa738c3a8910404ab82", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "7a62bd13860cd39ac98da16ffc8c24d601353f69", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "125807f43a86b5d58892b7ea6972eec0d6c164d2", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "406ebb8c8e2f7e852a1b47764b42494022ce652c", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.32.0-rc1", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "SilverSight", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 00000000..382c4160 --- /dev/null +++ b/lakefile.lean @@ -0,0 +1,22 @@ +import Lake +open Lake DSL + +package «SilverSight» where + -- Settings applied to both builds and interactive editing + leanOptions := #[ + ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b` + ] + -- Add any additional package configuration options here + +@[default_target] +lean_lib «SilverSightCore» where + -- Add any library configuration options here + srcDir := "Core" + roots := #[`SilverSightCore] + +lean_lib «SilverSightFormal» where + srcDir := "formal" + roots := #[`CoreFormalism.FixedPoint] + +require mathlib from git + "https://github.com/leanprover-community/mathlib4.git" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 00000000..63f51eaf --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.32.0-rc1 \ No newline at end of file diff --git a/python/q16_canonical.py b/python/q16_canonical.py index e1b04742..26e0b07e 100644 --- a/python/q16_canonical.py +++ b/python/q16_canonical.py @@ -1,6 +1,6 @@ """Canonical Q16_16 fixed-point arithmetic. -Single source of truth: CoreFormalism/Q16_16_Spec.lean +Single source of truth: CoreFormalism/FixedPoint.lean All operations MUST produce identical results to the Lean implementation. Q16_16 represents fixed-point numbers with 16 integer bits and 16 fractional bits. diff --git a/qubo/finsler_metric.py b/qubo/finsler_metric.py index 5d92049b..4b75f583 100644 --- a/qubo/finsler_metric.py +++ b/qubo/finsler_metric.py @@ -26,7 +26,7 @@ import numpy as np # ========================================================================= -# Q16_16 Fixed-Point Constants (from CoreFormalism/Q16_16_Spec.lean) +# Q16_16 Fixed-Point Constants (from CoreFormalism/FixedPoint.lean) # ========================================================================= Q16_SCALE: int = 65536 # 2^16 -- number of subdivisions per unit diff --git a/tests/q16_roundtrip_test.py b/tests/q16_roundtrip_test.py index 6b869319..8cde8d14 100644 --- a/tests/q16_roundtrip_test.py +++ b/tests/q16_roundtrip_test.py @@ -413,7 +413,7 @@ def run_test_summary(): print(" STATUS: ALL TESTS PASSED ✓") print() print(" Q16_16 rounding is CANONICAL across Python and C.") - print(" Lean specification: CoreFormalism/Q16_16_Spec.lean") + print(" Lean specification: CoreFormalism/FixedPoint.lean") print(" Python implementation: PythonBridge/q16_canonical.py") print(" C implementation: CBride/q16_canonical.c") return 0