Track EigenGate dependency slice

0-Core-Formalism/lean/Semantics/Semantics/Core/FoldedPointManifold.lean

@@ -0,0 +1,409 @@
+/-
+FoldedPointManifold.lean — apparent 0D footprint with higher-dimensional interior
+
+This module makes explicit the frame distinction:
+
+  observer-resolved dimension = 0
+  internal/folded dimension   may be > 0
+
+That prevents the model from treating "0D" as automatically empty. A point may
+be an observer-frame footprint of folded higher-dimensional structure, but the
+claim is admitted only when neutral closure, replay, bounded dimensionality, and
+torsional potential are declared.
+
+The stronger loopback claim is separate: when the observer frame has lost all
+resolution at apparent 0D, a declared 16D interior may become a permeable return
+surface only if the permeability witness is present.
+
+Permeability is not free leakage. It is conservation-preserving porosity: every
+dimensional level that participates in the loopback must carry the same
+accounting value.
+-/
+
+import Semantics.FixedPoint
+
+namespace Semantics.FoldedPointManifold
+
+open Semantics.FixedPoint
+
+/-- Terminal gate for a folded-point claim. -/
+inductive FoldDecision where
+  | admit
+  | hold
+  | reject
+  deriving Repr, BEq, DecidableEq
+
+/-- Terminal gate for the 0D -> 16D loopback/permeability claim. -/
+inductive LoopbackDecision where
+  | loopback
+  | hold
+  | reject
+  deriving Repr, BEq, DecidableEq
+
+/-- Terminal gate for conservation across the dimensional ladder. -/
+inductive ConservationDecision where
+  | conserved
+  | hold
+  | reject
+  deriving Repr, BEq, DecidableEq
+
+/-- Minimal folded-point event.
+
+`resolvedDim = 0` means the observer frame sees no extension.
+`internalDim > 0` means the event carries folded interior degrees of freedom.
+`neutralClosure` links the claim back to U0 accounting.
+`torsionPotential` is normalized Q0.16 expression potential.
+`permeabilityDeclared` is the extra witness for the stronger loopback claim.
+-/
+structure FoldedPointEvent where
+  resolvedDim : Nat
+  internalDim : Nat
+  apparentPoint : Bool
+  neutralClosure : Bool
+  replayReceiptPresent : Bool
+  torsionPotential : Q0_16
+  permeabilityDeclared : Bool
+  deriving Repr, BEq, DecidableEq
+
+/-- A folded point is a point only in the observer frame. -/
+def isFoldedPoint (e : FoldedPointEvent) : Bool :=
+  e.apparentPoint && e.resolvedDim == 0 && e.internalDim > 0
+
+/-- Current model cap: the folded interior may be up to the declared 16D
+manifold, but not an unbounded free variable. -/
+def withinDeclaredDimensionalCap (e : FoldedPointEvent) : Bool :=
+  e.internalDim <= 16
+
+/-- There must be nonzero torsional potential to unfold. -/
+def hasTorsionPotential (e : FoldedPointEvent) : Bool :=
+  e.torsionPotential.val != 0
+
+/-- The observer frame has lost all spatial resolution at the footprint. -/
+def resolutionLost (e : FoldedPointEvent) : Bool :=
+  e.apparentPoint && e.resolvedDim == 0
+
+/-- A folded point is admissible only when the apparent point, internal
+dimensional witness, neutral closure, replay, cap, and torsion potential close.
+Missing replay/neutrality/capacity routes to HOLD if the event is at least a
+folded-point candidate. Non-folded points reject the folded-space claim. -/
+def decideFoldedPoint (e : FoldedPointEvent) : FoldDecision :=
+  if isFoldedPoint e then
+    if withinDeclaredDimensionalCap e &&
+       e.neutralClosure &&
+       e.replayReceiptPresent &&
+       hasTorsionPotential e then
+      .admit
+    else
+      .hold
+  else
+    .reject
+
+/-- The stronger cyclic claim: after apparent 0D, a declared 16D interior can
+be treated as a permeable return surface only when the separate permeability
+witness is present. -/
+def decideLoopback (e : FoldedPointEvent) : LoopbackDecision :=
+  if resolutionLost e then
+    if e.internalDim == 16 &&
+       e.permeabilityDeclared &&
+       e.neutralClosure &&
+       e.replayReceiptPresent &&
+       hasTorsionPotential e then
+      .loopback
+    else
+      .hold
+  else
+    .reject
+
+/-- Conservation witness across the compressed 0D seed, carrier path, generator,
+projection surface, and 16D expression space.
+
+`mengerZeroSeed` marks the 0D boundary as a porous/fractal conservation limit,
+not an empty point. The values are abstract accounting charges/loads, not
+physical mass claims.
+-/
+structure DimensionalConservation where
+  level0 : Int
+  level1 : Int
+  level4 : Int
+  level3 : Int
+  level16 : Int
+  mengerZeroSeed : Bool
+  replayReceiptPresent : Bool
+  deriving Repr, BEq, DecidableEq
+
+/-- Conservation means every declared dimensional level carries the same
+accounting value. -/
+def conservedAcrossLevels (c : DimensionalConservation) : Bool :=
+  c.level0 == c.level1 &&
+  c.level1 == c.level4 &&
+  c.level4 == c.level3 &&
+  c.level3 == c.level16
+
+/-- The Menger-style 0D seed only admits conservation when replay is present.
+Broken conservation rejects. A missing porous seed or replay is HOLD. -/
+def decideConservation (c : DimensionalConservation) : ConservationDecision :=
+  if conservedAcrossLevels c then
+    if c.mengerZeroSeed && c.replayReceiptPresent then .conserved
+    else .hold
+  else
+    .reject
+
+/-- Canonical fixture: observer sees 0D, interior declares 16D, closure and
+replay are present, and torsional potential can unfold. -/
+def folded16Fixture : FoldedPointEvent :=
+  { resolvedDim := 0
+  , internalDim := 16
+  , apparentPoint := true
+  , neutralClosure := true
+  , replayReceiptPresent := true
+  , torsionPotential := Q0_16.half
+  , permeabilityDeclared := true }
+
+/-- Same folded candidate, but no replay receipt: HOLD, not ADMIT. -/
+def missingReplayFixture : FoldedPointEvent :=
+  { folded16Fixture with replayReceiptPresent := false }
+
+/-- Same observer point, but internal dimensionality exceeds the declared cap:
+HOLD until a new cap/law is declared. -/
+def overCapFixture : FoldedPointEvent :=
+  { folded16Fixture with internalDim := 17 }
+
+/-- An ordinary 0D point with no internal dimension rejects a folded-space
+claim. -/
+def ordinaryPointFixture : FoldedPointEvent :=
+  { folded16Fixture with internalDim := 0 }
+
+/-- Folded and neutral, but no permeability witness: HOLD for loopback. -/
+def noPermeabilityFixture : FoldedPointEvent :=
+  { folded16Fixture with permeabilityDeclared := false }
+
+/-- Menger-style 0D seed preserves the same accounting value across every
+declared dimensional level. -/
+def mengerConservedFixture : DimensionalConservation :=
+  { level0 := 3
+  , level1 := 3
+  , level4 := 3
+  , level3 := 3
+  , level16 := 3
+  , mengerZeroSeed := true
+  , replayReceiptPresent := true }
+
+def brokenConservationFixture : DimensionalConservation :=
+  { mengerConservedFixture with level16 := 4 }
+
+def missingMengerSeedFixture : DimensionalConservation :=
+  { mengerConservedFixture with mengerZeroSeed := false }
+
+/-! ## Gate Algebra for Total Interaction
+
+The total interaction is a pair `I_total(s) = (Γ(s), ΔR(s))`.
+
+`Γ(s)` is the ordered tensor product of individual gate outcomes.
+The order is: REJECT > HOLD > ADMIT.
+
+`ΔR(s)` is the resolution delta: shortcut gain plus shell error recovery
+minus projected error.
+-/
+
+/-- Ordered gate outcomes for the tensor product.
+    REJECT > HOLD > ADMIT - this ordering ensures that a single
+    rejection dominates, and a single hold blocks admission. -/
+inductive GateOutcome where
+  | reject
+  | hold
+  | admit
+  deriving Repr, BEq, DecidableEq
+
+/-- Ordered tensor product (⊗) of gate outcomes.
+    If any gate rejects, the product rejects.
+    If any gate holds (and none reject), the product holds.
+    Only if all gates admit does the product admit. -/
+def gateCompose (g1 g2 : GateOutcome) : GateOutcome :=
+  match g1 with
+  | .reject => .reject
+  | .hold   => match g2 with | .reject => .reject | _ => .hold
+  | .admit  => g2
+
+/-- The tensor product extends to a list of gates. -/
+def gateComposeList (gs : List GateOutcome) : GateOutcome :=
+  gs.foldl gateCompose .admit
+
+/-- Resolution delta components for the 0D→16D throat shortcut. -/
+structure ResolutionDelta where
+  manifoldDistance : Int  -- D_m: full manifold traversal distance
+  throatDistance   : Int  -- D_t: shortcut throat distance
+  shellError       : Int  -- E_s: recoverable shell baseline error
+  projectedError   : Int  -- E_p: new residual from the projection
+  deriving Repr, BEq, DecidableEq
+
+/-- Compute the net resolution change.
+    Positive = improvement (throat saves more than projection costs).
+    Zero = break-even.
+    Negative = decreased resolution. -/
+def deltaResolution (r : ResolutionDelta) : Int :=
+  (r.manifoldDistance - r.throatDistance) + r.shellError - r.projectedError
+
+/-- Final interaction outcome after applying the decision law. -/
+inductive InteractionOutcome where
+  | improved    -- Γ = ADMIT and ΔR > 0
+  | unchanged   -- Γ = ADMIT and ΔR = 0
+  | decreased   -- Γ = ADMIT and ΔR < 0
+  | hold        -- Γ = HOLD
+  | reject      -- Γ = REJECT
+  deriving Repr, BEq, DecidableEq
+
+/-- The total interaction pair: (gate tensor, resolution delta). -/
+structure TotalInteraction where
+  gateTensor : GateOutcome
+  deltaR     : ResolutionDelta
+  deriving Repr
+
+/-- Apply the decision law to the total interaction pair.
+    If Γ = REJECT → REJECT
+    If Γ = HOLD    → HOLD
+    If Γ = ADMIT   → sign(ΔR) determines IMPROVED/UNCHANGED/DECREASED -/
+def interact (ti : TotalInteraction) : InteractionOutcome :=
+  match ti.gateTensor with
+  | .reject => .reject
+  | .hold   => .hold
+  | .admit  =>
+      let d := deltaResolution ti.deltaR
+      if d > 0 then .improved
+      else if d == 0 then .unchanged
+      else .decreased
+
+/-- Canonical gate tensor: all five gates admit. -/
+def allAdmit : GateOutcome := .admit
+
+/-- Fixture: the throat saves distance and shell error exceeds projection cost. -/
+def positiveDeltaFixture : ResolutionDelta :=
+  { manifoldDistance := 10
+  , throatDistance   := 3
+  , shellError       := 2
+  , projectedError   := 1 }
+
+/-- Fixture: the throat costs more than it saves. -/
+def negativeDeltaFixture : ResolutionDelta :=
+  { positiveDeltaFixture with throatDistance := 15, projectedError := 5 }
+
+/-- Fixture: break-even. -/
+def zeroDeltaFixture : ResolutionDelta :=
+  { positiveDeltaFixture with throatDistance := 11, projectedError := 1 }
+
+/-- Total interaction with all gates open and positive delta → improved. -/
+def improvedInteractionFixture : TotalInteraction :=
+  { gateTensor := allAdmit, deltaR := positiveDeltaFixture }
+
+/-- Total interaction with all gates open and negative delta → decreased. -/
+def decreasedInteractionFixture : TotalInteraction :=
+  { gateTensor := allAdmit, deltaR := negativeDeltaFixture }
+
+/-- Total interaction with a reject in the gate tensor → reject. -/
+def rejectedInteractionFixture : TotalInteraction :=
+  { gateTensor := .reject, deltaR := positiveDeltaFixture }
+
+/-- Total interaction with a hold in the gate tensor → hold (ΔR ignored). -/
+def heldInteractionFixture : TotalInteraction :=
+  { gateTensor := .hold, deltaR := positiveDeltaFixture }
+
+theorem improvedFixture_yields_improved :
+    interact improvedInteractionFixture = .improved := by
+  native_decide
+
+theorem decreasedFixture_yields_decreased :
+    interact decreasedInteractionFixture = .decreased := by
+  native_decide
+
+theorem rejectedFixture_yields_reject :
+    interact rejectedInteractionFixture = .reject := by
+  native_decide
+
+theorem heldFixture_yields_hold :
+    interact heldInteractionFixture = .hold := by
+  native_decide
+
+theorem gateCompose_reject_dominates_left :
+    gateCompose .reject .admit = .reject := by rfl
+
+theorem gateCompose_reject_dominates_right :
+    gateCompose .admit .reject = .reject := by rfl
+
+theorem gateCompose_hold_blocks_admit :
+    gateCompose .hold .admit = .hold := by rfl
+
+theorem gateCompose_admit_neutral :
+    gateCompose .admit .admit = .admit := by rfl
+
+theorem deltaResolution_positive_fixture :
+    deltaResolution positiveDeltaFixture = 8 := by native_decide
+
+theorem deltaResolution_negative_fixture :
+    deltaResolution negativeDeltaFixture = -8 := by native_decide
+
+theorem deltaResolution_zero_fixture :
+    deltaResolution zeroDeltaFixture = 0 := by native_decide
+
+theorem folded16Fixture_admits :
+    decideFoldedPoint folded16Fixture = .admit := by
+  native_decide
+
+theorem missingReplayFixture_holds :
+    decideFoldedPoint missingReplayFixture = .hold := by
+  native_decide
+
+theorem overCapFixture_holds :
+    decideFoldedPoint overCapFixture = .hold := by
+  native_decide
+
+theorem ordinaryPointFixture_rejects :
+    decideFoldedPoint ordinaryPointFixture = .reject := by
+  native_decide
+
+theorem folded16Fixture_loopsBack :
+    decideLoopback folded16Fixture = .loopback := by
+  native_decide
+
+theorem noPermeabilityFixture_holdsLoopback :
+    decideLoopback noPermeabilityFixture = .hold := by
+  native_decide
+
+theorem ordinaryPointFixture_holdsLoopback :
+    decideLoopback ordinaryPointFixture = .hold := by
+  native_decide
+
+theorem mengerConservedFixture_conserved :
+    decideConservation mengerConservedFixture = .conserved := by
+  native_decide
+
+theorem brokenConservationFixture_rejects :
+    decideConservation brokenConservationFixture = .reject := by
+  native_decide
+
+theorem missingMengerSeedFixture_holds :
+    decideConservation missingMengerSeedFixture = .hold := by
+  native_decide
+
+#eval isFoldedPoint folded16Fixture
+#eval decideFoldedPoint folded16Fixture
+#eval decideFoldedPoint missingReplayFixture
+#eval decideFoldedPoint ordinaryPointFixture
+#eval decideLoopback folded16Fixture
+#eval decideLoopback noPermeabilityFixture
+#eval decideConservation mengerConservedFixture
+#eval decideConservation brokenConservationFixture
+
+#eval gateCompose .reject .admit
+#eval gateCompose .hold .admit
+#eval gateCompose .admit .admit
+#eval gateComposeList [.admit, .admit, .admit]
+#eval gateComposeList [.admit, .hold, .admit]
+#eval gateComposeList [.admit, .reject, .admit]
+#eval deltaResolution positiveDeltaFixture
+#eval deltaResolution negativeDeltaFixture
+#eval deltaResolution zeroDeltaFixture
+#eval interact improvedInteractionFixture
+#eval interact decreasedInteractionFixture
+#eval interact rejectedInteractionFixture
+#eval interact heldInteractionFixture
+
+end Semantics.FoldedPointManifold

0-Core-Formalism/lean/Semantics/Semantics/Core/PathEpigeneticManifold.lean

@@ -0,0 +1,282 @@
+/-
+PathEpigeneticManifold.lean — 1D regulatory path over a 16D manifold
+
+This module models the "circuit path as epigenetic control strand" idea:
+the 1D path is stable carrier geometry, while finite regulatory marks on that
+path determine which dimensions of a 16D manifold are expressed, damped,
+receipted, or routed to quarantine.
+
+The claim boundary is intentionally narrow. This is not a biological
+equivalence, fabrication rule, or compression claim. It is a receipt-bearing
+state update law.
+-/
+
+import Semantics.FixedPoint
+
+namespace Semantics.PathEpigeneticManifold
+
+open Semantics.FixedPoint
+
+/-- The 16 addressable dimensions of the manifold packet. -/
+inductive Dim16 where
+  | identity
+  | route
+  | scale
+  | phase
+  | torsion
+  | curvature
+  | energy
+  | velocity
+  | residual
+  | semanticMass
+  | confidence
+  | density
+  | topology
+  | witness
+  | underverse
+  | time
+  deriving Repr, BEq, DecidableEq
+
+/-- Finite regulatory mark actions carried by a 1D path site. -/
+inductive MarkerAction where
+  | activate
+  | damp
+  | gateWitness
+  | quarantine
+  deriving Repr, BEq, DecidableEq
+
+/-- Terminal decision for a path-regulated manifold update. -/
+inductive PathDecision where
+  | admit
+  | hold
+  | quarantine
+  deriving Repr, BEq, DecidableEq
+
+/-- One regulatory marker attached to a path site. -/
+structure RegulatoryMarker where
+  target : Dim16
+  action : MarkerAction
+  strength : Q0_16
+  receiptPresent : Bool
+  deriving Repr, BEq, DecidableEq
+
+/-- One 1D carrier-site. `layoutClear` is the circuit/route design-rule gate. -/
+structure PathSite where
+  siteId : UInt16
+  marker : RegulatoryMarker
+  layoutClear : Bool
+  deriving Repr, BEq, DecidableEq
+
+/-- The 16D manifold state. All fields use Q0.16 because they are normalized
+dimensionless expression levels in this first receipt surface. -/
+structure Manifold16 where
+  identity : Q0_16
+  route : Q0_16
+  scale : Q0_16
+  phase : Q0_16
+  torsion : Q0_16
+  curvature : Q0_16
+  energy : Q0_16
+  velocity : Q0_16
+  residual : Q0_16
+  semanticMass : Q0_16
+  confidence : Q0_16
+  density : Q0_16
+  topology : Q0_16
+  witness : Q0_16
+  underverse : Q0_16
+  time : Q0_16
+  deriving Repr, BEq, DecidableEq
+
+namespace Manifold16
+
+def zero : Manifold16 :=
+  { identity := Q0_16.zero
+  , route := Q0_16.zero
+  , scale := Q0_16.zero
+  , phase := Q0_16.zero
+  , torsion := Q0_16.zero
+  , curvature := Q0_16.zero
+  , energy := Q0_16.zero
+  , velocity := Q0_16.zero
+  , residual := Q0_16.zero
+  , semanticMass := Q0_16.zero
+  , confidence := Q0_16.zero
+  , density := Q0_16.zero
+  , topology := Q0_16.zero
+  , witness := Q0_16.zero
+  , underverse := Q0_16.zero
+  , time := Q0_16.zero }
+
+def get (s : Manifold16) : Dim16 → Q0_16
+  | Dim16.identity => s.identity
+  | Dim16.route => s.route
+  | Dim16.scale => s.scale
+  | Dim16.phase => s.phase
+  | Dim16.torsion => s.torsion
+  | Dim16.curvature => s.curvature
+  | Dim16.energy => s.energy
+  | Dim16.velocity => s.velocity
+  | Dim16.residual => s.residual
+  | Dim16.semanticMass => s.semanticMass
+  | Dim16.confidence => s.confidence
+  | Dim16.density => s.density
+  | Dim16.topology => s.topology
+  | Dim16.witness => s.witness
+  | Dim16.underverse => s.underverse
+  | Dim16.time => s.time
+
+def set (s : Manifold16) (d : Dim16) (v : Q0_16) : Manifold16 :=
+  match d with
+  | Dim16.identity => { s with identity := v }
+  | Dim16.route => { s with route := v }
+  | Dim16.scale => { s with scale := v }
+  | Dim16.phase => { s with phase := v }
+  | Dim16.torsion => { s with torsion := v }
+  | Dim16.curvature => { s with curvature := v }
+  | Dim16.energy => { s with energy := v }
+  | Dim16.velocity => { s with velocity := v }
+  | Dim16.residual => { s with residual := v }
+  | Dim16.semanticMass => { s with semanticMass := v }
+  | Dim16.confidence => { s with confidence := v }
+  | Dim16.density => { s with density := v }
+  | Dim16.topology => { s with topology := v }
+  | Dim16.witness => { s with witness := v }
+  | Dim16.underverse => { s with underverse := v }
+  | Dim16.time => { s with time := v }
+
+end Manifold16
+
+/-- A regulatory marker is admissible only if its local layout and receipt close. -/
+def markerAdmissible (site : PathSite) : Bool :=
+  site.layoutClear && site.marker.receiptPresent
+
+/-- Apply one marker. Missing receipt leaves the manifold unchanged; the decision
+gate records HOLD separately. Layout failure routes to quarantine. -/
+def applyMarker (s : Manifold16) (site : PathSite) : Manifold16 :=
+  if !site.layoutClear then
+    (s.set Dim16.underverse site.marker.strength).set Dim16.residual site.marker.strength
+  else if !site.marker.receiptPresent then
+    s
+  else
+    match site.marker.action with
+    | MarkerAction.activate =>
+        s.set site.marker.target site.marker.strength
+    | MarkerAction.damp =>
+        s.set site.marker.target Q0_16.zero
+    | MarkerAction.gateWitness =>
+        s.set Dim16.witness Q0_16.one
+    | MarkerAction.quarantine =>
+        (s.set Dim16.underverse site.marker.strength).set Dim16.residual site.marker.strength
+
+/-- Fold a 1D path over the 16D manifold. -/
+def applyPath (s : Manifold16) (path : List PathSite) : Manifold16 :=
+  path.foldl applyMarker s
+
+def anyLayoutViolation : List PathSite → Bool
+  | [] => false
+  | site :: rest => (!site.layoutClear) || anyLayoutViolation rest
+
+def anyMissingReceipt : List PathSite → Bool
+  | [] => false
+  | site :: rest => (site.layoutClear && !site.marker.receiptPresent) || anyMissingReceipt rest
+
+def anyQuarantineMarker : List PathSite → Bool
+  | [] => false
+  | site :: rest => (site.marker.action == MarkerAction.quarantine && site.marker.receiptPresent) || anyQuarantineMarker rest
+
+/-- Path-level decision: physical/layout violation or explicit quarantine wins;
+otherwise missing receipts HOLD; fully receipted paths ADMIT. -/
+def decidePath (path : List PathSite) : PathDecision :=
+  if anyLayoutViolation path || anyQuarantineMarker path then .quarantine
+  else if anyMissingReceipt path then .hold
+  else .admit
+
+/-- One completed path-regulated update receipt. -/
+structure PathReceipt where
+  before : Manifold16
+  after : Manifold16
+  siteCount : Nat
+  decision : PathDecision
+  deriving Repr, BEq, DecidableEq
+
+def runPath (s : Manifold16) (path : List PathSite) : PathReceipt :=
+  { before := s
+  , after := applyPath s path
+  , siteCount := path.length
+  , decision := decidePath path }
+
+def qSmall : Q0_16 := ⟨1⟩
+def qMedium : Q0_16 := ⟨0x0100⟩
+
+def torsionSite : PathSite :=
+  { siteId := 0
+  , marker :=
+      { target := Dim16.torsion
+      , action := MarkerAction.activate
+      , strength := qMedium
+      , receiptPresent := true }
+  , layoutClear := true }
+
+def dampResidualSite : PathSite :=
+  { siteId := 1
+  , marker :=
+      { target := Dim16.residual
+      , action := MarkerAction.damp
+      , strength := qSmall
+      , receiptPresent := true }
+  , layoutClear := true }
+
+def witnessSite : PathSite :=
+  { siteId := 2
+  , marker :=
+      { target := Dim16.witness
+      , action := MarkerAction.gateWitness
+      , strength := Q0_16.one
+      , receiptPresent := true }
+  , layoutClear := true }
+
+def missingReceiptSite : PathSite :=
+  { torsionSite with marker := { torsionSite.marker with receiptPresent := false } }
+
+def layoutViolationSite : PathSite :=
+  { torsionSite with layoutClear := false }
+
+def admittedPath : List PathSite := [torsionSite, witnessSite]
+def holdPath : List PathSite := [missingReceiptSite]
+def quarantinePath : List PathSite := [layoutViolationSite]
+
+theorem admittedPathActivatesTorsion :
+    (runPath Manifold16.zero admittedPath).after.torsion = qMedium := by
+  native_decide
+
+theorem admittedPathClosesWitness :
+    (runPath Manifold16.zero admittedPath).after.witness = Q0_16.one := by
+  native_decide
+
+theorem admittedPathDecision :
+    (runPath Manifold16.zero admittedPath).decision = .admit := by
+  native_decide
+
+theorem holdPathLeavesTorsionUnchanged :
+    (runPath Manifold16.zero holdPath).after.torsion = Q0_16.zero := by
+  native_decide
+
+theorem holdPathDecision :
+    (runPath Manifold16.zero holdPath).decision = .hold := by
+  native_decide
+
+theorem quarantinePathRoutesResidual :
+    (runPath Manifold16.zero quarantinePath).after.residual = qMedium := by
+  native_decide
+
+theorem quarantinePathDecision :
+    (runPath Manifold16.zero quarantinePath).decision = .quarantine := by
+  native_decide
+
+#eval (runPath Manifold16.zero admittedPath).decision
+#eval (runPath Manifold16.zero admittedPath).after.torsion
+#eval (runPath Manifold16.zero holdPath).decision
+#eval (runPath Manifold16.zero quarantinePath).after.underverse
+
+end Semantics.PathEpigeneticManifold

0-Core-Formalism/lean/Semantics/Semantics/Core/QuantumFoamBoundary.lean

@@ -0,0 +1,92 @@
+/-
+QuantumFoamBoundary.lean — bounded fluctuation guard around U0
+
+Quantum foam is modeled here as an accounting boundary around the zero layer,
+not as a promotion rule. Exact neutral closure still belongs to U0. Foam only
+classifies sub-resolution, unreceipted, or stochastic jitter as HOLD.
+-/
+
+namespace Semantics.QuantumFoamBoundary
+
+/-- Coarse scale band for an accounting fluctuation. -/
+inductive FoamScale where
+  | deterministic
+  | measurementFloor
+  | planckAnalogy
+  | subResolution
+  deriving Repr, BEq, DecidableEq
+
+/-- Decision emitted by the foam boundary. -/
+inductive FoamDecision where
+  | exactClosure
+  | holdFoam
+  | rejectClaim
+  deriving Repr, BEq, DecidableEq
+
+/-- Minimal foam-boundary sample.
+
+`netCharge` is the recomputed visible + Underverse + sink charge.
+`jitterBound` is the declared symmetric tolerance for a measurement/noise floor.
+`replayReceiptPresent` distinguishes exact U0 closure from a balanced-looking
+but unreceipted claim.
+-/
+structure FoamSample where
+  scale : FoamScale
+  netCharge : Int
+  jitterBound : Nat
+  replayReceiptPresent : Bool
+  deriving Repr, BEq, DecidableEq
+
+/-- A signed integer lies inside the declared symmetric jitter band. -/
+def withinJitter (s : FoamSample) : Bool :=
+  s.netCharge.natAbs <= s.jitterBound
+
+/-- Foam boundary classifier.
+
+Exact zero with replay belongs to `exactClosure`.
+Nonzero values inside a declared jitter band are HOLD, never ADMIT.
+Nonzero values outside the band reject the zero/foam claim.
+-/
+def decideFoamBoundary (s : FoamSample) : FoamDecision :=
+  if s.netCharge == 0 && s.replayReceiptPresent then .exactClosure
+  else if withinJitter s then .holdFoam
+  else .rejectClaim
+
+def exactZeroFixture : FoamSample :=
+  { scale := .deterministic
+  , netCharge := 0
+  , jitterBound := 0
+  , replayReceiptPresent := true
+  }
+
+def foamJitterFixture : FoamSample :=
+  { scale := .subResolution
+  , netCharge := 1
+  , jitterBound := 2
+  , replayReceiptPresent := false
+  }
+
+def outOfBandFixture : FoamSample :=
+  { scale := .measurementFloor
+  , netCharge := 5
+  , jitterBound := 2
+  , replayReceiptPresent := false
+  }
+
+theorem exactZeroFixture_closes :
+    decideFoamBoundary exactZeroFixture = .exactClosure := by
+  rfl
+
+theorem foamJitterFixture_holds :
+    decideFoamBoundary foamJitterFixture = .holdFoam := by
+  rfl
+
+theorem outOfBandFixture_rejects :
+    decideFoamBoundary outOfBandFixture = .rejectClaim := by
+  rfl
+
+#eval decideFoamBoundary exactZeroFixture
+#eval decideFoamBoundary foamJitterFixture
+#eval decideFoamBoundary outOfBandFixture
+
+end Semantics.QuantumFoamBoundary

