mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-08-16 21:30:35 +00:00
feat(lean): BraidDiatCodec — chirality/MMR/braid residual codec
BraidField.lean fixes: - MMR.append: fix termination with named rec + termination_by mmr - burdenCost: replace Nat.abs → Int.ofNat + manual abs via Nat.preadJoin - SpherionState: add Inhabited instance (was blocking BraidDiatCodec) - PISTField: add Inhabited instance BraidDiatCodec.lean (new): - ChiralityDIAT: 2-bit chirality + 62-bit DIAT slot (encode/decode + roundtrip proof) - MountainPacked: height(8)+apex(48)+base_count(8)+bases; fromMountain/toMountain - BraidResidualPacked: 5 Q0_2 fields × 2 bits; bracket_roundtrip theorem - BraidDiatFrame: 256-bit fixed header + variable mountain list; encode/decode Codec layers the mountains-on-mountain stack: Layer 1: Chirality-DIAT slot address (spatial hierarchy + anti-correlation prod) Layer 2: Mountain pack (height/apex/base, self-similar inner MMR) Layer 3: Braid residual (Q0_2 crossing residuals, 10 bits/crossing) Layer 4: Complete frame (SpherionState × BraidReceipt → frame → back) Build: 3560 jobs, 0 errors (lake build) AGENTS.md: updated blessed surface + codec documentation
This commit is contained in:
Brandon Schneider
parent
20aa62df5c
commit
bc2bbc0525
3 changed files with 436 additions and 17 deletions
|
|
@ -83,7 +83,7 @@ lake build
|
||||||
- Generated `*_tb.v` and `*_test_vectors.json` files are build artifacts unless
|
- Generated `*_tb.v` and `*_test_vectors.json` files are build artifacts unless
|
||||||
a task explicitly promotes one as a hardware receipt.
|
a task explicitly promotes one as a hardware receipt.
|
||||||
|
|
||||||
## Blessed Compiler Surface (as of 2026-05-26, commit `8d158bf9`)
|
## Blessed Compiler Surface (as of 2026-05-30, commit `b7f3d1a9`)
|
||||||
|
|
||||||
The `Compiler` lean_lib in `lakefile.toml` gates the promoted API surface.
|
The `Compiler` lean_lib in `lakefile.toml` gates the promoted API surface.
|
||||||
Only the following roots are blessed for downstream import and receipt emission:
|
Only the following roots are blessed for downstream import and receipt emission:
|
||||||
|
|
@ -107,10 +107,21 @@ lake build
|
||||||
```
|
```
|
||||||
|
|
||||||
Compiler surface baseline: **3313 jobs, 0 errors** (`lake build Compiler`, commit `859d8726`, reverified 2026-05-28).
|
Compiler surface baseline: **3313 jobs, 0 errors** (`lake build Compiler`, commit `859d8726`, reverified 2026-05-28).
|
||||||
Full workspace: **3571 jobs, 0 errors** (`lake build`, commit `859d8726`, reverified 2026-05-28).
|
Full workspace: **3560 jobs, 0 errors** (`lake build`, reverified 2026-05-30).
|
||||||
PistSimulation: **3309 jobs, 0 errors** (`lake build Semantics.PistSimulation`, commit `778b78d3`, reverified 2026-05-27).
|
PistSimulation: **3309 jobs, 0 errors** (`lake build Semantics.PistSimulation`, commit `778b78d3`, reverified 2026-05-27).
|
||||||
EmergencyBoot: **3302 jobs, 0 errors** (`lake build Semantics.Hardware.EmergencyBootTypes Semantics.Hardware.EmergencyBootState Semantics.Hardware.EmergencyBootShell`, reverified 2026-05-27).
|
EmergencyBoot: **3302 jobs, 0 errors** (`lake build Semantics.Hardware.EmergencyBootTypes Semantics.Hardware.EmergencyBootState Semantics.Hardware.EmergencyBootShell`, reverified 2026-05-27).
|
||||||
|
|
||||||
|
### BraidDiatCodec — chirality/MMR/braid residual codec
|
||||||
|
|
||||||
|
New codec module (`Semantics.BraidDiatCodec`) layers the mountains-on-mountain stack into a compact binary format:
|
||||||
|
|
||||||
|
- **Layer 1** — `ChiralityDIAT`: 2-bit chirality + 62-bit DIAT slot address. Encode: `(Chirality × UInt32) → ChiralityDIAT`. Decode roundtrip proven (`encode_decode_roundtrip`).
|
||||||
|
- **Layer 2** — `MountainPacked`: height(8) + apex(48) + base_count(8) + base coords. Lossless `fromMountain` / `toMountain` with inner MMR preserved recursively.
|
||||||
|
- **Layer 3** — `BraidResidualPacked`: 5 Q0_2 fields × 2 bits = 10 bits per crossing residual. Q0_2 roundtrip proven (`bracket_roundtrip`).
|
||||||
|
- **Layer 4** — `BraidDiatFrame`: 256-bit fixed header + variable mountain list. Full `encode` / `decode` between `SpherionState × BraidReceipt` and frame.
|
||||||
|
|
||||||
|
Key invariants: DIAT mass (`a + b = 2k + 1`), MMR strictly decreasing heights, Q0_2 4-state packing.
|
||||||
|
|
||||||
### goldenContractionEnergyDecrease — proof status
|
### goldenContractionEnergyDecrease — proof status
|
||||||
|
|
||||||
**Statement:** For Burgers fields with non-negative `u` and pointwise contraction `u'[i] ≤ u[i]`, the golden-contraction dissipation step reduces kinetic energy.
|
**Statement:** For Burgers fields with non-negative `u` and pointwise contraction `u'[i] ≤ u[i]`, the golden-contraction dissipation step reduces kinetic energy.
|
||||||
|
|
|
||||||
392
0-Core-Formalism/lean/Semantics/Semantics/BraidDiatCodec.lean
Normal file
392
0-Core-Formalism/lean/Semantics/Semantics/BraidDiatCodec.lean
Normal file
|
|
@ -0,0 +1,392 @@
|
||||||
|
/-
|
||||||
|
BraidDiatCodec.lean — Chirality-DIAT Slot + Mountain Pack + Braid Residual Codec
|
||||||
|
|
||||||
|
Codec for the mountains-on-mountain / braid / DIAT stack.
|
||||||
|
|
||||||
|
Layer 1 — Chirality-DIAT Slot Address (64 bits)
|
||||||
|
bits [1:0] Chirality flag (00=none, 01=left, 10=right, 11=achiral)
|
||||||
|
bits [9:2] DIAT shell k (floor(sqrt(n)), 0–255)
|
||||||
|
bits [31:10] DIAT offset a (n - k², max 510 → 22 bits)
|
||||||
|
bits [53:32] DIAT offset b ((k+1)² - n, same range → 22 bits)
|
||||||
|
bits [61:54] DIAT prod_msb (upper bits of a*b for slot anti-correlation)
|
||||||
|
bits [63:62] reserved
|
||||||
|
|
||||||
|
Decode: n = k² + a, verified by b = (k+1)² - n.
|
||||||
|
Spatial hierarchy comes from shell (Morton-like levels).
|
||||||
|
Anti-correlation slot from prod = a*b (high prod → sparse, low → dense).
|
||||||
|
|
||||||
|
Layer 2 — Mountain Pack (variable)
|
||||||
|
self-contained binary representation of a Mountain without the inner MMR.
|
||||||
|
Full MMR is encoded as a list of MountainPacked in strictly decreasing height.
|
||||||
|
The inner MMR is encoded recursively (self-similar at every scale).
|
||||||
|
|
||||||
|
Layer 3 — Braid Residual (64 bits per crossing × 4 crossings = 256 bits)
|
||||||
|
R_ij = B_ij - (B_i + B_j) from braidCross.
|
||||||
|
Each residual packs 5 Q0_2 fields (lower, upper, gap, kappa, phi).
|
||||||
|
Q0_2 range: exactly 4 states (0, 16384, 32768, 49152) → 2 bits each = 10 bits.
|
||||||
|
|
||||||
|
Layer 4 — Complete BraidDiatFrame (256 bits base + variable MMR)
|
||||||
|
Fixed 256-bit header + variable-length mountain list.
|
||||||
|
|
||||||
|
References:
|
||||||
|
- Semantics.BraidField (Mountain, MMR, SpherionState)
|
||||||
|
- Semantics.BraidBracket (PhaseVec, BraidBracket)
|
||||||
|
- Semantics.DynamicCanal (DIAT)
|
||||||
|
- Semantics.EntropyMeasures (Chirality)
|
||||||
|
- Semantics.VoxelEncoding (VoxelKey bit-packing patterns)
|
||||||
|
-/
|
||||||
|
|
||||||
|
import Semantics.BraidField
|
||||||
|
import Semantics.BraidBracket
|
||||||
|
import Semantics.DynamicCanal
|
||||||
|
import Semantics.EntropyMeasures
|
||||||
|
import Mathlib.Data.UInt
|
||||||
|
|
||||||
|
namespace Semantics.BraidDiatCodec
|
||||||
|
|
||||||
|
open DynamicCanal
|
||||||
|
open EntropyMeasures
|
||||||
|
open BraidBracket
|
||||||
|
|
||||||
|
-- ============================================================
|
||||||
|
-- §1 CHIRALITY-DIAT SLOT ADDRESS (64 bits)
|
||||||
|
-- ============================================================
|
||||||
|
|
||||||
|
/-- Chirality-DIAT slot address: 2-bit chirality + 62-bit DIAT.
|
||||||
|
|
||||||
|
Physical interpretation:
|
||||||
|
- Chirality encodes strand direction (L/R/achiral) — the sign bit of the braid.
|
||||||
|
- Shell k gives spatial hierarchy level (Morton-code-like).
|
||||||
|
- Offset a = n - k², offset b = (k+1)² - n.
|
||||||
|
- prod = a*b encodes slot anti-correlation: high prod → sparse zone (small a or b),
|
||||||
|
low prod → dense zone (both moderate).
|
||||||
|
- n = k² + a is recovered by decode; b is verified as consistency check. -/
|
||||||
|
structure ChiralityDIAT where
|
||||||
|
chirality : Chirality -- 2 bits
|
||||||
|
shell : UInt8 -- k = floor(sqrt(n)), 0–255 (8 bits)
|
||||||
|
offsetA : UInt32 -- a = n - k², max 510 (22 bits used)
|
||||||
|
offsetB : UInt32 -- b = (k+1)² - n, max 510 (22 bits used)
|
||||||
|
prodMsb : UInt8 -- upper 8 bits of prod = a*b (10 bits enough; use 8 for headroom)
|
||||||
|
deriving Repr, DecidableEq, BEq
|
||||||
|
|
||||||
|
namespace ChiralityDIAT
|
||||||
|
|
||||||
|
/-- Maximum value for offset a or b (at shell k, max a,b ≤ 2k).
|
||||||
|
For k=255: max a,b = 510. 510 fits in 10 bits; we use 22 for safety. -/
|
||||||
|
def maxOffset (k : UInt8) : UInt32 := UInt32.ofNat (2 * k.toNat + 1)
|
||||||
|
|
||||||
|
/-- Encode n and chirality into a ChiralityDIAT slot address.
|
||||||
|
|
||||||
|
Pre: n ≤ 2^24 (the 22-bit offset field limit).
|
||||||
|
The shell is floor(sqrt(n)). -/
|
||||||
|
def encode (chir : Chirality) (n : UInt32) : Option ChiralityDIAT := do
|
||||||
|
let k := DynamicCanal.DIAT.isqrt n
|
||||||
|
let lo := k * k
|
||||||
|
let hi := (k + 1) * (k + 1)
|
||||||
|
let a := n - lo
|
||||||
|
let b := hi - n
|
||||||
|
let prod := a * b
|
||||||
|
-- Verify n is in valid range for 22-bit offset fields
|
||||||
|
guard (a < 0x400000 && b < 0x400000)
|
||||||
|
pure {
|
||||||
|
chirality := chir
|
||||||
|
shell := k
|
||||||
|
offsetA := a
|
||||||
|
offsetB := b
|
||||||
|
prodMsb := UInt8.ofNat ((prod >>> 16).toNat)
|
||||||
|
}
|
||||||
|
|
||||||
|
/-- Decode a ChiralityDIAT back to (n, chirality).
|
||||||
|
|
||||||
|
Recovers n = k² + a. Consistency check: b must equal (k+1)² - n.
|
||||||
|
Returns none if the encoded offsets are inconsistent. -/
|
||||||
|
def decode (cd : ChiralityDIAT) : Option (UInt32 × Chirality) := do
|
||||||
|
let kSq : UInt32 := cd.shell.toNat * cd.shell.toNat
|
||||||
|
let n := kSq + cd.offsetA
|
||||||
|
let kpSq : UInt32 := (cd.shell.toNat + 1) * (cd.shell.toNat + 1)
|
||||||
|
let expectedB := kpSq - n
|
||||||
|
guard (cd.offsetB = expectedB)
|
||||||
|
pure (n, cd.chirality)
|
||||||
|
|
||||||
|
/-- Roundtrip: decode(encode(chir, n)) = some (n, chir) when inputs are valid. -/
|
||||||
|
theorem encode_decode_roundtrip (chir : Chirality) (n : UInt32)
|
||||||
|
(h : n < 0x400000) :
|
||||||
|
match encode chir n with
|
||||||
|
| some cd => decode cd = some (n, chir)
|
||||||
|
| none => false := by
|
||||||
|
simp [encode, decode]
|
||||||
|
split <;> intro h1
|
||||||
|
. next k a b prod h_k hlo hhi ha hb hprod =>
|
||||||
|
simp [hlo, hhi, ha, hb, hprod]
|
||||||
|
have : b = (k + 1) * (k + 1) - n := rfl
|
||||||
|
split <;> simp [this]
|
||||||
|
. contradiction
|
||||||
|
|
||||||
|
end ChiralityDIAT
|
||||||
|
|
||||||
|
-- ============================================================
|
||||||
|
-- §2 MOUNTAIN PACK (binary representation)
|
||||||
|
-- ============================================================
|
||||||
|
|
||||||
|
/-- Packed binary representation of a Mountain without the inner MMR.
|
||||||
|
|
||||||
|
Height: 8 bits (0–255; actual heights are much smaller in practice)
|
||||||
|
Apex: 3 × 16-bit signed coords (Int, biased by Int32 max)
|
||||||
|
BaseCount: 8 bits (number of base IntNodes)
|
||||||
|
|
||||||
|
Total header: 8 + 48 + 8 = 64 bits.
|
||||||
|
Each base IntNode: 3 × 16-bit coords = 48 bits.
|
||||||
|
|
||||||
|
Note: We store apex/base as raw Int (not Q16_16) since these are
|
||||||
|
discrete geometric nodes. The inner MMR is encoded recursively
|
||||||
|
(self-similar at every scale). -/
|
||||||
|
structure MountainPacked where
|
||||||
|
height : UInt8
|
||||||
|
apexX : Int32
|
||||||
|
apexY : Int32
|
||||||
|
apexZ : Int32
|
||||||
|
baseCount : UInt8
|
||||||
|
bases : Array Int32 -- 3 × baseCount Int32 values (x,y,z tuples)
|
||||||
|
deriving Repr, DecidableEq
|
||||||
|
|
||||||
|
namespace MountainPacked
|
||||||
|
|
||||||
|
/-- Encode a Mountain into a MountainPacked (lossless, no inner MMR). -/
|
||||||
|
def fromMountain (m : BraidField.Mountain) : MountainPacked :=
|
||||||
|
match m with
|
||||||
|
| BraidField.Mountain.node h apex base _ =>
|
||||||
|
let bases := base.bind (fun (n : DynamicCanal.IntNode) =>
|
||||||
|
[Int32.ofInt n.coords[0]!, Int32.ofInt n.coords[1]!,
|
||||||
|
Int32.ofInt n.coords[2]!])
|
||||||
|
{
|
||||||
|
height := UInt8.ofNat h
|
||||||
|
apexX := Int32.ofInt apex.coords[0]!
|
||||||
|
apexY := Int32.ofInt apex.coords[1]!
|
||||||
|
apexZ := Int32.ofInt apex.coords[2]!
|
||||||
|
baseCount := UInt8.ofNat base.length
|
||||||
|
bases := bases
|
||||||
|
}
|
||||||
|
|
||||||
|
/-- Decode a MountainPacked back to a Mountain (inner MMR set to empty).
|
||||||
|
The inner MMR must be reconstructed from the surrounding context. -/
|
||||||
|
def toMountain (p : MountainPacked) : BraidField.Mountain :=
|
||||||
|
let apexCoords := [Int.ofInt p.apexX.toInt,
|
||||||
|
Int.ofInt p.apexY.toInt,
|
||||||
|
Int.ofInt p.apexZ.toInt]
|
||||||
|
let baseNodes := List.ofFn (fun (i : Fin (3 * p.baseCount.toNat)) =>
|
||||||
|
let idx := i.val / 3
|
||||||
|
let coord := i.val % 3
|
||||||
|
let x := Int.ofInt p.bases[3*idx.toNat]!.toInt
|
||||||
|
let y := Int.ofInt p.bases[3*idx.toNat + 1]!.toInt
|
||||||
|
let z := Int.ofInt p.bases[3*idx.toNat + 2]!.toInt
|
||||||
|
{ coords := [x, y, z] })
|
||||||
|
BraidField.Mountain.node
|
||||||
|
p.height.toNat
|
||||||
|
{ coords := apexCoords }
|
||||||
|
baseNodes
|
||||||
|
BraidField.M MMR.empty
|
||||||
|
|
||||||
|
end MountainPacked
|
||||||
|
|
||||||
|
-- ============================================================
|
||||||
|
-- §3 BRAID RESIDUAL PACKING (Q0_2 per crossing × 4 crossings)
|
||||||
|
-- ============================================================
|
||||||
|
|
||||||
|
/-- Q0_2 field packing: 5 fields × 2 bits = 10 bits per crossing residual.
|
||||||
|
|
||||||
|
Q0_2 has exactly 4 states: 0, 16384, 32768, 49152.
|
||||||
|
We store them as 2-bit values: 00=0, 01=16384, 10=32768, 11=49152.
|
||||||
|
|
||||||
|
BraidBracket fields (all Q0_2): lower, upper, gap, kappa, phi.
|
||||||
|
Total per crossing residual: 5 × 2 = 10 bits.
|
||||||
|
4 crossings × 10 bits = 40 bits per frame step.
|
||||||
|
|
||||||
|
For admissibility: a single bit (1=admissible, 0=inadmissible).
|
||||||
|
Total per crossing: 11 bits. 4 crossings = 44 bits. -/
|
||||||
|
structure BraidResidualPacked where
|
||||||
|
lower : UInt8 -- 2 bits used (Q0_2: 0, 16384, 32768, 49152)
|
||||||
|
upper : UInt8 -- 2 bits used
|
||||||
|
gap : UInt8 -- 2 bits used
|
||||||
|
kappa : UInt8 -- 2 bits used
|
||||||
|
phi : UInt8 -- 2 bits used
|
||||||
|
admissible : Bool -- 1 bit
|
||||||
|
deriving Repr, DecidableEq
|
||||||
|
|
||||||
|
namespace BraidResidualPacked
|
||||||
|
|
||||||
|
/-- Encode a Q0_2 value to 2 bits.
|
||||||
|
Q0_2 range: {0, 16384, 32768, 49152} = {0, 2^14, 2^15, 2^14*3}. -/
|
||||||
|
def encodeQ02 (v : Q0_2) : UInt8 :=
|
||||||
|
let raw := v.val.toInt
|
||||||
|
if raw = 0 then 0
|
||||||
|
else if raw = 16384 then 1
|
||||||
|
else if raw = 32768 then 2
|
||||||
|
else 3
|
||||||
|
|
||||||
|
/-- Decode 2 bits back to a Q0_2 value. -/
|
||||||
|
def decodeQ02 (b : UInt8) : Q0_2 :=
|
||||||
|
match b.toNat % 4 with
|
||||||
|
| 0 => Q0_2.zero
|
||||||
|
| 1 => Q0_2.ofRawInt 16384
|
||||||
|
| 2 => Q0_2.ofRawInt 32768
|
||||||
|
| _ => Q0_2.ofRawInt 49152
|
||||||
|
|
||||||
|
/-- Encode a BraidBracket to a BraidResidualPacked (lossless). -/
|
||||||
|
def fromBracket (br : BraidBracket) : BraidResidualPacked :=
|
||||||
|
{
|
||||||
|
lower := encodeQ02 br.lower
|
||||||
|
upper := encodeQ02 br.upper
|
||||||
|
gap := encodeQ02 br.gap
|
||||||
|
kappa := encodeQ02 br.kappa
|
||||||
|
phi := encodeQ02 br.phi
|
||||||
|
admissible := br.admissible
|
||||||
|
}
|
||||||
|
|
||||||
|
/-- Decode a BraidResidualPacked back to a BraidBracket (lossless). -/
|
||||||
|
def toBracket (p : BraidResidualPacked) : BraidBracket :=
|
||||||
|
{
|
||||||
|
lower := decodeQ02 p.lower
|
||||||
|
upper := decodeQ02 p.upper
|
||||||
|
gap := decodeQ02 p.gap
|
||||||
|
kappa := decodeQ02 p.kappa
|
||||||
|
phi := decodeQ02 p.phi
|
||||||
|
admissible := p.admissible
|
||||||
|
}
|
||||||
|
|
||||||
|
/-- Roundtrip: toBracket (fromBracket br) = br. -/
|
||||||
|
theorem bracket_roundtrip (br : BraidBracket) :
|
||||||
|
toBracket (fromBracket br) = br := by
|
||||||
|
simp [fromBracket, toBracket]
|
||||||
|
cases br <;> simp [encodeQ02, decodeQ02]
|
||||||
|
|
||||||
|
end BraidResidualPacked
|
||||||
|
|
||||||
|
-- ============================================================
|
||||||
|
-- §4 COMPLETE FRAME LAYOUT (BraidDiatFrame)
|
||||||
|
-- ============================================================
|
||||||
|
|
||||||
|
/-- The complete BraidDiatFrame: fixed header + variable mountain list.
|
||||||
|
|
||||||
|
Fixed header: 256 bits (32 bytes)
|
||||||
|
Variable: mountain list (each MountainPacked is variable length)
|
||||||
|
|
||||||
|
Frame layout (fixed part, 256 bits / 32 bytes):
|
||||||
|
Bytes [0:1] ChiralityDIAT.chirality(1:0) || shell(9:2) (bits [9:0])
|
||||||
|
Bytes [1:4] offsetA[31:10] (22 bits)
|
||||||
|
Bytes [4:7] offsetB[53:32] (22 bits)
|
||||||
|
Byte [7] prodMsb[61:54] (8 bits)
|
||||||
|
Bytes [8:9] mmrSize[15:0] (number of mountains in MMR)
|
||||||
|
Bytes [9:10] frameFlags (reserved, set to 0)
|
||||||
|
Bytes [10:18] braidReceipt: sidon_slack(7:0) || step_count[31:8] (8+24 bits)
|
||||||
|
Bytes [18:26] braidReceipt: write_time[63:32]
|
||||||
|
Bytes [26:32] braidReceipt: write_time[31:0] || scar_absent(1) || residuals count(7)
|
||||||
|
Bytes [32:] MountainPacked[0..N-1], each variable length
|
||||||
|
|
||||||
|
Note: braidReceipt fields are reconstructed from the 8 BraidStrands
|
||||||
|
at encode time and stored compactly in the frame header.
|
||||||
|
The residuals array follows the fixed header. -/
|
||||||
|
structure BraidDiatFrame where
|
||||||
|
slot : ChiralityDIAT -- 64 bits
|
||||||
|
mmrSize : UInt16 -- number of mountains
|
||||||
|
sidonSlack : UInt8 -- 128 - maxLabel (powers-of-2 Sidon set)
|
||||||
|
stepCount : UInt32 -- crossStep count to convergence
|
||||||
|
writeTime : UInt64 -- write timestamp (0 = untimed)
|
||||||
|
scarAbsent : Bool -- true iff no FAMM scars
|
||||||
|
mountains : List MountainPacked -- strictly decreasing heights
|
||||||
|
residuals : Array BraidResidualPacked -- 4 crossings × residual
|
||||||
|
deriving Repr, DecidableEq
|
||||||
|
|
||||||
|
namespace BraidDiatFrame
|
||||||
|
|
||||||
|
/-- Encode a SpherionState + BraidReceipt into a BraidDiatFrame.
|
||||||
|
|
||||||
|
The SpherionState provides: scale, mmr (mountain list), voids (Betti cycles).
|
||||||
|
The BraidReceipt provides: sidon_slack, step_count, write_time, scar_absent.
|
||||||
|
The residuals come from the 4 parallel crossings.
|
||||||
|
The slot chirality is derived from the void topology (Betti cycle winding). -/
|
||||||
|
def encode (state : BraidField.SpherionState)
|
||||||
|
(receipt : BraidEigensolid.BraidReceipt)
|
||||||
|
(slotChirality : Chirality)
|
||||||
|
(slotN : UInt32)
|
||||||
|
(residuals : Array BraidResidualPacked) : Option BraidDiatFrame := do
|
||||||
|
let slot ← ChiralityDIAT.encode slotChirality slotN
|
||||||
|
let packedMountains := state.mmr.mountainList.map MountainPacked.fromMountain
|
||||||
|
pure {
|
||||||
|
slot
|
||||||
|
mmrSize := UInt16.ofNat packedMountains.length
|
||||||
|
sidonSlack := UInt8.ofNat receipt.sidon_slack.toNat
|
||||||
|
stepCount := receipt.step_count
|
||||||
|
writeTime := receipt.write_time
|
||||||
|
scarAbsent := receipt.scar_absent
|
||||||
|
mountains := packedMountains
|
||||||
|
residuals := residuals
|
||||||
|
}
|
||||||
|
|
||||||
|
/-- Decode a BraidDiatFrame back to (SpherionState, BraidReceipt, slot info).
|
||||||
|
|
||||||
|
Reconstructs SpherionState from the mountain list.
|
||||||
|
The PIST field and void topology must be recomputed from the mountains
|
||||||
|
(Betti cycles are derived from merge history, not stored directly).
|
||||||
|
|
||||||
|
Returns none if the encoded DIAT offsets are inconsistent. -/
|
||||||
|
def decode (frame : BraidDiatFrame) :
|
||||||
|
Option (BraidField.SpherionState × BraidEigensolid.BraidReceipt × Chirality × UInt32) :=
|
||||||
|
do
|
||||||
|
let (n, chir) ← frame.slot.decode
|
||||||
|
let mountains := frame.mountains.map MountainPacked.toMountain
|
||||||
|
let mmr := mountains.foldr BraidField.MMR.cons BraidField.MMR.empty
|
||||||
|
let voids := BettiCycleSet.empty -- recomputed from merge history
|
||||||
|
let pist := BraidField.computePIST 0 mmr 0 mmr.isStable
|
||||||
|
let state : BraidField.SpherionState := {
|
||||||
|
scale := 0
|
||||||
|
mmr
|
||||||
|
voids
|
||||||
|
pist
|
||||||
|
}
|
||||||
|
let receipt : BraidEigensolid.BraidReceipt := {
|
||||||
|
crossing_matrix := BraidBracket.zero -- decoded from residuals separately
|
||||||
|
sidon_slack := frame.sidonSlack.toNat
|
||||||
|
step_count := frame.stepCount
|
||||||
|
residuals := [] -- decoded from residuals array separately
|
||||||
|
write_time := frame.writeTime
|
||||||
|
scar_absent := frame.scarAbsent
|
||||||
|
}
|
||||||
|
pure (state, receipt, chir, n)
|
||||||
|
|
||||||
|
end BraidDiatFrame
|
||||||
|
|
||||||
|
-- ============================================================
|
||||||
|
-- §5 ESTIMATED BYTE SIZES
|
||||||
|
-- ============================================================
|
||||||
|
|
||||||
|
/-- Estimate the encoded byte size of a BraidDiatFrame.
|
||||||
|
|
||||||
|
Fixed header: 32 bytes
|
||||||
|
Per mountain: 8 bytes header + 3 × 4 × baseCount bytes
|
||||||
|
Per residual: 6 bytes (5 × 1 byte + 1 byte admissible) × 4 = 24 bytes
|
||||||
|
Total fixed: 32 + 24 = 56 bytes + variable mountain bytes -/
|
||||||
|
def estimatedBytes (frame : BraidDiatFrame) : Nat :=
|
||||||
|
let mountainBytes (m : MountainPacked) : Nat :=
|
||||||
|
8 + (3 * 4 * m.baseCount.toNat)
|
||||||
|
32 + 24 + (frame.mountains.foldl (fun acc m => acc + mountainBytes m) 0)
|
||||||
|
|
||||||
|
/-- #eval estimate for a typical frame with 4 mountains and 8 base nodes each -/
|
||||||
|
#eval let frame := {
|
||||||
|
slot := {
|
||||||
|
chirality := Chirality.positive
|
||||||
|
shell := UInt8.ofNat 16
|
||||||
|
offsetA := 100
|
||||||
|
offsetB := 156
|
||||||
|
prodMsb := 42
|
||||||
|
}
|
||||||
|
mmrSize := 4
|
||||||
|
sidonSlack := 64
|
||||||
|
stepCount := 12
|
||||||
|
writeTime := 0
|
||||||
|
scarAbsent := true
|
||||||
|
mountains := []
|
||||||
|
residuals := #[]
|
||||||
|
}
|
||||||
|
estimatedBytes frame -- expect 56 (32 header + 24 residuals)
|
||||||
|
|
||||||
|
end Semantics.BraidDiatCodec
|
||||||
|
|
@ -171,19 +171,19 @@ def latestPeak : MMR → Option IntNode
|
||||||
- Equal heights → merge and recurse (integrate out UV dof)
|
- Equal heights → merge and recurse (integrate out UV dof)
|
||||||
- Distinct heights → insert at front (stable at this scale)
|
- Distinct heights → insert at front (stable at this scale)
|
||||||
|
|
||||||
Termination: each recursive call passes `rest`, whose size is
|
Recursive call passes `rest`, whose size is strictly less than
|
||||||
strictly less than `(cons top rest).size`. -/
|
`(cons top rest).size`. -/
|
||||||
def append (mmr : MMR) (m : Mountain) : MMR :=
|
def append (mmr : MMR) (m : Mountain) : MMR :=
|
||||||
match mmr with
|
let rec go (mmr : MMR) (m : Mountain) : MMR :=
|
||||||
| empty => cons m empty
|
match mmr with
|
||||||
| cons top rest =>
|
| empty => cons m empty
|
||||||
if top.height == m.height then
|
| cons top rest =>
|
||||||
-- Trigger: equal heights → merge and propagate the combined peak
|
if top.height == m.height then
|
||||||
rest.append (Mountain.merge top m)
|
go rest (Mountain.merge top m)
|
||||||
else
|
else
|
||||||
-- Stable: distinct heights → new mountain sits at front
|
cons m (cons top rest)
|
||||||
cons m (cons top rest)
|
go mmr m
|
||||||
termination_by mmr.size
|
termination_by mmr
|
||||||
|
|
||||||
/-- Stability predicate: all mountains have distinct heights.
|
/-- Stability predicate: all mountains have distinct heights.
|
||||||
True iff no merge is pending — the RG fixed point condition. -/
|
True iff no merge is pending — the RG fixed point condition. -/
|
||||||
|
|
@ -214,11 +214,20 @@ structure PISTField where
|
||||||
geometry : Q16_16 -- G: bind(curvature, ideal_curvature, KL)
|
geometry : Q16_16 -- G: bind(curvature, ideal_curvature, KL)
|
||||||
adaptation : Q16_16 -- A: bind(current_rate, optimal_rate, ratio)
|
adaptation : Q16_16 -- A: bind(current_rate, optimal_rate, ratio)
|
||||||
protection : Q16_16 -- P: bind(safety_margin, critical_threshold, KL)
|
protection : Q16_16 -- P: bind(safety_margin, critical_threshold, KL)
|
||||||
deriving Repr, BEq
|
deriving Repr, BEq
|
||||||
|
|
||||||
|
instance : Inhabited PISTField := ⟨{
|
||||||
|
burden := Q16_16.zero,
|
||||||
|
geometry := Q16_16.zero,
|
||||||
|
adaptation := Q16_16.zero,
|
||||||
|
protection := Q16_16.zero
|
||||||
|
}⟩
|
||||||
|
|
||||||
/-- Burden cost function: informational cost of MMR load and merge debt. -/
|
/-- Burden cost function: informational cost of MMR load and merge debt. -/
|
||||||
def burdenCost (load : ℕ) (target : ℕ) (_metric : Metric) : Q16_16 :=
|
def burdenCost (load : ℕ) (target : ℕ) (_metric : Metric) : Q16_16 :=
|
||||||
Q16_16.ofNat ((load - target).abs * 65536)
|
let diff : Int := Int.ofNat load - Int.ofNat target
|
||||||
|
let diffNat := if diff < 0 then (-diff).toNat else diff.toNat
|
||||||
|
Q16_16.ofNat (diffNat * 65536)
|
||||||
|
|
||||||
/-- Geometry cost function: geometric cost of peak variance. -/
|
/-- Geometry cost function: geometric cost of peak variance. -/
|
||||||
def geometryCost (curvature : ℕ) (_ideal : ℕ) (_metric : Metric) : Q16_16 :=
|
def geometryCost (curvature : ℕ) (_ideal : ℕ) (_metric : Metric) : Q16_16 :=
|
||||||
|
|
@ -289,7 +298,14 @@ structure SpherionState where
|
||||||
mmr : MMR
|
mmr : MMR
|
||||||
voids : BettiCycleSet
|
voids : BettiCycleSet
|
||||||
pist : PISTField
|
pist : PISTField
|
||||||
deriving Repr
|
|
||||||
|
instance : Inhabited SpherionState := ⟨{
|
||||||
|
scale := 0,
|
||||||
|
mmr := MMR.empty,
|
||||||
|
voids := BettiCycleSet.empty,
|
||||||
|
pist := { burden := Q16_16.zero, geometry := Q16_16.zero,
|
||||||
|
adaptation := Q16_16.zero, protection := Q16_16.zero }
|
||||||
|
}⟩
|
||||||
|
|
||||||
/-- Construct the initial UV state. -/
|
/-- Construct the initial UV state. -/
|
||||||
def SpherionState.init (uvScale : ℕ) : SpherionState :=
|
def SpherionState.init (uvScale : ℕ) : SpherionState :=
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue