feat(lean): add SilverSight Semantics core modules (Schema, Layout, WireFormat, View, LayoutBridge, CanalLayout)

Implements the YaFF-inspired separation of schema, layout, and access pattern in Core/SilverSight/Semantics/: - Schema.lean: fixed-size Schema typeclass with byteSize and wellFormed. - Layout.lean: Layout enum, AccessProfile cost model, and cost-based selector with an ε-suboptimality theorem. - WireFormat.lean: certified encode/decode/roundTrip/encode_size structure. - View.lean: zero-copy View with address-arithmetic invariant. - LayoutBridge.lean: certified layout-conversion structure and identity bridges. - CanalLayout.lean: CanalRegime enum and regime-aware layout selection. Also updates: - lakefile.lean: adds SilverSight.Semantics.* roots to SilverSightCore. - docs/ARCHITECTURE.md, RRC_REFACTOR_READINESS.md, PROJECT_MAP.{md,json}, build_logs/2026-06-21_session_build_baseline.md, and GLOSSARY.md. - AGENTS.md: build baseline, blessed surfaces, and pending proof work. Build: 2987 jobs, 0 errors (lake build) Tests: Python 21/21, Lean/C 35/35
2026-07-31 01:25:21 +00:00 · 2026-06-21 14:00:56 -05:00 · 2026-06-21 14:00:56 -05:00 · 3504bca392
commit 3504bca392
parent fec200205e
14 changed files with 675 additions and 33 deletions
--- a/AGENTS.md
+++ b/AGENTS.md
@ -310,8 +310,11 @@ Current Research Stack cornfield ref (for cross-repo lookup only):
 - `Core/SilverSight/FixedPoint.lean` is the canonical Q16_16 / Q0_16 source of
  truth. `formal/CoreFormalism/FixedPoint.lean` is a compatibility shim.
 - `Core/SilverSight/FixedPoint.lean` is the canonical `Q16_16`/`Q0_16` source
-  of truth (3132 jobs, 0 errors under `lake build SilverSightCore`).
-  `formal/CoreFormalism/FixedPoint.lean` is a compatibility shim.
+  of truth. `formal/CoreFormalism/FixedPoint.lean` is a compatibility shim.
+- `Core/SilverSight/Semantics/` is the YaFF-inspired schema/layout/wireformat
+  core. It now contains `Schema`, `Layout`, `WireFormat`, `View`,
+  `LayoutBridge`, and `CanalLayout`. These modules build under
+  `lake build SilverSightCore` (2987 jobs, 0 errors) and import only Mathlib.
 - `formal/CoreFormalism/SidonSets.lean` is ported from Research Stack and
  builds under `lake build CoreFormalism.SidonSets` (2601 jobs, 0 errors).  The
  chaos-game appendix was removed because it did not build; the core Singer