0-Core-Formalism/lean/Semantics/Semantics/Core/S3CProjectedGeodesicResolution.lean

@@ -0,0 +1,245 @@
+/-
+S3CProjectedGeodesicResolution.lean — folded-throat resolution gate
+
+This module compares the old S3C projected-geodesic score against the refined
+folded-point theory:
+
+  baseline S3C score
+    = manifold distance minus shell/projection error
+
+  folded-throat score
+    = baseline distance plus throat shortcut gain minus projected error
+
+The refinement is allowed to improve resolution only when the 0D throat has a
+declared folded 16D interior, loopback permeability, Menger-style conservation,
+and genus-3/S3C lobe alignment. Otherwise the refinement holds or rejects
+instead of silently increasing precision.
+-/
+
+import Semantics.Core.FoldedPointManifold
+
+namespace Semantics.S3CProjectedGeodesicResolution
+
+open Semantics.FoldedPointManifold
+
+/-- Resolution comparison after applying the folded-throat refinement. -/
+inductive ResolutionDecision where
+  | improved
+  | unchanged
+  | decreased
+  | hold
+  | reject
+  deriving Repr, BEq, DecidableEq
+
+/-- Diagnostic reason for the resolution decision. -/
+inductive ResolutionReason where
+  | foldedPointRejected
+  | loopbackRejected
+  | conservationRejected
+  | foldedPointMissing
+  | loopbackMissing
+  | conservationMissing
+  | lobeMismatch
+  | noThroatShortcut
+  | shortcutOutrunsResidual
+  | residualOutrunsShortcut
+  | exactBoundary
+  deriving Repr, BEq, DecidableEq
+
+/-- Minimal finite S3C geodesic sample.
+
+`manifoldDist` is the original S3C route distance.
+`throatLength` is the route through the projected 0D throat.
+`shellError` is the old shell/projection residual.
+`projectedError` is the residual after the folded-throat projection.
+`lobeCount = 3` is the S3C/genus-3 alignment witness.
+-/
+structure S3CGeodesicSample where
+  manifoldDist : Nat
+  throatLength : Nat
+  shellError : Nat
+  projectedError : Nat
+  lobeCount : Nat
+  folded : FoldedPointEvent
+  conservation : DimensionalConservation
+  deriving Repr, BEq, DecidableEq
+
+/-- Old resolution score: larger means more usable route resolution. -/
+def baselineScore (s : S3CGeodesicSample) : Nat :=
+  s.manifoldDist - s.shellError
+
+/-- Distance saved by going through the projected throat. -/
+def shortcutGain (s : S3CGeodesicSample) : Nat :=
+  s.manifoldDist - s.throatLength
+
+/-- S3C's three-handle/lobe alignment gate. -/
+def genus3Aligned (s : S3CGeodesicSample) : Bool :=
+  s.lobeCount == 3
+
+/-- Full admissibility gate for using the folded 0D throat as a precision
+refinement. -/
+def foldedThroatAdmissible (s : S3CGeodesicSample) : Bool :=
+  decideFoldedPoint s.folded == .admit &&
+  decideLoopback s.folded == .loopback &&
+  decideConservation s.conservation == .conserved &&
+  genus3Aligned s &&
+  s.throatLength <= s.manifoldDist
+
+/-- Refined resolution score.
+
+The refinement can only claim a sharper route when the folded-throat gate is
+closed. Otherwise it preserves the baseline score and lets `decideResolution`
+return HOLD/REJECT where appropriate.
+-/
+def refinedScore (s : S3CGeodesicSample) : Nat :=
+  if foldedThroatAdmissible s then
+    s.manifoldDist + shortcutGain s - s.projectedError
+  else
+    baselineScore s
+
+/-- Amount of old uncertainty that the folded-throat refinement can pay down.
+
+The refinement can improve only when this budget is larger than the new
+projected residual:
+
+  shortcutGain + shellError > projectedError
+-/
+def resolutionBudget (s : S3CGeodesicSample) : Nat :=
+  shortcutGain s + s.shellError
+
+/-- Signed score delta: refined score minus baseline score. -/
+def resolutionDelta (s : S3CGeodesicSample) : Int :=
+  Int.ofNat (refinedScore s) - Int.ofNat (baselineScore s)
+
+/-- Compare the baseline and refined scores. -/
+def compareScores (base refined : Nat) : ResolutionDecision :=
+  if refined > base then .improved
+  else if refined == base then .unchanged
+  else .decreased
+
+/-- Decide whether the folded-throat theory improves, preserves, decreases, or
+refuses the projected-geodesic resolution. -/
+def decideResolution (s : S3CGeodesicSample) : ResolutionDecision :=
+  if decideFoldedPoint s.folded == .reject ||
+     decideLoopback s.folded == .reject ||
+     decideConservation s.conservation == .reject then
+    .reject
+  else if foldedThroatAdmissible s then
+    compareScores (baselineScore s) (refinedScore s)
+  else
+    .hold
+
+/-- Explain why the score improved, decreased, held, or rejected. -/
+def explainResolution (s : S3CGeodesicSample) : ResolutionReason :=
+  if decideFoldedPoint s.folded == .reject then
+    .foldedPointRejected
+  else if decideLoopback s.folded == .reject then
+    .loopbackRejected
+  else if decideConservation s.conservation == .reject then
+    .conservationRejected
+  else if decideFoldedPoint s.folded != .admit then
+    .foldedPointMissing
+  else if decideLoopback s.folded != .loopback then
+    .loopbackMissing
+  else if decideConservation s.conservation != .conserved then
+    .conservationMissing
+  else if !genus3Aligned s then
+    .lobeMismatch
+  else if !(s.throatLength <= s.manifoldDist) then
+    .noThroatShortcut
+  else
+    match compareScores (baselineScore s) (refinedScore s) with
+    | .improved => .shortcutOutrunsResidual
+    | .decreased => .residualOutrunsShortcut
+    | .unchanged => .exactBoundary
+    | .hold => .exactBoundary
+    | .reject => .exactBoundary
+
+/-- The theory improves resolution when the throat is short, projection error is
+lower than the old shell residual, and all folded/conservation gates close. -/
+def improvedFixture : S3CGeodesicSample :=
+  { manifoldDist := 100
+  , throatLength := 40
+  , shellError := 20
+  , projectedError := 5
+  , lobeCount := 3
+  , folded := folded16Fixture
+  , conservation := mengerConservedFixture }
+
+/-- The theory can decrease resolution when a nominally admissible throat adds
+too little shortcut gain and the projected residual is worse. -/
+def decreasedFixture : S3CGeodesicSample :=
+  { improvedFixture with
+    throatLength := 95
+    shellError := 10
+    projectedError := 20 }
+
+/-- Missing permeability leaves the refinement in HOLD. -/
+def holdFixture : S3CGeodesicSample :=
+  { improvedFixture with folded := noPermeabilityFixture }
+
+/-- Broken conservation rejects the refined geodesic claim. -/
+def rejectFixture : S3CGeodesicSample :=
+  { improvedFixture with conservation := brokenConservationFixture }
+
+/-- The exact boundary where folded-throat gain equals projected residual. -/
+def unchangedFixture : S3CGeodesicSample :=
+  { improvedFixture with
+    throatLength := 90
+    shellError := 10
+    projectedError := 20 }
+
+theorem improvedFixtureImproves :
+    decideResolution improvedFixture = .improved := by
+  native_decide
+
+theorem decreasedFixtureDecreases :
+    decideResolution decreasedFixture = .decreased := by
+  native_decide
+
+theorem holdFixtureHolds :
+    decideResolution holdFixture = .hold := by
+  native_decide
+
+theorem rejectFixtureRejects :
+    decideResolution rejectFixture = .reject := by
+  native_decide
+
+theorem unchangedFixtureUnchanged :
+    decideResolution unchangedFixture = .unchanged := by
+  native_decide
+
+theorem improvedFixtureBaselineScore :
+    baselineScore improvedFixture = 80 := by
+  native_decide
+
+theorem improvedFixtureRefinedScore :
+    refinedScore improvedFixture = 155 := by
+  native_decide
+
+theorem improvedFixtureReason :
+    explainResolution improvedFixture = .shortcutOutrunsResidual := by
+  native_decide
+
+theorem decreasedFixtureReason :
+    explainResolution decreasedFixture = .residualOutrunsShortcut := by
+  native_decide
+
+theorem unchangedFixtureReason :
+    explainResolution unchangedFixture = .exactBoundary := by
+  native_decide
+
+#eval baselineScore improvedFixture
+#eval refinedScore improvedFixture
+#eval resolutionBudget improvedFixture
+#eval resolutionDelta improvedFixture
+#eval decideResolution improvedFixture
+#eval explainResolution improvedFixture
+#eval decideResolution decreasedFixture
+#eval explainResolution decreasedFixture
+#eval decideResolution unchangedFixture
+#eval explainResolution unchangedFixture
+#eval decideResolution holdFixture
+#eval decideResolution rejectFixture
+
+end Semantics.S3CProjectedGeodesicResolution

0-Core-Formalism/lean/Semantics/Semantics/Core/UnderverseZeroLayer.lean

@@ -0,0 +1,101 @@
+/-
+UnderverseZeroLayer.lean — explicit neutral closure accounting
+
+The zero layer is the receipt boundary between observable accounting and
+Underverse/complement accounting. It prevents "missing" or "opposite" terms
+from becoming free variables: a neutral event is admitted only when the net
+charge closes exactly and the replay receipt is present.
+
+The genus-3 case is deliberately a checked assumption surface, not a topology
+proof. Genus 3 may be the selected chart, but zero charge still has to be
+declared and replayed.
+-/
+
+namespace Semantics.UnderverseZeroLayer
+
+/-- Which chart the neutral event is being checked in. -/
+inductive ChargeChart where
+  | ordinary
+  | genus3
+  | mirror
+  | antiBaryonic
+  deriving Repr, BEq, DecidableEq
+
+/-- Terminal decision for the zero layer. -/
+inductive ZeroDecision where
+  | admit
+  | hold
+  | reject
+  deriving Repr, BEq, DecidableEq
+
+/-- Minimal zero-layer event.
+
+`observableCharge` is the visible/accounted side.
+`underverseCharge` is the complement, inverse, hidden, or Underverse side.
+`sinkCharge` is a typed loss/annihilation/sink sidecar.
+
+The event is neutral only when all three sum to zero and replay is present.
+-/
+structure ZeroLayerEvent where
+  chart : ChargeChart
+  genus : Nat
+  observableCharge : Int
+  underverseCharge : Int
+  sinkCharge : Int
+  replayReceiptPresent : Bool
+  deriving Repr, BEq, DecidableEq
+
+/-- Net accounting charge across observable, Underverse, and sink lanes. -/
+def netCharge (e : ZeroLayerEvent) : Int :=
+  e.observableCharge + e.underverseCharge + e.sinkCharge
+
+/-- The neutral closure predicate. -/
+def closesNeutral (e : ZeroLayerEvent) : Bool :=
+  netCharge e == 0 && e.replayReceiptPresent
+
+/-- Genus-3 zero-charge assumption is explicit: genus=3, chart=genus3, net=0,
+and the replay receipt is present. -/
+def genus3ZeroChargeEvent (e : ZeroLayerEvent) : Bool :=
+  e.chart == .genus3 && e.genus == 3 && closesNeutral e
+
+/-- Decision gate for neutral closure. -/
+def decideZeroLayer (e : ZeroLayerEvent) : ZeroDecision :=
+  if closesNeutral e then .admit
+  else if netCharge e == 0 then .hold
+  else .reject
+
+/-- Canonical fixture: visible +1, Underverse -1, no sink, genus-3 chart. -/
+def genus3BalancedFixture : ZeroLayerEvent :=
+  { chart := .genus3
+  , genus := 3
+  , observableCharge := 1
+  , underverseCharge := -1
+  , sinkCharge := 0
+  , replayReceiptPresent := true
+  }
+
+/-- Same charges, but no replay receipt: balance is only HOLD. -/
+def missingReplayFixture : ZeroLayerEvent :=
+  { genus3BalancedFixture with replayReceiptPresent := false }
+
+/-- Nonzero net charge rejects the zero-layer claim. -/
+def nonzeroChargeFixture : ZeroLayerEvent :=
+  { genus3BalancedFixture with underverseCharge := 0 }
+
+theorem genus3BalancedFixture_closes :
+    genus3ZeroChargeEvent genus3BalancedFixture = true := by
+  rfl
+
+theorem missingReplayFixture_holds :
+    decideZeroLayer missingReplayFixture = .hold := by
+  rfl
+
+theorem nonzeroChargeFixture_rejects :
+    decideZeroLayer nonzeroChargeFixture = .reject := by
+  rfl
+
+#eval genus3ZeroChargeEvent genus3BalancedFixture
+#eval decideZeroLayer missingReplayFixture
+#eval decideZeroLayer nonzeroChargeFixture
+
+end Semantics.UnderverseZeroLayer

