/-
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