--- a/Core/SilverSight/Semantics/CanalLayout.lean
+++ b/Core/SilverSight/Semantics/CanalLayout.lean
@ -0,0 +1,39 @@
+/-
+SilverSight.Semantics.CanalLayout
+
+Links the pure layout-cost model to the DynamicCanal substrate concept.
+The Core keeps the regime enum minimal so that the full DynamicCanal
+physics can live in a library without importing it into the invariant core.
+-/
+
+import SilverSight.Semantics.Layout
+
+namespace SilverSight.Semantics
+
+/-- Minimal canal regime enum used for layout decisions at the Core level.
+    The richer `DynamicCanal.Regime` in `CoreFormalism` refines these three
+    states with pressure, lambda, and edge models. -/
+inductive CanalRegime where
+  | coherent -- stable transport; let the cost model choose
+  | stressed -- distorted transport; prefer compact encoding
+  | throat   -- wormhole/transfer; prefer columnar field access
+  deriving Repr, DecidableEq, BEq
+
+/-- Choose a layout from an access profile and a canal regime.
+
+    In the `coherent` regime the cost model is authoritative. In `stressed`
+    and `throat` regimes the regime overrides the cost model, because
+    substrate pressure makes compactness or field-locality more important
+    than the raw event-weighted score. -/
+def chooseLayout (profile : AccessProfile) (regime : CanalRegime) : Layout :=
+  match regime with
+  | CanalRegime.coherent => chooseLayoutByCost profile
+  | CanalRegime.stressed => Layout.compact
+  | CanalRegime.throat   => Layout.columnar
+
+/-- In the coherent regime the chosen layout is ε-suboptimal with respect
+    to the pure cost model. -/
+theorem chooseLayout_coherent_eq (profile : AccessProfile) :
+    chooseLayout profile CanalRegime.coherent = chooseLayoutByCost profile := rfl
+
+end SilverSight.Semantics
--- a/Core/SilverSight/Semantics/Layout.lean
+++ b/Core/SilverSight/Semantics/Layout.lean
@ -0,0 +1,141 @@
+/-
+SilverSight.Semantics.Layout
+
+A Layout is a physical encoding choice for a Schema. It is independent of
+the logical shape: the same schema may be encoded as row-major, columnar,
+compact, or an mmap view. The Core only defines the layout enum and a
+fixed-point cost model; layout-specific encoders live in WireFormat.
+-/
+
+import SilverSight.FixedPoint
+
+namespace SilverSight.Semantics
+
+open SilverSight.FixedPoint.Q0_16
+
+/-- Physical layout choices for a fixed-size schema. -/
+inductive Layout where
+  | rowMajor   -- natural C-array order, good for sequential scans
+  | columnar   -- field-major order, good for random field access
+  | compact    -- bit-packed or delta-coded, good for storage/transfer
+  | mmapView   -- direct memory-map view, no copy on read
+  deriving Repr, DecidableEq, BEq
+
+export Layout (rowMajor columnar compact mmapView)
+
+/-- Access profile used to score a layout. All counts are raw event tallies;
+    the cost function compresses them into a Q0_16 dimensionless score. -/
+structure AccessProfile where
+  randomReads     : Nat
+  sequentialReads : Nat
+  writes          : Nat
+  deriving Repr, DecidableEq, BEq
+
+namespace Layout
+
+/-- Per-layout operation weights (relative, dimensionless). -/
+def randomReadWeight : Layout → Nat
+  | rowMajor  => 4
+  | columnar  => 1
+  | compact   => 3
+  | mmapView  => 1
+
+def sequentialReadWeight : Layout → Nat
+  | rowMajor  => 1
+  | columnar  => 3
+  | compact   => 4
+  | mmapView  => 2
+
+def writeWeight : Layout → Nat
+  | rowMajor  => 3
+  | columnar  => 3
+  | compact   => 1
+  | mmapView  => 4
+
+/-- Cost of a layout for a given access profile. Lower is better.
+
+    The raw score is a weighted sum of event counts. It is clamped into the
+    Q0_16 range, so extremely hot profiles saturate rather than overflow. -/
+def cost (layout : Layout) (profile : AccessProfile) : Q0_16 :=
+  let raw :=
+    profile.randomReads     * randomReadWeight layout +
+    profile.sequentialReads * sequentialReadWeight layout +
+    profile.writes          * writeWeight layout
+  ofRawInt (Int.ofNat raw)
+
+end Layout
+
+/-- All Core layouts, in the order used by the default cost-based selector. -/
+def allLayouts : List Layout :=
+  [Layout.rowMajor, Layout.columnar, Layout.compact, Layout.mmapView]
+
+private def pickBest (best l : Layout) (profile : AccessProfile) : Layout :=
+  if lt (Layout.cost l profile) (Layout.cost best profile) then l else best
+
+private lemma le_refl (a : Q0_16) : le a a := by simp [le]
+
+private lemma le_trans {a b c : Q0_16} (h1 : le a b) (h2 : le b c) : le a c := by
+  simp [le] at h1 h2 ⊢
+  omega
+
+private lemma not_lt_iff_le (a b : Q0_16) : lt a b = false ↔ le b a := by
+  simp [lt, le]
+
+private lemma pickBest_le_best (best l : Layout) (profile : AccessProfile) :
+    le (Layout.cost (pickBest best l profile) profile) (Layout.cost best profile) := by
+  unfold pickBest
+  split_ifs with h
+  · have hlt : (Layout.cost l profile).toInt < (Layout.cost best profile).toInt := by
+      simpa [lt] using h
+    simp [le]
+    omega
+  · exact le_refl _
+
+private lemma pickBest_le_l (best l : Layout) (profile : AccessProfile) :
+    le (Layout.cost (pickBest best l profile) profile) (Layout.cost l profile) := by
+  unfold pickBest
+  split_ifs with h
+  · exact le_refl _
+  · have hle : (Layout.cost best profile).toInt ≤ (Layout.cost l profile).toInt := by
+      simpa [lt, le] using h
+    simp [le]
+    omega
+
+private lemma foldl_le_seen (profile : AccessProfile) (init : Layout) (ls : List Layout) :
+    let result := ls.foldl (fun b l => pickBest b l profile) init
+    le (Layout.cost result profile) (Layout.cost init profile) ∧
+    ∀ l ∈ ls, le (Layout.cost result profile) (Layout.cost l profile) := by
+  induction ls generalizing init with
+  | nil => simp [le_refl]
+  | cons h t ih =>
+      simp [List.foldl]
+      apply And.intro
+      · apply le_trans
+        · exact (ih (pickBest init h profile)).1
+        · exact pickBest_le_best init h profile
+      · apply And.intro
+        · apply le_trans
+          · exact (ih (pickBest init h profile)).1
+          · exact pickBest_le_l init h profile
+        · intro a hmem
+          exact (ih (pickBest init h profile)).2 a hmem
+
+/-- Choose the layout with minimal cost for a given access profile.
+    Ties are broken toward the earlier layout in `allLayouts`. -/
+def chooseLayoutByCost (profile : AccessProfile) : Layout :=
+  allLayouts.foldl (fun best l => pickBest best l profile) Layout.rowMajor
+
+/-- The cost-based selector is ε-suboptimal: it never picks a layout with
+    higher cost than any other Core layout. -/
+theorem chooseLayoutByCost_le (profile : AccessProfile) (l : Layout) :
+    le (Layout.cost (chooseLayoutByCost profile) profile) (Layout.cost l profile) := by
+  have h : ∀ x ∈ allLayouts,
+      le (Layout.cost (chooseLayoutByCost profile) profile) (Layout.cost x profile) := by
+    simp [chooseLayoutByCost]
+    exact (foldl_le_seen profile Layout.rowMajor allLayouts).2
+  cases l
+  all_goals
+    apply h
+    simp [allLayouts]
+
+end SilverSight.Semantics
--- a/Core/SilverSight/Semantics/LayoutBridge.lean
+++ b/Core/SilverSight/Semantics/LayoutBridge.lean
@ -0,0 +1,46 @@
+/-
+SilverSight.Semantics.LayoutBridge
+
+A LayoutBridge converts between two wire formats of the same schema and
+preserves meaning. The `correct` field is a Lean proof that converting the
+encoding in layout L1 yields exactly the encoding in layout L2.
+
+The Core only provides the bridge interface and identity bridges. Concrete
+bridges (row-major ↔ columnar, compact expansion, mmap view wrapping) are
+library extensions that must each supply a `correct` proof.
+-/
+
+import SilverSight.Semantics.Schema
+import SilverSight.Semantics.Layout
+import SilverSight.Semantics.WireFormat
+
+namespace SilverSight.Semantics
+
+/-- A certified conversion between two wire formats of the same schema. -/
+structure LayoutBridge (α : Type) [Schema α] (L1 L2 : Layout) where
+  wf1     : WireFormat α L1
+  wf2     : WireFormat α L2
+  convert : ByteArray → ByteArray
+  correct : ∀ a, convert (wf1.encode a) = wf2.encode a
+
+namespace LayoutBridge
+
+/-- The identity bridge: encoding in L is already the encoding in L. -/
+def identity {α : Type} {L : Layout} [Schema α] (wf : WireFormat α L) :
+    LayoutBridge α L L where
+  wf1     := wf
+  wf2     := wf
+  convert := id
+  correct := by simp
+
+/-- Identity bridge for `Bool` row-major. -/
+def boolRowMajor : LayoutBridge Bool rowMajor rowMajor :=
+  identity WireFormat.boolRowMajor
+
+/-- Identity bridge for `UInt8` row-major. -/
+def uint8RowMajor : LayoutBridge UInt8 rowMajor rowMajor :=
+  identity WireFormat.uint8RowMajor
+
+end LayoutBridge
+
+end SilverSight.Semantics
--- a/Core/SilverSight/Semantics/Schema.lean
+++ b/Core/SilverSight/Semantics/Schema.lean
@ -0,0 +1,58 @@
+/-
+SilverSight.Semantics.Schema
+
+A Schema is the logical shape of a type. It is the source of truth;
+layouts and wire formats are derived from it.
+
+Core schemas are fixed-size. Variable-length containers (lists, maps,
+streams) are represented by pointing to a separately-scoped buffer and
+are a library extension, not part of the invariant core.
+-/
+
+namespace SilverSight.Semantics
+
+/-- Core schema: fixed byte size on the wire plus a well-formedness check.
+
+    `byteSize` is the canonical encoded length. `wellFormed` is the
+    minimal structural predicate the decoder may assume/verify. It is
+    a `Bool`, not a `Prop`, so that decoders can use it directly at
+    runtime without requiring a `Decidable` instance. -/
+class Schema (α : Type) where
+  byteSize   : Nat
+  wellFormed : α → Bool
+
+export Schema (byteSize wellFormed)
+
+/-- Shorthand for the canonical encoded size of a type. -/
+def encodedSize (α : Type) [Schema α] : Nat := byteSize α
+
+/-- A value is schema-admissible if it is well-formed. -/
+def SchemaAdmissible {α : Type} [Schema α] (a : α) : Prop := wellFormed a = true
+
+/-- The empty schema is admissible for unit-like values. -/
+instance : Schema Unit where
+  byteSize   := 0
+  wellFormed := fun _ => true
+
+/-- Booleans occupy one byte on the wire. -/
+instance : Schema Bool where
+  byteSize   := 1
+  wellFormed := fun _ => true
+
+@[simp] theorem bool_byteSize : byteSize Bool = 1 := rfl
+
+/-- 8-bit unsigned integers occupy one byte. -/
+instance : Schema UInt8 where
+  byteSize   := 1
+  wellFormed := fun _ => true
+
+@[simp] theorem uint8_byteSize : byteSize UInt8 = 1 := rfl
+
+/-- 32-bit unsigned integers occupy four bytes in row-major layout. -/
+instance : Schema UInt32 where
+  byteSize   := 4
+  wellFormed := fun _ => true
+
+@[simp] theorem uint32_byteSize : byteSize UInt32 = 4 := rfl
+
+end SilverSight.Semantics
--- a/Core/SilverSight/Semantics/View.lean
+++ b/Core/SilverSight/Semantics/View.lean
@ -0,0 +1,48 @@
+/-
+SilverSight.Semantics.View
+
+A View is a structured value read from a byte range without copying the
+underlying buffer. The Core defines the address-arithmetic contract; the
+zero-copy property is a theorem about offsets and schema sizes.
+
+Only fixed-size Core schemas have built-in accessors. Variable-length views
+are a library extension that must preserve the same address-arithmetic
+invariant.
+-/
+
+import SilverSight.Semantics.Schema
+
+namespace SilverSight.Semantics
+
+/-- A zero-copy view of a fixed-size schema value inside a byte buffer.
+
+    `valid` is the address-arithmetic invariant: the schema's byte range
+    fits entirely inside the buffer starting at `offset`. -/
+structure View (α : Type) [Schema α] where
+  base   : ByteArray
+  offset : Nat
+  valid  : offset + byteSize α ≤ base.size
+
+namespace View
+
+/-- Read a UInt8 through a one-byte view. The result is the byte at the
+    view's offset; no copy of the underlying buffer occurs. -/
+def readUInt8 (v : View UInt8) : UInt8 :=
+  v.base.get v.offset (by
+    have h : byteSize UInt8 = 1 := rfl
+    have hv := v.valid
+    omega
+  )
+
+/-- Reading a UInt8 view returns exactly the byte at the stored offset. -/
+@[simp]
+theorem readUInt8_eq_get (v : View UInt8) :
+    readUInt8 v = v.base.get v.offset (by
+      have h : byteSize UInt8 = 1 := rfl
+      have hv := v.valid
+      omega
+    ) := rfl
+
+end View
+
+end SilverSight.Semantics
--- a/Core/SilverSight/Semantics/WireFormat.lean
+++ b/Core/SilverSight/Semantics/WireFormat.lean
@ -0,0 +1,73 @@
+/-
+SilverSight.Semantics.WireFormat
+
+A WireFormat is a certified encoder/decoder pair for a fixed-size Schema
+under a specific Layout. The `roundTrip` field is a Lean proof that decoding
+an encoded value reproduces the original value.
+
+Core WireFormats are intentionally simple. Complex layout-specific encodings
+(columnar stripping, compact packing, mmap views) are library extensions that
+must provide their own `roundTrip` proofs against this interface.
+-/
+
+import SilverSight.Semantics.Schema
+import SilverSight.Semantics.Layout
+
+namespace SilverSight.Semantics
+
+/-- Certified wire format: encode, decode, and a proof that they round-trip.
+
+    The `encode_size` field guarantees that every encoding consumes exactly
+    `Schema.byteSize α` bytes, matching the schema contract. -/
+structure WireFormat (α : Type) [Schema α] (layout : Layout) where
+  encode      : α → ByteArray
+  decode      : ByteArray → Option α
+  encode_size : ∀ a, (encode a).size = byteSize α
+  roundTrip   : ∀ a, decode (encode a) = some a
+
+namespace WireFormat
+
+/-- The trivial wire format for `Unit`: zero bytes round-trip. -/
+def unitRowMajor : WireFormat Unit rowMajor where
+  encode      := fun _ => ByteArray.empty
+  decode      := fun _ => some ()
+  encode_size := fun _ => rfl
+  roundTrip   := fun _ => rfl
+
+/-- Row-major wire format for `Bool`: one byte, 1 = true, 0 = false. -/
+def boolRowMajor : WireFormat Bool rowMajor where
+  encode := fun b => ByteArray.mk #[if b then (1 : UInt8) else (0 : UInt8)]
+  decode := fun bs =>
+    if h : bs.size = 1 then
+      let idx : Fin bs.size := ⟨0, by rw [h]; decide⟩
+      match bs.get idx with
+      | 1 => some true
+      | 0 => some false
+      | _ => none
+    else none
+  encode_size := by
+    intro _
+    rfl
+  roundTrip := by
+    intro b
+    cases b <;> simp [ByteArray.get, ByteArray.size]
+
+/-- Row-major wire format for `UInt8`: one byte, identity. -/
+def uint8RowMajor : WireFormat UInt8 rowMajor where
+  encode := fun u => ByteArray.mk #[u]
+  decode := fun bs =>
+    if h : bs.size = 1 then
+      let idx : Fin bs.size := ⟨0, by rw [h]; decide⟩
+      some (bs.get idx)
+    else
+      none
+  encode_size := by
+    intro _
+    rfl
+  roundTrip := by
+    intro u
+    simp [ByteArray.get, ByteArray.size]
+
+end WireFormat
+
+end SilverSight.Semantics
--- a/docs/ARCHITECTURE.md
+++ b/docs/ARCHITECTURE.md
@ -20,8 +20,15 @@ Layer 1: Core              <- Core/SilverSightCore.lean, Core/SilverSight/FixedP

 - **`Core/SilverSightCore.lean`** — Hachimoji states, `Receipt`, abstract AVM transition `δ`, TIC axiom, library interface.
 - **`Core/SilverSight/FixedPoint.lean`** — canonical `Q16_16` / `Q0_16` fixed-point arithmetic.