0-Core-Formalism/lean/Semantics/Semantics/Kernel/EigenGate.lean

@@ -0,0 +1,180 @@
+/-
+EigenGate.lean — The canonical eigengate type.
+
+Every physical law, every compression check, every routing decision is an
+eigenstate condition: ∥G·s − s∥ ≤ τ, where G is the operator defining the
+expected invariant, and the residual is the fraction of deviation from identity.
+
+Residuals live in Q0_16 — the dimensionless pure-fraction type from
+FixedPoint.lean. Products stay in [0,1): the multiplicative gate chain
+never overflows, and any zero-score gate collapses the entire product.
+
+  verdict : admit if residual=0, hold if ≤ threshold, reject if >
+  score   : 1/(1+r) — proximity to λ=1 eigenspace
+  route   : eigenstate / nearEigenstate / boundary / underverse / error
+
+Specific physics emerges from WHICH operator G and WHICH calibration constants
+parameterize it. The full physical universe is the intersection of λ=1
+eigenspaces for all required gate operators simultaneously.
+-/
+
+import Semantics.FixedPoint
+
+namespace Semantics.Kernel
+
+open Semantics.FixedPoint (Q0_16)
+
+inductive EigenVerdict where
+  | admit | hold | reject
+  deriving Repr, BEq, DecidableEq, Inhabited
+
+inductive Route where
+  | eigenstate
+  | nearEigenstate
+  | boundary
+  | underverse
+  | error
+  deriving Repr, BEq, DecidableEq, Inhabited
+
+structure Eigengate (α : Type) where
+  operator  : α → α
+  residual  : α → Q0_16
+  threshold : Q0_16
+
+def verdict {α : Type} (g : Eigengate α) (s : α) : EigenVerdict :=
+  let r := g.residual s
+  if r.val == 0 then EigenVerdict.admit
+  else if r.val ≤ g.threshold.val then EigenVerdict.hold
+  else EigenVerdict.reject
+
+def score (r : Q0_16) : Q0_16 :=
+  let denom := Q0_16.add Q0_16.one r
+  Q0_16.div Q0_16.one denom
+
+def route {α : Type} (g : Eigengate α) (s : α) (hasReceipt : Bool) : Route :=
+  let v := verdict g s
+  let r := g.residual s
+  match v with
+  | EigenVerdict.admit =>
+      if r.val == 0 then Route.eigenstate
+      else Route.nearEigenstate
+  | EigenVerdict.hold  => Route.boundary
+  | EigenVerdict.reject =>
+      if hasReceipt then Route.underverse
+      else Route.error
+
+def chainVerdict {α : Type} (gates : List (Eigengate α × Bool)) (s : α) : EigenVerdict :=
+  let required := gates.filter (fun (_, req) => req) |>.map (fun (g, _) => g)
+  if required.any fun g => verdict g s == EigenVerdict.reject then
+    EigenVerdict.reject
+  else if required.any fun g => verdict g s == EigenVerdict.hold then
+    EigenVerdict.hold
+  else
+    EigenVerdict.admit
+
+def q0Ratio (num den : Nat) : Q0_16 :=
+  if den = 0 then Q0_16.one
+  else ⟨(Nat.min 32767 ((num * 32767) / den)).toUInt16⟩
+
+def shore : Q0_16 := Q0_16.zero
+
+def approach (N : Nat) : Q0_16 :=
+  if N == 0 then Q0_16.zero
+  else if N ≥ 16 then Q0_16.one
+  else
+    let step := (1 <<< N) - 1
+    let maxV := (1 <<< N)
+    q0Ratio step maxV
+
+def testGateAllAdmit : Eigengate Q0_16 :=
+  { operator := λ s => s
+  , residual := λ _ => Q0_16.zero
+  , threshold := Q0_16.one }
+
+def testGateAllReject : Eigengate Q0_16 :=
+  { operator := λ s => s
+  , residual := λ _ => Q0_16.one
+  , threshold := q0Ratio 1 4 }
+
+def testGateResidualAtHalf : Eigengate Q0_16 :=
+  { operator := λ s => s
+  , residual := λ s => if s.val == 0 then Q0_16.zero else Q0_16.half
+  , threshold := q0Ratio 1 4 }
+
+def chainFixtureAllAdmit : List (Eigengate Q0_16 × Bool) :=
+  [ (testGateAllAdmit, true), (testGateAllAdmit, true) ]
+
+def chainFixtureOneRejects : List (Eigengate Q0_16 × Bool) :=
+  [ (testGateAllAdmit, true), (testGateAllReject, true) ]
+
+def chainFixtureOptionalReject : List (Eigengate Q0_16 × Bool) :=
+  [ (testGateAllAdmit, true), (testGateAllReject, false) ]
+
+theorem shore_is_zero : shore.val == 0 := rfl
+
+theorem admit_verdict_on_zero_residual :
+    verdict testGateAllAdmit Q0_16.zero = EigenVerdict.admit := by
+  native_decide
+
+theorem reject_verdict_on_high_residual :
+    verdict testGateAllReject Q0_16.zero = EigenVerdict.reject := by
+  native_decide
+
+theorem score_val_on_zero_residual :
+    (score Q0_16.zero).val = 32768 := by
+  native_decide
+
+theorem chain_all_admit_admits :
+    chainVerdict chainFixtureAllAdmit Q0_16.zero = EigenVerdict.admit := by
+  native_decide
+
+theorem chain_one_rejects_rejects :
+    chainVerdict chainFixtureOneRejects Q0_16.zero = EigenVerdict.reject := by
+  native_decide
+
+theorem chain_optional_reject_no_effect :
+    chainVerdict chainFixtureOptionalReject Q0_16.zero = EigenVerdict.admit := by
+  native_decide
+
+theorem route_admit_zero_residual_is_eigenstate :
+    route testGateAllAdmit Q0_16.zero true = Route.eigenstate := by
+  native_decide
+
+theorem route_reject_no_receipt_is_error :
+    route testGateAllReject Q0_16.zero false = Route.error := by
+  native_decide
+
+theorem route_reject_with_receipt_is_underverse :
+    route testGateAllReject Q0_16.zero true = Route.underverse := by
+  native_decide
+
+theorem approach_bounded (N : Nat) : Q0_16.le (approach N) Q0_16.one := by
+  by_cases hN0 : N = 0
+  · subst hN0; unfold approach Q0_16.le; native_decide
+  · by_cases hN16 : N ≥ 16
+    · unfold approach; simp [hN0, hN16]; unfold Q0_16.le; native_decide
+    · have hNle : N ≤ 15 := by omega
+      interval_cases N <;> unfold approach Q0_16.le <;> native_decide
+
+#eval verdict testGateAllAdmit Q0_16.zero
+#eval verdict testGateAllReject Q0_16.zero
+#eval verdict testGateResidualAtHalf Q0_16.half
+
+#eval score Q0_16.zero
+#eval score Q0_16.half
+
+#eval shore
+
+#eval approach 2
+#eval approach 5
+#eval approach 16
+
+#eval chainVerdict chainFixtureAllAdmit Q0_16.zero
+#eval chainVerdict chainFixtureOneRejects Q0_16.zero
+#eval chainVerdict chainFixtureOptionalReject Q0_16.zero
+
+#eval route testGateAllAdmit Q0_16.zero true
+#eval route testGateAllReject Q0_16.zero true
+#eval route testGateAllReject Q0_16.zero false
+
+end Semantics.Kernel

