allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(lean): BraidDiatCodec — chirality/MMR/braid residual codec

Browse source 
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 2026-05-30 02:51:30 -05:00
parent 39047b9bc3
commit 77d67323f3
3 changed files with 436 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
0-Core-Formalism/lean/Semantics/AGENTS.md
View file

@ -83,7 +83,7 @@ lake build
- Generated `*_tb.v` and `*_test_vectors.json` files are build artifacts unless
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.
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).
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).
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
**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
View 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

46
0-Core-Formalism/lean/Semantics/Semantics/BraidField.lean
View file

@ -171,19 +171,19 @@ def latestPeak : MMR → Option IntNode
- Equal heights → merge and recurse (integrate out UV dof)
- Distinct heights → insert at front (stable at this scale)
Termination: each recursive call passes `rest`, whose size is
strictly less than `(cons top rest).size`. -/
Recursive call passes `rest`, whose size is strictly less than
`(cons top rest).size`. -/
def append (mmr : MMR) (m : Mountain) : MMR :=
match mmr with
| empty => cons m empty
| cons top rest =>
if top.height == m.height then
-- Trigger: equal heights → merge and propagate the combined peak
rest.append (Mountain.merge top m)
else
-- Stable: distinct heights → new mountain sits at front
cons m (cons top rest)
termination_by mmr.size
let rec go (mmr : MMR) (m : Mountain) : MMR :=
match mmr with
| empty => cons m empty
| cons top rest =>
if top.height == m.height then
go rest (Mountain.merge top m)
else
cons m (cons top rest)
go mmr m
termination_by mmr
/-- Stability predicate: all mountains have distinct heights.
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)
adaptation : Q16_16 -- A: bind(current_rate, optimal_rate, ratio)
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. -/
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. -/
def geometryCost (curvature : ℕ) (_ideal : ℕ) (_metric : Metric) : Q16_16 :=
@ -289,7 +298,14 @@ structure SpherionState where
mmr : MMR
voids : BettiCycleSet
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. -/
def SpherionState.init (uvScale : ℕ) : SpherionState :=