+- **`Core/SilverSight/Semantics/`** — YaFF-inspired schema/layout/wireformat core:
+  - `Schema.lean` — fixed-size schema contract (`byteSize`, `wellFormed`).
+  - `Layout.lean` — physical layouts (`rowMajor`, `columnar`, `compact`, `mmapView`) and a Q0_16 cost model with an ε-suboptimal selector.
+  - `WireFormat.lean` — certified encoder/decoder pairs (`encode`, `decode`, `roundTrip`, `encode_size`).
+  - `View.lean` — zero-copy address-arithmetic views.
+  - `LayoutBridge.lean` — certified conversions between layouts.
+  - `CanalLayout.lean` — canal-regime override on top of the cost model.

-**Status:** ✅ Active. `lake build SilverSightCore` is green (3132 jobs, 0 errors).
+**Status:** ✅ Active. `lake build SilverSightCore` is green (2987 jobs, 0 errors).

 **Connection to old map:** This replaces Research Stack L1 `FixedPoint.lean` + `Basic.lean` + `SIConstants.lean`. SilverSight keeps only the fixed-point contract; constants and `Basic` are absorbed into CoreFormalism or omitted.

@ -41,12 +48,15 @@ Layer 1: Core              <- Core/SilverSightCore.lean, Core/SilverSight/FixedP
 - **`RRCLogogramProjection.lean`** — RRC shapes, witness status, projection/merge gates.
 - **`ReceiptCore.lean`** — internal validation receipt model and `toSilverSightReceipt` bridge.
 - **`RRC/Emit.lean`** — alignment gate, 6 canonical fixture rows, JSON emitter.