0-Core-Formalism/lean/Semantics/Semantics/Kernel/GateChain.lean

@@ -0,0 +1,56 @@
+/-
+GateChain.lean — Multiplicative eigengate composition.
+
+Imports EigenGate.lean for the canonical Eigengate, EigenVerdict, and
+score/verdict/route/chainVerdict primitives. Adds chain-level composition
+and product-score computation.
+-/
+
+import Semantics.FixedPoint
+import Semantics.Kernel.EigenGate
+
+namespace Semantics.Kernel
+
+open Semantics.FixedPoint (Q0_16)
+open Semantics.Kernel (Eigengate EigenVerdict)
+
+structure ChainGate (α : Type) where
+  gate     : Eigengate α
+  required : Bool
+
+abbrev GateChain (α : Type) : Type := List (ChainGate α)
+
+def chainGatesToTuples {α : Type} (chain : GateChain α) : List (Eigengate α × Bool) :=
+  chain.map fun cg => (cg.gate, cg.required)
+
+def chainScore {α : Type} (chain : GateChain α) (s : α) : Q0_16 :=
+  let requiredScores := chain
+    |>.filter (fun cg => cg.required)
+    |>.map fun cg => score (cg.gate.residual s)
+  requiredScores.foldl Q0_16.mul Q0_16.one
+
+def testChainAllAdmit : GateChain Q0_16 :=
+  [ { gate := testGateAllAdmit, required := true }
+  , { gate := testGateAllAdmit, required := true } ]
+
+def testChainOptionalOnly : GateChain Q0_16 :=
+  [ { gate := testGateAllAdmit, required := true }
+  , { gate := testGateAllReject, required := false } ]
+
+theorem chainCompositionAllAdmit :
+    chainVerdict (chainGatesToTuples testChainAllAdmit) Q0_16.zero = EigenVerdict.admit := by
+  native_decide
+
+theorem chain_optional_reject_preserves_admit :
+    chainVerdict (chainGatesToTuples testChainOptionalOnly) Q0_16.zero = EigenVerdict.admit := by
+  native_decide
+
+theorem chainScore_all_admit_is_one :
+    chainScore testChainAllAdmit Q0_16.zero = Q0_16.one := by
+  native_decide
+
+#eval chainVerdict (chainGatesToTuples testChainAllAdmit) Q0_16.zero
+#eval chainVerdict (chainGatesToTuples testChainOptionalOnly) Q0_16.zero
+#eval chainScore testChainAllAdmit Q0_16.zero
+
+end Semantics.Kernel

