mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
4490dc28a7
- Move canonical FixedPoint to Core/SilverSight/FixedPoint.lean - Add SilverSightRRC library: RRC logogram gates, receipt bridge, AVM ISA - Add AVMIsa.Emit as the sole top-level JSON output boundary - Add rrc-emit-fixture executable and Python I/O shims - Update AGENTS.md, glossary, project map, and build baseline Build: 2981 jobs, 0 errors (lake build)
122 lines
No EOL
3.6 KiB
Text
122 lines
No EOL
3.6 KiB
Text
/-
|
|
BraidStrand.lean - Transport Topology with Bracket Shell
|
|
|
|
Braids carry the flow. Each strand accumulates PhaseVec contributions linearly
|
|
and carries a BraidBracket shell for local admissibility.
|
|
|
|
Hierarchy: DIAT leaf → AMMR vector → braid strand → bracket shell
|
|
-/
|
|
|
|
import CoreFormalism.DynamicCanal
|
|
import CoreFormalism.BraidBracket
|
|
import CoreFormalism.FixedPoint
|
|
open SilverSight.FixedPoint.Q16_16
|
|
|
|
set_option linter.dupNamespace false
|
|
|
|
namespace SilverSight.BraidStrand
|
|
|
|
open DynamicCanal
|
|
open SilverSight.BraidBracket
|
|
open SilverSight.FixedPoint.Q16_16
|
|
|
|
/-- BraidStrand: a single transport strand in the braid topology
|
|
|
|
zᵢ = Σₖ Φᵢₖ (linear AMMR accumulation)
|
|
Bᵢ = C(zᵢ, μᵢ) (bracket from accumulated state)
|
|
-/
|
|
structure BraidStrand where
|
|
phaseAcc : PhaseVec -- zᵢ: accumulated phase vector
|
|
parity : Bool -- strand parity for crossing orientation
|
|
slot : UInt32 -- μᵢ: transport slot / channel assignment
|
|
residue : Q16_16 -- residual from prior crossings
|
|
jitter : Q16_16 -- timing/phase jitter bound
|
|
bracket : BraidBracket -- C(zᵢ, μᵢ): admissibility shell
|
|
deriving Repr, DecidableEq, BEq
|
|
|
|
namespace BraidStrand
|
|
|
|
/-- Create a fresh strand from initial phase contribution
|
|
|
|
For DIAT leaf encoding: strand starts with single AMMR contribution.
|
|
-/
|
|
def fromLeaf (Φ : PhaseVec) (slot : UInt32) (μ : Q16_16) : BraidStrand :=
|
|
let z := Φ
|
|
{ phaseAcc := z
|
|
, parity := true
|
|
, slot := slot
|
|
, residue := Q16_16.zero
|
|
, jitter := Q16_16.zero
|
|
, bracket := BraidBracket.fromPhaseVec z μ }
|
|
|
|
/-- Update bracket after phase accumulation changes
|
|
|
|
Recompute C(z, μ) from current phaseAcc and slot.
|
|
This is the correct pattern: merge linearly, then derive bracket.
|
|
-/
|
|
def updateBracket (s : BraidStrand) : BraidStrand :=
|
|
let μ := Q16_16.ofNat s.slot.toNat
|
|
{ s with bracket := BraidBracket.fromPhaseVec s.phaseAcc μ }
|
|
|
|
/-- Add AMMR contribution to strand (linear accumulation)
|
|
|
|
Φ is the local vector contribution from a mode/carrier.
|
|
Bracket is NOT updated here — updateBracket must be called explicitly.
|
|
-/
|
|
def addContribution (s : BraidStrand) (Φ : PhaseVec) : BraidStrand :=
|
|
{ s with phaseAcc := PhaseVec.add s.phaseAcc Φ }
|
|
|
|
/-- Zero strand (identity element for merge) -/
|
|
def zero (slot : UInt32) : BraidStrand :=
|
|
let z := PhaseVec.zero
|
|
let μ := Q16_16.ofNat slot.toNat
|
|
{ phaseAcc := z
|
|
, parity := true
|
|
, slot := slot
|
|
, residue := Q16_16.zero
|
|
, jitter := Q16_16.zero
|
|
, bracket := BraidBracket.fromPhaseVec z μ }
|
|
|
|
/-- Check if strand is admissible (bracket bounds valid) -/
|
|
def isAdmissible (s : BraidStrand) : Bool :=
|
|
s.bracket.admissible && s.bracket.gapConserved
|
|
|
|
/-- Strand magnitude ‖zᵢ‖ (norm approximation) -/
|
|
def magnitude (s : BraidStrand) : Q16_16 :=
|
|
s.phaseAcc.normApprox
|
|
|
|
/-- Strand phase angle (0 if zero vector) -/
|
|
def phaseAngle (s : BraidStrand) : Q16_16 :=
|
|
s.bracket.phi
|
|
|
|
end BraidStrand
|
|
|
|
|
|
/-- Strand registry for AVMR append-only storage -/
|
|
structure StrandRegistry where
|
|
entries : List BraidStrand
|
|
nextSlot : UInt32
|
|
deriving Repr, DecidableEq
|
|
|
|
namespace StrandRegistry
|
|
|
|
def empty : StrandRegistry :=
|
|
{ entries := [], nextSlot := 0 }
|
|
|
|
def register (reg : StrandRegistry) (strand : BraidStrand) : StrandRegistry :=
|
|
{ entries := strand :: reg.entries
|
|
, nextSlot := reg.nextSlot + 1 }
|
|
|
|
def count (reg : StrandRegistry) : Nat :=
|
|
reg.entries.length
|
|
|
|
def allAdmissible (reg : StrandRegistry) : Bool :=
|
|
reg.entries.all (fun s => BraidStrand.isAdmissible s)
|
|
|
|
end StrandRegistry
|
|
|
|
|
|
#eval BraidStrand.isAdmissible (BraidStrand.zero 0)
|
|
#eval (StrandRegistry.empty.nextSlot)
|
|
|
|
end SilverSight.BraidStrand |