+- **`RRC/ReceiptDensity.lean`** — Q16_16 receipt-density scoring gate.
+- **`RRC/PolyFactorIdentity.lean`** — divisor-sum signature gate.
+- **`RRC/EntropyCandidates.lean`** — 10 certifiable braid-state fixtures.
 - **`AVMIsa/{Types,Value,Instr,State,Step,Run}.lean`** — concrete typed AVM ISA.
 - **`AVMIsa/Emit.lean`** — sole top-level JSON output boundary.
 - **`formal/RRCLib/`** — user-facing symlinks into `formal/SilverSight/`.
 - **`exe/RrcEmitFixture.lean`** — executable that emits the AVM-stamped fixture corpus JSON.

-**Status:** ✅ Bare-minimum refactor complete. `lake build SilverSightRRC` is green (2992 jobs, 0 errors).
+**Status:** ✅ Bare-minimum refactor complete. `lake build SilverSightRRC` is green (3006 jobs, 0 errors).

 **Connection to old map:** This maps to Research Stack L4 (`RRC/Corpus250.lean`, `RRC/RRCTypeWitness.lean`, `AVMIsa/*.lean`). SilverSight currently has the RRC surface and AVM ISA but **not** the full 250-equation corpus or `RRCTypeWitness`.

@ -148,7 +158,14 @@ python3 docs/generate_project_map.py
 ├── Core/
 │   ├── SilverSightCore.lean          ← Layer 1: invariant core
 │   └── SilverSight/