0-Core-Formalism/lean/Semantics/Semantics/Testing/ErdosSurface.lean

@@ -0,0 +1,149 @@
+import Semantics.Testing.ErdosHarness
+
+namespace Semantics.Testing.ErdosSurface
+
+open Semantics.Testing.ErdosHarness
+
+/-!
+ErdosSurface.lean
+
+Pure Lean surface plan for the DAG/FAMM split.  Lean owns the finite packet
+status model and emits a compact receipt for the Rust surface manager.
+
+The surface lanes are deliberately treated as acceleration and transport
+lanes.  They do not promote theorem claims.
+-/
+
+inductive SurfaceLane where
+  | leanTrust
+  | shmControl
+  | vulkanShader
+  | h264Transport
+  | h265Transport
+  | audioDsp
+  deriving Repr, DecidableEq
+
+structure LanePlan where
+  lane : SurfaceLane
+  role : String
+  trustBoundary : String
+  deriving Repr
+
+structure FammCount where
+  domain : String
+  status : String
+  count : Nat
+  deriving Repr, DecidableEq
+
+def laneName : SurfaceLane -> String
+  | .leanTrust => "lean_trust"
+  | .shmControl => "shm_control"
+  | .vulkanShader => "vulkan_shader"
+  | .h264Transport => "h264_transport"
+  | .h265Transport => "h265_transport"
+  | .audioDsp => "audio_dsp"
+
+def surfacePlan : List LanePlan :=
+  [ { lane := .leanTrust
+      role := "packet status model and promotion gate"
+      trustBoundary := "authoritative finite receipt classifier" }
+  , { lane := .shmControl
+      role := "RAM resident payload exchange"
+      trustBoundary := "transport only; hash and length checked by host" }
+  , { lane := .vulkanShader
+      role := "numeric reductions over compact packet counts"
+      trustBoundary := "acceleration only; results rechecked by Lean/CPU" }
+  , { lane := .h264Transport
+      role := "dense packet-frame telemetry transport"
+      trustBoundary := "lossy unless decoded and hash-verified" }
+  , { lane := .h265Transport
+      role := "denser packet-frame telemetry transport"
+      trustBoundary := "lossy unless decoded and hash-verified" }
+  , { lane := .audioDsp
+      role := "streaming DSP metrics over packet waveforms"
+      trustBoundary := "signal lane only; not proof-bearing" } ]
+
+def currentFammCounts : List FammCount :=
+  [ { domain := "erdos_gyarfas", status := "verified_has_power_two_cycle", count := 5 }
+  , { domain := "erdos_mollin_walsh", status := "finite_smoke_pass", count := 3 }
+  , { domain := "erdos_selfridge", status := "finite_smoke_pass", count := 2 }
+  , { domain := "erdos_selfridge", status := "invalid_packet", count := 2 } ]
+
+def totalCount (xs : List FammCount) : Nat :=
+  xs.foldl (fun acc x => acc + x.count) 0
+
+def allSurfaceClaimsFinite (xs : List FammCount) : Bool :=
+  xs.all (fun x =>
+    x.status == "verified_has_power_two_cycle" ||
+    x.status == "finite_smoke_pass" ||
+    x.status == "invalid_packet" ||
+    x.status == "detector_anomaly")
+
+theorem current_surface_claims_are_finite :
+    allSurfaceClaimsFinite currentFammCounts = true := by
+  native_decide
+
+theorem current_surface_total_count :
+    totalCount currentFammCounts = 12 := by
+  native_decide
+
+def escapeJson (s : String) : String :=
+  s.foldl
+    (fun acc c =>
+      if c == '"' then acc ++ "\\\""
+      else if c == '\\' then acc ++ "\\\\"
+      else if c == '\n' then acc ++ "\\n"
+      else acc.push c)
+    ""
+
+def q (s : String) : String :=
+  "\"" ++ escapeJson s ++ "\""
+
+def joinWith (sep : String) : List String -> String
+  | [] => ""
+  | x :: xs => xs.foldl (fun acc y => acc ++ sep ++ y) x
+
+def boolJson (b : Bool) : String :=
+  if b then "true" else "false"
+
+def lanePlanJson (p : LanePlan) : String :=
+  "{" ++
+    q "lane" ++ ":" ++ q (laneName p.lane) ++ "," ++
+    q "role" ++ ":" ++ q p.role ++ "," ++
+    q "trust_boundary" ++ ":" ++ q p.trustBoundary ++
+  "}"
+
+def countJson (c : FammCount) : String :=
+  "{" ++
+    q "domain" ++ ":" ++ q c.domain ++ "," ++
+    q "status" ++ ":" ++ q c.status ++ "," ++
+    q "count" ++ ":" ++ toString c.count ++
+  "}"
+
+def countsArrayJson (xs : List FammCount) : String :=
+  "[" ++ joinWith "," (xs.map countJson) ++ "]"
+
+def countValuesJson (xs : List FammCount) : String :=
+  "[" ++ joinWith "," (xs.map (fun x => toString x.count)) ++ "]"
+
+def lanesJson : String :=
+  "[" ++ joinWith "," (surfacePlan.map lanePlanJson) ++ "]"
+
+def surfaceReceiptJson : String :=
+  "{" ++
+    q "schema" ++ ":" ++ q "erdos_surface_v1" ++ "," ++
+    q "claim_boundary" ++ ":" ++ q "surface lanes accelerate or transport; Lean owns promotion gates" ++ "," ++
+    q "finite_statuses_only" ++ ":" ++ boolJson (allSurfaceClaimsFinite currentFammCounts) ++ "," ++
+    q "total_count" ++ ":" ++ toString (totalCount currentFammCounts) ++ "," ++
+    q "counts" ++ ":" ++ countsArrayJson currentFammCounts ++ "," ++
+    q "count_values" ++ ":" ++ countValuesJson currentFammCounts ++ "," ++
+    q "lanes" ++ ":" ++ lanesJson ++
+  "}"
+
+def main : IO Unit := do
+  IO.println surfaceReceiptJson
+
+end Semantics.Testing.ErdosSurface
+
+def main : IO Unit :=
+  Semantics.Testing.ErdosSurface.main