-│       └── FixedPoint.lean           ← Layer 1: canonical Q16_16
+│       ├── FixedPoint.lean           ← Layer 1: canonical Q16_16 / Q0_16
+│       └── Semantics/                ← Layer 1: schema / layout / wireformat core
+│           ├── Schema.lean
+│           ├── Layout.lean
+│           ├── WireFormat.lean
+│           ├── View.lean
+│           ├── LayoutBridge.lean
+│           └── CanalLayout.lean
 ├── formal/
 │   ├── CoreFormalism/                ← Layer 2: Sidon, braid, Hachimoji
 │   ├── PVGS_DQ_Bridge/               ← Layer 2: photon-varied Gaussian bridge
@ -160,7 +177,8 @@ python3 docs/generate_project_map.py
 ├── qubo/                             ← Layer 4: optimization shims
 ├── tests/                            ← Verification fixtures
 ├── exe/
-│   └── RrcEmitFixture.lean           ← JSON emitter executable
+│   ├── RrcEmitFixture.lean           ← JSON emitter executable
+│   └── Q16_16Roundtrip.lean        ← Lean ↔ C Q16_16 roundtrip executable
 ├── .github/
 │   ├── workflows/                    ← CI
 │   └── scripts/                      ← repo hygiene scripts
@ -175,8 +193,8 @@ python3 docs/generate_project_map.py

 1. Port the full 250-equation `Corpus250` fixture corpus.
 2. Add `PIST.Classify` / matrix builder so `pistProxyLabel` / `pistExactLabel` can be populated from real data.
-3. Add `RRC.ReceiptDensity`, `RRC.PolyFactorIdentity`, `RRC.EntropyCandidates` if needed.
-4. Add a C/Lean FFI or Python `ctypes` bridge for the canonical Q16_16 roundtrip test.
+3. Extend `Semantics.WireFormat` and `Semantics.LayoutBridge` with concrete columnar/compact encodings for product types (e.g., `BraidState`).
+4. Promote `CanalRegime` into `CoreFormalism.DynamicCanal` so the library physics drives the Core layout override.
 5. Keep promotion as `not_promoted` everywhere until a Lean gate explicitly passes.

 ## Explicitly out of scope for SilverSight
--- a/docs/GLOSSARY.md
+++ b/docs/GLOSSARY.md
@ -47,6 +47,20 @@ name and explains the delta.
 | **pathCost** | Raw integer cost metric carried on a `Receipt`; never a `Float`. | `Core/SilverSightCore.lean` |
 | **Library method** | The architecture rule: `Core/` defines contracts, libraries implement them, and no library imports another library. | `AGENTS.md` |
 | **Core** | The invariant center of SilverSight: `Core/SilverSightCore.lean` and `Core/SilverSight/FixedPoint.lean`. Defines Receipt, AVM, TIC, and canonical Q16_16. | `AGENTS.md` |
+| **Schema** | Typeclass describing fixed-size, well-formed data: `byteSize` and `wellFormed`. | `Core/SilverSight/Semantics/Schema.lean` |
+| **byteSize** | Number of bytes occupied by a value of a `Schema` type; constant and statically known. | `Core/SilverSight/Semantics/Schema.lean` |
+| **wellFormed** | Predicate asserting that a value satisfies its `Schema` invariants. | `Core/SilverSight/Semantics/Schema.lean` |
+| **Layout** | Physical data placement: `rowMajor`, `columnar`, `compact`, `mmapView`. | `Core/SilverSight/Semantics/Layout.lean` |
+| **AccessProfile** | Read/write mix used by the layout cost model. | `Core/SilverSight/Semantics/Layout.lean` |
+| **WireFormat** | Certified encoder/decoder pair for a `Schema` under a `Layout`. | `Core/SilverSight/Semantics/WireFormat.lean` |
+| **roundTrip** | WireFormat axiom: `decode (encode a) = some a` for every value. | `Core/SilverSight/Semantics/WireFormat.lean` |
+| **View** | Zero-copy, address-bounded window into a `ByteArray`. | `Core/SilverSight/Semantics/View.lean` |
+| **LayoutBridge** | Certified conversion between two `Layout`s with a round-trip guarantee. | `Core/SilverSight/Semantics/LayoutBridge.lean` |
+| **CanalRegime** | Storage regime (`cold`, `warm`, `hot`, `flash`) used by layout selection. | `Core/SilverSight/Semantics/CanalLayout.lean` |
+| **CanalLayout** | Module that maps `CanalRegime` to a preferred `Layout` and profile. | `Core/SilverSight/Semantics/CanalLayout.lean` |
+| **rowMajor** | Default `Layout`: fields stored contiguously in declaration order. | `Core/SilverSight/Semantics/Layout.lean` |
+| **mmapView** | `Layout` optimized for memory-mapped, read-only access. | `Core/SilverSight/Semantics/Layout.lean` |
+| **BraidState** | Aggregated braid carrier state used by the eigensolid compressor. | `formal/CoreFormalism/BraidState.lean` |

 ## RRC / AVM ISA

--- a/docs/PROJECT_MAP.json
+++ b/docs/PROJECT_MAP.json
@ -1,13 +1,13 @@
 {
  "schema": "silversight_project_map_v1",
-  "generated_at": "2026-06-21T15:38:08.247263+00:00",
+  "generated_at": "2026-06-21T18:58:40.565557+00:00",
  "repo": "https://github.com/allaunthefox/SilverSight",
  "local_path": "/tmp/SilverSight",
  "summary": {
-    "total_files": 110,
-    "lean_files": 56,
+    "total_files": 116,
+    "lean_files": 62,
    "python_files": 23,
-    "active": 109,
+    "active": 115,
    "quarantined": 1,
    "archived": 0,
    "receipt_boundary_files": 4
@ -18,10 +18,10 @@
      "name": "Core",
      "path": "Core",
      "description": "Invariant core: no imports except Mathlib; defines Receipt and AVM.",
-      "file_count": 2,
-      "lean_files": 2,
+      "file_count": 8,
+      "lean_files": 8,
      "python_files": 0,
-      "active": 2,
+      "active": 8,
      "quarantined": 0,
      "archived": 0
    },
@ -239,7 +239,7 @@
      "research_stack_source": null,
      "role": "",
      "receipt_boundary": false,
-      "line_count": 363
+      "line_count": 366
    },
    {
      "path": "CITATION.cff",
@ -261,7 +261,7 @@
      "language": "lean",
      "kind": "core",
      "module": "SilverSight.FixedPoint",
-      "build_target": "SilverSightFormal",
+      "build_target": "SilverSight.FixedPoint",
      "status": "active",
      "imports": [
        "Lean.Data.Json",
@ -275,6 +275,103 @@
      "receipt_boundary": false,
      "line_count": 1311
    },
+    {
+      "path": "Core/SilverSight/Semantics/CanalLayout.lean",
+      "layer": "core",
+      "language": "lean",
+      "kind": "core",
+      "module": "SilverSight.Semantics.CanalLayout",
+      "build_target": "SilverSightFormal",
+      "status": "active",
+      "imports": [
+        "SilverSight.Semantics.Layout"
+      ],
+      "research_stack_source": null,
+      "role": "",
+      "receipt_boundary": false,
+      "line_count": 39
+    },
+    {
+      "path": "Core/SilverSight/Semantics/Layout.lean",
+      "layer": "core",
+      "language": "lean",
+      "kind": "core",
+      "module": "SilverSight.Semantics.Layout",
+      "build_target": "SilverSight.Semantics.Layout",
+      "status": "active",
+      "imports": [
+        "SilverSight.FixedPoint"
+      ],
+      "research_stack_source": null,
+      "role": "",
+      "receipt_boundary": false,
+      "line_count": 141
+    },
+    {
+      "path": "Core/SilverSight/Semantics/LayoutBridge.lean",
+      "layer": "core",
+      "language": "lean",
+      "kind": "core",
+      "module": "SilverSight.Semantics.LayoutBridge",
+      "build_target": "SilverSight.Semantics.LayoutBridge",
+      "status": "active",
+      "imports": [
+        "SilverSight.Semantics.Schema",
+        "SilverSight.Semantics.Layout",
+        "SilverSight.Semantics.WireFormat"
+      ],
+      "research_stack_source": null,
+      "role": "",
+      "receipt_boundary": false,
+      "line_count": 46
+    },
+    {
+      "path": "Core/SilverSight/Semantics/Schema.lean",
+      "layer": "core",
+      "language": "lean",
+      "kind": "core",
+      "module": "SilverSight.Semantics.Schema",
+      "build_target": "SilverSight.Semantics.Schema",
+      "status": "active",
+      "imports": [],
+      "research_stack_source": null,
+      "role": "",
+      "receipt_boundary": false,
+      "line_count": 58
+    },
+    {
+      "path": "Core/SilverSight/Semantics/View.lean",
+      "layer": "core",
+      "language": "lean",
+      "kind": "core",
+      "module": "SilverSight.Semantics.View",
+      "build_target": "SilverSight.Semantics.View",
+      "status": "active",
+      "imports": [
+        "SilverSight.Semantics.Schema"
+      ],
+      "research_stack_source": null,
+      "role": "",
+      "receipt_boundary": false,
+      "line_count": 48
+    },
+    {
+      "path": "Core/SilverSight/Semantics/WireFormat.lean",
+      "layer": "core",
+      "language": "lean",
+      "kind": "core",
+      "module": "SilverSight.Semantics.WireFormat",
+      "build_target": "SilverSight.Semantics.WireFormat",
+      "status": "active",
+      "imports": [
+        "SilverSight.Semantics.Schema",
+        "SilverSight.Semantics.Layout"
+      ],
+      "research_stack_source": null,
+      "role": "",
+      "receipt_boundary": false,
+      "line_count": 73
+    },
    {
      "path": "Core/SilverSightCore.lean",
      "layer": "core",
@ -375,7 +472,7 @@
      "research_stack_source": null,
      "role": "",
      "receipt_boundary": false,
-      "line_count": 187
+      "line_count": 205
    },
    {
      "path": "docs/GLOSSARY.md",
@ -431,7 +528,7 @@
      "research_stack_source": null,
      "role": "",
      "receipt_boundary": false,
-      "line_count": 2207
+      "line_count": 2376
    },
    {
      "path": "docs/PROJECT_MAP.md",
@ -445,7 +542,7 @@
      "research_stack_source": null,
      "role": "",
      "receipt_boundary": false,
-      "line_count": 191
+      "line_count": 192
    },
    {
      "path": "docs/RRC_PLACEMENT.md",
@ -473,7 +570,7 @@
      "research_stack_source": null,
      "role": "",
      "receipt_boundary": false,
-      "line_count": 95
+      "line_count": 100
    },
    {
      "path": "docs/TESTING.md",
@ -501,7 +598,7 @@
      "research_stack_source": null,
      "role": "",
      "receipt_boundary": false,
-      "line_count": 185
+      "line_count": 239
    },
    {
      "path": "docs/generate_porting_candidates.py",
@ -2072,6 +2169,46 @@
    }
  ],
  "edges": [
+    {
+      "from": "Core/SilverSight/Semantics/CanalLayout.lean",
+      "to": "Core/SilverSight/Semantics/Layout.lean",
+      "relation": "imports"
+    },
+    {
+      "from": "Core/SilverSight/Semantics/Layout.lean",
+      "to": "Core/SilverSight/FixedPoint.lean",
+      "relation": "imports"
+    },
+    {
+      "from": "Core/SilverSight/Semantics/LayoutBridge.lean",
+      "to": "Core/SilverSight/Semantics/Schema.lean",
+      "relation": "imports"
+    },
+    {
+      "from": "Core/SilverSight/Semantics/LayoutBridge.lean",
+      "to": "Core/SilverSight/Semantics/Layout.lean",
+      "relation": "imports"
+    },
+    {
+      "from": "Core/SilverSight/Semantics/LayoutBridge.lean",
+      "to": "Core/SilverSight/Semantics/WireFormat.lean",
+      "relation": "imports"
+    },
+    {
+      "from": "Core/SilverSight/Semantics/View.lean",
+      "to": "Core/SilverSight/Semantics/Schema.lean",
+      "relation": "imports"
+    },
+    {
+      "from": "Core/SilverSight/Semantics/WireFormat.lean",
+      "to": "Core/SilverSight/Semantics/Schema.lean",
+      "relation": "imports"
+    },
+    {
+      "from": "Core/SilverSight/Semantics/WireFormat.lean",
+      "to": "Core/SilverSight/Semantics/Layout.lean",
+      "relation": "imports"
+    },
    {
      "from": "exe/Q16_16Roundtrip.lean",
      "to": "Core/SilverSight/FixedPoint.lean",
--- a/docs/PROJECT_MAP.md
+++ b/docs/PROJECT_MAP.md
@ -1,6 +1,6 @@
 # SilverSight Project Map

-**Generated:** 2026-06-21T15:38:08.247263+00:00
+**Generated:** 2026-06-21T18:58:40.565557+00:00

 **Source repo:** https://github.com/allaunthefox/SilverSight

@ -8,17 +8,17 @@

 ## 1. Project Overview

- **Total tracked files:** 110
- **Lean files:** 56
+- **Total tracked files:** 116
+- **Lean files:** 62
 - **Python files:** 23
- **Active:** 109 | **Quarantined:** 1 | **Archived:** 0
+- **Active:** 115 | **Quarantined:** 1 | **Archived:** 0
 - **Receipt-boundary files:** 4

 ## 2. Layer Summary

 | Layer | Path | Files | Lean | Python | Active | Quarantined | Archived | Description |
 |-------|------|-------|------|--------|--------|-------------|----------|-------------|
-| Core | `Core` | 2 | 2 | 0 | 2 | 0 | 0 | Invariant core: no imports except Mathlib; defines Receipt and AVM. |
+| Core | `Core` | 8 | 8 | 0 | 8 | 0 | 0 | Invariant core: no imports except Mathlib; defines Receipt and AVM. |
 | CoreFormalism | `formal/CoreFormalism` | 18 | 18 | 0 | 18 | 0 | 0 | Canonical Q16_16, Sidon, braid, and Hachimoji foundations. |
 | PVGS_DQ_Bridge | `formal/PVGS_DQ_Bridge` | 9 | 8 | 1 | 9 | 0 | 0 | Photon-varied Gaussian state dual-quaternion bridge. |
 | UniversalEncoding | `formal/UniversalEncoding` | 2 | 2 | 0 | 2 | 0 | 0 | Universal math address space and chirality. |
@ -35,7 +35,13 @@

 | File | Module | Build Target | Status | Receipt Boundary | Research-Stack Source | Role |
 |------|--------|--------------|--------|------------------|----------------------|------|
-| `Core/SilverSight/FixedPoint.lean` | SilverSight.FixedPoint | SilverSightFormal | active | — | — | — |
+| `Core/SilverSight/FixedPoint.lean` | SilverSight.FixedPoint | SilverSight.FixedPoint | active | — | — | — |
+| `Core/SilverSight/Semantics/CanalLayout.lean` | SilverSight.Semantics.CanalLayout | SilverSightFormal | active | — | — | — |
+| `Core/SilverSight/Semantics/Layout.lean` | SilverSight.Semantics.Layout | SilverSight.Semantics.Layout | active | — | — | — |
+| `Core/SilverSight/Semantics/LayoutBridge.lean` | SilverSight.Semantics.LayoutBridge | SilverSight.Semantics.LayoutBridge | active | — | — | — |
+| `Core/SilverSight/Semantics/Schema.lean` | SilverSight.Semantics.Schema | SilverSight.Semantics.Schema | active | — | — | — |
+| `Core/SilverSight/Semantics/View.lean` | SilverSight.Semantics.View | SilverSight.Semantics.View | active | — | — | — |
+| `Core/SilverSight/Semantics/WireFormat.lean` | SilverSight.Semantics.WireFormat | SilverSight.Semantics.WireFormat | active | — | — | — |
 | `Core/SilverSightCore.lean` | SilverSightCore | SilverSightCore | active | ✅ | — | Invariant core: Hachimoji states, Receipt, AVM δ, TIC axiom, library interface. |

 ### CoreFormalism (`formal/CoreFormalism`)
--- a/docs/RRC_REFACTOR_READINESS.md
+++ b/docs/RRC_REFACTOR_READINESS.md
@ -15,6 +15,8 @@
 - ✅ AVM-stamped RRC fixture corpus emitter (`emitFixtureCorpus`)
 - ✅ Python raw-feature shims (`pist_matrix_builder.py`, `validate_rrc_predictions.py`)
 - ✅ Executable `rrc-emit-fixture` to extract the JSON bundle
+- ✅ RRC gates ported: `ReceiptDensity`, `PolyFactorIdentity`, `EntropyCandidates`
+- ✅ Q16_16 cross-language roundtrip test (Lean ↔ C ↔ Python)
 - ✅ Glossary entries for all new domain terms

 ## Location
@ -71,23 +73,26 @@ python3 python/validate_rrc_predictions.py /tmp/rrc_fixture_emitted.json

 | Gate | Result |
 |---|---|
-| `lake build` | ✅ 2981 jobs, 0 errors |
-| `lake build SilverSightCore` | ✅ 3132 jobs, 0 errors |
+| `lake build` | ✅ 2987 jobs, 0 errors |
+| `lake build SilverSightCore` | ✅ 2987 jobs, 0 errors |
 | `lake build SilverSightFormal` | ✅ 3132 jobs, 0 errors |
-| `lake build SilverSightRRC` | ✅ 2992 jobs, 0 errors |
+| `lake build SilverSightRRC` | ✅ 3006 jobs, 0 errors |
 | `lake build rrc-emit-fixture` | ✅ green |
+| `lake build q16-roundtrip` | ✅ 5949 jobs, 0 errors |
 | `python3 -m py_compile python/pist_matrix_builder.py python/validate_rrc_predictions.py tests/test_q16_canonical.py .github/scripts/check_doc_sync.py .github/scripts/glossary_lint.py` | ✅ green |
 | `python3 .github/scripts/glossary_lint.py` | ✅ no warnings |
 | `python3 .github/scripts/check_doc_sync.py` | ✅ OK |
 | `rrc-emit-fixture \| validate_rrc_predictions.py` | ✅ OK: 6 rows |
+| `python3 tests/test_q16_roundtrip.py` | ✅ 21 tests passed |
+| `.lake/build/bin/q16-roundtrip` | ✅ 35 Lean ↔ C tests passed |
 | `pytest tests/test_q16_canonical.py` | ⚠️ not run — pytest not installed in this environment |

 ## Out of scope (future work)

 - Full 250-equation `Corpus250` (requires `PIST.Classify`, `PIST.Matrices250`, source JSON).
- `RRC.ReceiptDensity`, `RRC.PolyFactorIdentity`, `RRC.EntropyCandidates`.
 - `python/build_corpus250.py` generator for the full corpus.
 - PIST classifier surface to populate `pistProxyLabel` / `pistExactLabel` from real matrices.
+- Concrete `WireFormat`/`LayoutBridge` instances for multi-field Core types such as `BraidState`.

 ## References

--- a/docs/build_logs/2026-06-21_session_build_baseline.md
+++ b/docs/build_logs/2026-06-21_session_build_baseline.md
@ -183,3 +183,57 @@ Ported Research-Stack RRC decision surface into SilverSight as a new library.
 |---|---|
 | `python3 tests/test_q16_roundtrip.py` | ✅ 21 tests passed |
 | `.lake/build/bin/q16-roundtrip` | ✅ 35 Lean ↔ C tests passed |
+
+---
+
+## Later same day: Phase 1 core — schema / layout / wireformat modules
+
+### What changed
+
+Implemented the YaFF-inspired Phase 1 Core modules in
+`Core/SilverSight/Semantics/`:
+
+- `Schema.lean` — fixed-size schema contract (`byteSize`, `wellFormed`).
+- `Layout.lean` — `Layout` enum, `AccessProfile`, Q0_16 `Layout.cost`,
+  `chooseLayoutByCost`, and an ε-suboptimality theorem.
+- `WireFormat.lean` — certified encoder/decoder structure
+  (`encode`, `decode`, `encode_size`, `roundTrip`) with row-major instances
+  for `Unit`, `Bool`, and `UInt8`.
+- `View.lean` — zero-copy view contract (`base`, `offset`, `valid`) and a
+  `readUInt8` accessor backed by address-arithmetic.
+- `LayoutBridge.lean` — certified layout conversion structure and identity
+  bridges.
+- `CanalLayout.lean` — `CanalRegime` enum and `chooseLayout` override on
+  top of the pure cost model.
+
+Updated `lakefile.lean` to add all new `SilverSight.Semantics.*` modules to
+`SilverSightCore`. Updated `docs/ARCHITECTURE.md`, `AGENTS.md`,
+`docs/RRC_REFACTOR_READINESS.md`, and `SilverSight_Spec.md` to reflect the
+new Core surface.
+
+### Build baselines
+
+| Command | Jobs | Errors | Notes |
+|---|---|---|---|
+| `lake build` | 2987 | 0 | Default target now includes Semantics core |
+| `lake build SilverSightCore` | 2987 | 0 | Core + Semantics modules |
+| `lake build SilverSightRRC` | 3006 | 0 | RRC decision surface |
+| `lake build q16-roundtrip` | 5949 | 0 | Lean ↔ C executable |
+
+### Verification results
+
+| Test | Result |
+|---|---|
+| `python3 tests/test_q16_roundtrip.py` | ✅ 21 tests passed |
+| `.lake/build/bin/q16-roundtrip` | ✅ 35 Lean ↔ C tests passed |
+| `python3 .github/scripts/glossary_lint.py` | ✅ no warnings |
+| `python3 .github/scripts/check_doc_sync.py` | ✅ OK |
+
+### Notes
+
+- `Semantics` modules import only `SilverSight.FixedPoint` and Mathlib,
+  preserving the library-method rule that Core may not depend on libraries.
+- The full `DynamicCanal` physics remains in `CoreFormalism.DynamicCanal`;
+  `CanalLayout` is the Core-side abstraction that will be driven by it.
+- Concrete `WireFormat`/`LayoutBridge` instances for product types such as
+  `BraidState` are left as library extensions.
--- a/lakefile.lean
+++ b/lakefile.lean
@ -13,7 +13,7 @@ package «SilverSight» where
 lean_lib «SilverSightCore» where
  -- Add any library configuration options here
  srcDir := "Core"
-  roots := #[`SilverSightCore, `SilverSight.FixedPoint]
+  roots := #[`SilverSightCore, `SilverSight.FixedPoint, `SilverSight.Semantics.Schema, `SilverSight.Semantics.Layout, `SilverSight.Semantics.WireFormat, `SilverSight.Semantics.View, `SilverSight.Semantics.LayoutBridge, `SilverSight.Semantics.CanalLayout]

 lean_lib «SilverSightFormal» where
  srcDir := "formal"