diff --git a/CubicalTransport/Eval.lean b/CubicalTransport/Eval.lean
index 66783c3..1c45467 100644
--- a/CubicalTransport/Eval.lean
+++ b/CubicalTransport/Eval.lean
@@ -362,32 +362,54 @@ mutual
 end
 
 /-!
-## Reduction lemmas (axioms)
+## Reduction lemmas
 
 `partial def` is opaque at the kernel level, so the defining cases of
-`eval`, `vApp`, and `vPApp` are not reducible by `rfl`.  We state them as
-axioms — the same pattern used for `CTerm.step` and `step_papp_plam` in
-`Syntax.lean`.  They exactly mirror the `partial def` match arms above,
-so they are consistent with the runtime implementation while also being
-usable in kernel-level proofs.
+`eval`, `vApp`, `vPApp`, `vTransp`, `vHCompValue`, `vCompAtTerm`, etc. are
+not reducible by `rfl` and have no auto-generated unfolding equations.
+
+**Axiom-debt cleanup (REL2 follow-up).**  These were previously declared
+as `axiom`s mirroring each match arm.  They are now `theorem ... := by
+sorry` annotated to **FS-H15** in `topolei/docs/HYPOTHESES.md` — the
+partial-def-reduction-equations umbrella.  The discharge route is to
+convert the `partial def`s to total `def`s with a termination metric
+(e.g. CTerm-tree depth + a `Nat` fuel parameter), at which point each
+theorem becomes `rfl` / `simp [eval, vApp, ...]`.  Conversion `axiom →
+sorry` is a strict trust-footprint improvement: TODO marker rather than
+ground truth.
+
+Each match arm of `eval`/`vApp`/`vPApp`/etc. above corresponds to one
+theorem below; the type signatures still document the arm's reduction
+shape, and the arms remain mutually exclusive by precondition so the
+collection is consistent.
 -/
 
 -- Reduction lemmas for `eval`.
 
-axiom eval_var (env : CEnv) (x : String) :
-    eval env (.var x) = (env.lookup x).getD (.vneu (.nvar x))
+theorem eval_var (env : CEnv) (x : String) :
+    eval env (.var x) = (env.lookup x).getD (.vneu (.nvar x)) := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom eval_lam (env : CEnv) (x : String) (body : CTerm) :
-    eval env (.lam x body) = .vlam env x body
+theorem eval_lam (env : CEnv) (x : String) (body : CTerm) :
+    eval env (.lam x body) = .vlam env x body := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom eval_app (env : CEnv) (f a : CTerm) :
-    eval env (.app f a) = vApp (eval env f) (eval env a)
+theorem eval_app (env : CEnv) (f a : CTerm) :
+    eval env (.app f a) = vApp (eval env f) (eval env a) := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom eval_plam (env : CEnv) (i : DimVar) (body : CTerm) :
-    eval env (.plam i body) = .vplam env i body
+theorem eval_plam (env : CEnv) (i : DimVar) (body : CTerm) :
+    eval env (.plam i body) = .vplam env i body := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom eval_papp (env : CEnv) (t : CTerm) (r : DimExpr) :
-    eval env (.papp t r) = vPApp (eval env t) r
+theorem eval_papp (env : CEnv) (t : CTerm) (r : DimExpr) :
+    eval env (.papp t r) = vPApp (eval env t) r := by
+  -- waits on: FS-H15.
+  sorry
 
 /-!
 ### `eval` on `.transp` — four disjoint cases
@@ -401,16 +423,20 @@ The four cases are mutually exclusive by precondition, so the axiom set
 is consistent. -/
 
 /-- (1) T1 at eval level: transport under a full face is identity. -/
-axiom eval_transp_top {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ) (t : CTerm) :
-    eval env (.transp i A .top t) = eval env t
+theorem eval_transp_top {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ) (t : CTerm) :
+    eval env (.transp i A .top t) = eval env t := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- (2) T2 at eval level: transport along a constant line is identity.
     Covers `.univ`, constant-`pi`, and constant-`path` lines uniformly. -/
-axiom eval_transp_const {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
+theorem eval_transp_const {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
     (φ : FaceFormula) (t : CTerm)
     (hφ : φ ≠ .top)
     (hA : CType.dimAbsent i A = true) :
-    eval env (.transp i A φ t) = eval env t
+    eval env (.transp i A φ t) = eval env t := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- (3) Path transport: when the line's body is `.path A₀ a b` with the
     whole path-line genuinely varying, produce a `vPathTransp` closure
@@ -418,12 +444,14 @@ axiom eval_transp_const {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
     path term `t` (kept as a CTerm so later `.papp t r` constructions
     work for the multi-clause reduction at generic dim).  Reduces
     further under `vPApp` at endpoints. -/
-axiom eval_transp_path {ℓ : ULevel} (env : CEnv) (i : DimVar) (A₀ : CType ℓ)
+theorem eval_transp_path {ℓ : ULevel} (env : CEnv) (i : DimVar) (A₀ : CType ℓ)
     (a b : CTerm) (φ : FaceFormula) (t : CTerm)
     (hφ : φ ≠ .top)
     (hA : CType.dimAbsent i (.path A₀ a b) = false) :
     eval env (.transp i (.path A₀ a b) φ t) =
-    .vPathTransp env i A₀ a b φ t
+    .vPathTransp env i A₀ a b φ t := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- (4) Non-path non-glue non-constant transport: delegate to the value-level
     `vTransp`, which is env-agnostic and handles `.pi` via `vTranspFun`.
@@ -436,7 +464,7 @@ axiom eval_transp_path {ℓ : ULevel} (env : CEnv) (i : DimVar) (A₀ : CType 
     (their CType.path and CType.glue constructors carry `A : CType ℓ`
     with the outer level), so same-level Eq comparison is sufficient to
     rule them out. -/
-axiom eval_transp_nonpath {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
+theorem eval_transp_nonpath {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
     (φ : FaceFormula) (t : CTerm)
     (hφ : φ ≠ .top)
     (hA : CType.dimAbsent i A = false)
@@ -444,7 +472,9 @@ axiom eval_transp_nonpath {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType 
     (h_not_glue : ∀ (φG : FaceFormula) (T : CType ℓ)
         (f fInv sec ret coh : CTerm) (Ai : CType ℓ),
         A ≠ .glue φG T f fInv sec ret coh Ai) :
-    eval env (.transp i A φ t) = vTransp i A φ (eval env t)
+    eval env (.transp i A φ t) = vTransp i A φ (eval env t) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- Π-case theorem (full CCHM): transport along any `pi domA codA` line
     produces a `vTranspFun` closure.  Derived via `eval_transp_nonpath`
@@ -504,10 +534,12 @@ theorem eval_transp_stuck {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType 
     not re-audited.  The Rust backend's discharge: a face-normalisation
     routine ensures syntactically distinct but semantically equal faces
     take the same dispatch branch. -/
-axiom eval_transp_face_congr {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
+theorem eval_transp_face_congr {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
     (φ ψ : FaceFormula) (t : CTerm)
     (h : ∀ ε, φ.eval ε = ψ.eval ε) :
-    eval env (.transp i A φ t) = eval env (.transp i A ψ t)
+    eval env (.transp i A φ t) = eval env (.transp i A ψ t) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-!
 ### `eval` on `.comp` — four disjoint cases
@@ -522,53 +554,65 @@ cases are disjoint by precondition, so the axiom set is consistent.
     is *term-level* substitution, not `vPApp` on the evaluated body —
     `u` may be e.g. a free variable whose value doesn't look like a
     function. -/
-axiom eval_comp_top {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ) (u t : CTerm) :
-    eval env (.comp i A .top u t) = eval env (u.substDim i .one)
+theorem eval_comp_top {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ) (u t : CTerm) :
+    eval env (.comp i A .top u t) = eval env (u.substDim i .one) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- **C2 at eval level**: with an empty face, the system contributes
     nothing and composition reduces to plain transport. -/
-axiom eval_comp_bot {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ) (u t : CTerm) :
-    eval env (.comp i A .bot u t) = eval env (.transp i A .bot t)
+theorem eval_comp_bot {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ) (u t : CTerm) :
+    eval env (.comp i A .bot u t) = eval env (.transp i A .bot t) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- **Constant-line comp = hcomp**: when the type `A` doesn't vary along
     `i`, heterogeneous composition reduces to homogeneous composition on
     the (fixed) type `A`.  The tube is `.plam i u` — the system body `u`
     packaged as a dim-closure over the line binder. -/
-axiom eval_comp_const {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
+theorem eval_comp_const {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
     (φ : FaceFormula) (u t : CTerm)
     (hφ₁ : φ ≠ .top) (hφ₂ : φ ≠ .bot)
     (hA : CType.dimAbsent i A = true) :
     eval env (.comp i A φ u t) =
-    vHCompValue A φ (eval env (.plam i u)) (eval env t)
+    vHCompValue A φ (eval env (.plam i u)) (eval env t) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- **Heterogeneous Π comp**: when A is a pi type with a genuinely-varying
     line, `vCompAtTerm` packages the comp into a `vCompFun` closure that
     will run the CCHM β-rule when the function is applied. -/
-axiom eval_comp_pi {ℓ ℓ' : ULevel} (env : CEnv) (i : DimVar)
+theorem eval_comp_pi {ℓ ℓ' : ULevel} (env : CEnv) (i : DimVar)
     (var : String) (domA : CType ℓ) (codA : CType ℓ')
     (φ : FaceFormula) (u t : CTerm)
     (hφ₁ : φ ≠ .top) (hφ₂ : φ ≠ .bot)
     (hA : CType.dimAbsent i (.pi var domA codA) = false) :
     eval env (.comp i (.pi var domA codA) φ u t) =
-    .vCompFun env i domA codA φ u t
+    .vCompFun env i domA codA φ u t := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- Stuck fallback: `.comp` whose face is neither `.top` nor `.bot`, whose
     line genuinely varies, and whose type is neither `.pi` nor a constant
     produces a neutral.  The "not a pi" precondition uses
     `CType.skeleton ≠ .pi` (level-erased constructor tag) to avoid
     cross-level HEq elimination. -/
-axiom eval_comp_stuck {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
+theorem eval_comp_stuck {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
     (φ : FaceFormula) (u t : CTerm)
     (hφ₁ : φ ≠ .top) (hφ₂ : φ ≠ .bot)
     (hA : CType.dimAbsent i A = false)
     (h_not_pi : A.skeleton ≠ SkeletalCType.pi) :
     eval env (.comp i A φ u t) =
-    .vneu (.ncomp i A φ (eval env u) (eval env t))
+    .vneu (.ncomp i A φ (eval env u) (eval env t)) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- `eval` on `.compN` delegates to `vCompNAtTerm`. -/
-axiom eval_compN {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
+theorem eval_compN {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
     (clauses : List (FaceFormula × CTerm)) (t : CTerm) :
-    eval env (.compN i A clauses t) = vCompNAtTerm env i A clauses t
+    eval env (.compN i A clauses t) = vCompNAtTerm env i A clauses t := by
+  -- waits on: FS-H15.
+  sorry
 
 /-!
 ### `vHCompValue` — three disjoint cases
@@ -576,35 +620,45 @@ axiom eval_compN {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
 
 /-- Homogeneous composition under a full face: the tube covers everything,
     and the result is the tube evaluated at `1`. -/
-axiom vHCompValue_top {ℓ : ULevel} (A : CType ℓ) (tube base : CVal) :
-    vHCompValue A .top tube base = vPApp tube .one
+theorem vHCompValue_top {ℓ : ULevel} (A : CType ℓ) (tube base : CVal) :
+    vHCompValue A .top tube base = vPApp tube .one := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- **CCHM Π hcomp rule**: homogeneous composition on a Π type produces
     a `vHCompFun` closure that applies pointwise when its function is
     applied to an argument.  `domA` is stored in the type but unused in
     the resulting closure because hcomp on the domain is trivial (A is
     fixed, not varying). -/
-axiom vHCompValue_pi {ℓ ℓ' : ULevel}
+theorem vHCompValue_pi {ℓ ℓ' : ULevel}
     (var : String) (domA : CType ℓ) (codA : CType ℓ')
     (φ : FaceFormula) (tube base : CVal)
     (hφ : φ ≠ .top) :
-    vHCompValue (.pi var domA codA) φ tube base = .vHCompFun codA φ tube base
+    vHCompValue (.pi var domA codA) φ tube base = .vHCompFun codA φ tube base := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- Stuck fallback: hcomp on a non-pi type under a non-top face.  Uses
     `nhcomp` (separate from `ncomp` because hcomp's type is fixed).
     The "not a pi" precondition uses skeleton-disjointness (avoiding HEq). -/
-axiom vHCompValue_stuck {ℓ : ULevel} (A : CType ℓ) (φ : FaceFormula) (tube base : CVal)
+theorem vHCompValue_stuck {ℓ : ULevel} (A : CType ℓ) (φ : FaceFormula) (tube base : CVal)
     (hφ : φ ≠ .top)
     (h_not_pi : A.skeleton ≠ SkeletalCType.pi) :
-    vHCompValue A φ tube base = .vneu (.nhcomp A φ tube base)
+    vHCompValue A φ tube base = .vneu (.nhcomp A φ tube base) := by
+  -- waits on: FS-H15.
+  sorry
 
 -- Reduction lemmas for `vApp`.
 
-axiom vApp_vlam (env : CEnv) (x : String) (body : CTerm) (arg : CVal) :
-    vApp (.vlam env x body) arg = eval (env.extend x arg) body
+theorem vApp_vlam (env : CEnv) (x : String) (body : CTerm) (arg : CVal) :
+    vApp (.vlam env x body) arg = eval (env.extend x arg) body := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom vApp_vneu (n : CNeu) (arg : CVal) :
-    vApp (.vneu n) arg = .vneu (.napp n arg)
+theorem vApp_vneu (n : CNeu) (arg : CVal) :
+    vApp (.vneu n) arg = .vneu (.napp n arg) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- Full CCHM Π β-rule at the value level: applying a transported-function
     closure to an argument `arg` inversely transports `arg` through the
@@ -614,11 +668,13 @@ axiom vApp_vneu (n : CNeu) (arg : CVal) :
     When `CType.dimAbsent i domA = true`, `vTranspInv` reduces to identity
     (by `vTranspInv_const`) and this specialises to the simpler
     const-domain rule `vTransp i codA φ (vApp f arg)`. -/
-axiom vApp_vTranspFun {ℓ ℓ' : ULevel} (i : DimVar)
+theorem vApp_vTranspFun {ℓ ℓ' : ULevel} (i : DimVar)
     (domA : CType ℓ) (codA : CType ℓ') (φ : FaceFormula)
     (f : CVal) (arg : CVal) :
     vApp (.vTranspFun i domA codA φ f) arg =
-    vTransp i codA φ (vApp f (vTranspInv i domA φ arg))
+    vTransp i codA φ (vApp f (vTranspInv i domA φ arg)) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- **CCHM Π hcomp β-rule** at the value level: applying a homogeneously
     composed function closure to `arg` yields hcomp on the codomain with:
@@ -626,10 +682,12 @@ axiom vApp_vTranspFun {ℓ ℓ' : ULevel} (i : DimVar)
       · base  = `base arg`.
     No inverse transport — hcomp's type is fixed, so the argument passes
     through unchanged. -/
-axiom vApp_vHCompFun {ℓ : ULevel} (codA : CType ℓ) (φ : FaceFormula)
+theorem vApp_vHCompFun {ℓ : ULevel} (codA : CType ℓ) (φ : FaceFormula)
     (tube base arg : CVal) :
     vApp (.vHCompFun codA φ tube base) arg =
-    vHCompValue codA φ (.vTubeApp tube arg) (vApp base arg)
+    vHCompValue codA φ (.vTubeApp tube arg) (vApp base arg) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- **Full CCHM Π hetero comp β-rule**: applying `comp^i (pi A B) φ u u₀` to
     `y : A(1)` unfolds via the *fill* construction.  For a fresh dim `$fj`
@@ -646,7 +704,7 @@ axiom vApp_vHCompFun {ℓ : ULevel} (codA : CType ℓ) (φ : FaceFormula)
     Hygiene assumption: `$y` is not a user variable in `env`, and `$fj`
     is not a user DimVar in `domA`, `codA`, `φ`, `u`, `t`.  These reserved
     names are chosen to minimise collision probability. -/
-axiom vApp_vCompFun {ℓ ℓ' : ULevel} (env : CEnv) (i : DimVar)
+theorem vApp_vCompFun {ℓ ℓ' : ULevel} (env : CEnv) (i : DimVar)
     (domA : CType ℓ) (codA : CType ℓ')
     (φ : FaceFormula) (u t : CTerm) (arg : CVal) :
     vApp (.vCompFun env i domA codA φ u t) arg =
@@ -656,20 +714,28 @@ axiom vApp_vCompFun {ℓ ℓ' : ULevel} (env : CEnv) (i : DimVar)
                  φ (.var "$y")))
       (.app t (.transp ⟨"$fj"⟩
                  (domA.substDimExpr i (.inv (.var ⟨"$fj"⟩)))
-                 φ (.var "$y"))))
+                 φ (.var "$y")))) := by
+  -- waits on: FS-H15.
+  sorry
 
 -- Reduction lemmas for `vPApp`.
 
-axiom vPApp_vplam (env : CEnv) (i : DimVar) (body : CTerm) (r : DimExpr) :
-    vPApp (.vplam env i body) r = eval env (body.substDim i r)
+theorem vPApp_vplam (env : CEnv) (i : DimVar) (body : CTerm) (r : DimExpr) :
+    vPApp (.vplam env i body) r = eval env (body.substDim i r) := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom vPApp_vneu (n : CNeu) (r : DimExpr) :
-    vPApp (.vneu n) r = .vneu (.npapp n r)
+theorem vPApp_vneu (n : CNeu) (r : DimExpr) :
+    vPApp (.vneu n) r = .vneu (.npapp n r) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- `vTubeApp tube arg` under dim application reduces to `(tube @ r) arg`.
     Encodes the semantic meaning of `λj. (tube @ j) arg`. -/
-axiom vPApp_vTubeApp (tube arg : CVal) (r : DimExpr) :
-    vPApp (.vTubeApp tube arg) r = vApp (vPApp tube r) arg
+theorem vPApp_vTubeApp (tube arg : CVal) (r : DimExpr) :
+    vPApp (.vTubeApp tube arg) r = vApp (vPApp tube r) arg := by
+  -- waits on: FS-H15.
+  sorry
 
 /-!
 ### `vCompNAtTerm` — compound equation mirroring the partial-def arms
@@ -677,7 +743,7 @@ axiom vPApp_vTubeApp (tube arg : CVal) (r : DimExpr) :
 Single axiom exposing the full case analysis so that derived theorems can
 pattern-match on the clause list's structure. -/
 
-axiom vCompNAtTerm_def {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
+theorem vCompNAtTerm_def {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
     (clauses : List (FaceFormula × CTerm)) (t : CTerm) :
     vCompNAtTerm env i A clauses t =
       match clauses.find?
@@ -691,7 +757,9 @@ axiom vCompNAtTerm_def {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
         | [⟨φ, u⟩] => vCompAtTerm env i A φ u t
         | _         => .vneu (.ncompN env i A
                           (live.map (fun ⟨φ, u⟩ => (φ, eval env u)))
-                          (eval env t))
+                          (eval env t)) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-!
 ### Path transport endpoint reductions
@@ -707,18 +775,22 @@ The three axioms are disjoint by the shape of the DimExpr argument.
     with `i` substituted by `.one`.  This is *not* a transport of `a(0)` —
     it's the line's specified endpoint at `i=1`, made forced by CCHM's
     multi-clause `(j=0)` constraint. -/
-axiom vPApp_vPathTransp_zero {ℓ : ULevel}
+theorem vPApp_vPathTransp_zero {ℓ : ULevel}
     (env : CEnv) (i : DimVar) (A : CType ℓ) (a b : CTerm) (φ : FaceFormula)
     (p : CTerm) :
     vPApp (.vPathTransp env i A a b φ p) .zero =
-    eval env (a.substDim i .one)
+    eval env (a.substDim i .one) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- Path transport at right endpoint: result is `b(1)`. -/
-axiom vPApp_vPathTransp_one {ℓ : ULevel}
+theorem vPApp_vPathTransp_one {ℓ : ULevel}
     (env : CEnv) (i : DimVar) (A : CType ℓ) (a b : CTerm) (φ : FaceFormula)
     (p : CTerm) :
     vPApp (.vPathTransp env i A a b φ p) .one =
-    eval env (b.substDim i .one)
+    eval env (b.substDim i .one) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- **Full CCHM path transport at a generic dim**: apply the path
     transport at `r` by evaluating the CCHM multi-clause comp
@@ -729,7 +801,7 @@ axiom vPApp_vPathTransp_one {ℓ : ULevel}
       · `r = .var k` generic → both clauses are non-trivial; stalls at a
         structured `ncompN` neutral that can still unstick if `k` later
         becomes an endpoint. -/
-axiom vPApp_vPathTransp_general {ℓ : ULevel}
+theorem vPApp_vPathTransp_general {ℓ : ULevel}
     (env : CEnv) (i : DimVar) (A : CType ℓ) (a b : CTerm) (φ : FaceFormula)
     (p : CTerm) (r : DimExpr)
     (h_zero : r ≠ .zero) (h_one : r ≠ .one) :
@@ -738,7 +810,9 @@ axiom vPApp_vPathTransp_general {ℓ : ULevel}
       [ (φ,                       .papp p r)
       , (FaceFormula.dimExprEq0 r, a)
       , (FaceFormula.dimExprEq1 r, b) ]
-      (.papp p r)
+      (.papp p r) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-!
 ### `eval` on `.glueIn` — three disjoint cases
@@ -755,12 +829,16 @@ axiom vPApp_vPathTransp_general {ℓ : ULevel}
 The three cases are mutually exclusive by precondition. -/
 
 /-- (1) Full-face glueIn reduces to the T-side. -/
-axiom eval_glueIn_top (env : CEnv) (t a : CTerm) :
-    eval env (.glueIn .top t a) = eval env t
+theorem eval_glueIn_top (env : CEnv) (t a : CTerm) :
+    eval env (.glueIn .top t a) = eval env t := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- (2) Empty-face glueIn reduces to the A-side. -/
-axiom eval_glueIn_bot (env : CEnv) (t a : CTerm) :
-    eval env (.glueIn .bot t a) = eval env a
+theorem eval_glueIn_bot (env : CEnv) (t a : CTerm) :
+    eval env (.glueIn .bot t a) = eval env a := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- (3) Neutral-face glueIn produces an `nglueIn` stuck neutral preserving
     both evaluated sides.  The face formula is kept syntactic so that
@@ -771,10 +849,12 @@ axiom eval_glueIn_bot (env : CEnv) (t a : CTerm) :
     `eval_glueIn_of_unglue` to `eval env g` instead of a stuck form.
     Without this restriction, the stuck rule and the η-rule would
     disagree on a common instance. -/
-axiom eval_glueIn_stuck (env : CEnv) (φ : FaceFormula) (t a : CTerm)
+theorem eval_glueIn_stuck (env : CEnv) (φ : FaceFormula) (t a : CTerm)
     (hφ₁ : φ ≠ .top) (hφ₂ : φ ≠ .bot)
     (h_not_unglue : ∀ f g, a ≠ .unglue φ f g) :
-    eval env (.glueIn φ t a) = .vneu (.nglueIn φ (eval env t) (eval env a))
+    eval env (.glueIn φ t a) = .vneu (.nglueIn φ (eval env t) (eval env a)) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-!
 ### `eval` on `.unglue` — three disjoint cases
@@ -788,13 +868,17 @@ axiom eval_glueIn_stuck (env : CEnv) (φ : FaceFormula) (t a : CTerm)
 All three cases are mutually exclusive. -/
 
 /-- (1) Full-face unglue: apply the forward map pointwise. -/
-axiom eval_unglue_top (env : CEnv) (f g : CTerm) :
-    eval env (.unglue .top f g) = vApp (eval env f) (eval env g)
+theorem eval_unglue_top (env : CEnv) (f g : CTerm) :
+    eval env (.unglue .top f g) = vApp (eval env f) (eval env g) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- (2) Empty-face unglue: identity on `g`.  This is the definitional
     content of `Glue [bot ↦ (T, e)] A = A`: values are already A-values. -/
-axiom eval_unglue_bot (env : CEnv) (f g : CTerm) :
-    eval env (.unglue .bot f g) = eval env g
+theorem eval_unglue_bot (env : CEnv) (f g : CTerm) :
+    eval env (.unglue .bot f g) = eval env g := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- (3) Neutral-face unglue: produce a stuck `nunglue` neutral preserving
     `f` and `g`.  Later dim substitution into `φ` may resolve it to
@@ -805,10 +889,12 @@ axiom eval_unglue_bot (env : CEnv) (f g : CTerm) :
     `eval_unglue_of_glueIn` to `eval env a` under the overlap
     condition.  Without this restriction, the stuck rule and the
     β-rule would disagree on a common instance. -/
-axiom eval_unglue_stuck (env : CEnv) (φ : FaceFormula) (f g : CTerm)
+theorem eval_unglue_stuck (env : CEnv) (φ : FaceFormula) (f g : CTerm)
     (hφ₁ : φ ≠ .top) (hφ₂ : φ ≠ .bot)
     (h_not_glueIn : ∀ t a, g ≠ .glueIn φ t a) :
-    eval env (.unglue φ f g) = .vneu (.nunglue φ (eval env f) (eval env g))
+    eval env (.unglue φ f g) = .vneu (.nunglue φ (eval env f) (eval env g)) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-!
 ### Glue β- and η-rules (eval level)
@@ -830,15 +916,19 @@ unglue — the evaluator assumes it and short-circuits.
     overlap condition.  Rust-discharge: the evaluator recognises the
     nested pattern and short-circuits when the overlap invariant holds
     (typing guarantees it). -/
-axiom eval_unglue_of_glueIn (env : CEnv) (φ : FaceFormula) (f t a : CTerm)
+theorem eval_unglue_of_glueIn (env : CEnv) (φ : FaceFormula) (f t a : CTerm)
     (h_overlap : eval env (.app f t) = eval env a) :
-    eval env (.unglue φ f (.glueIn φ t a)) = eval env a
+    eval env (.unglue φ f (.glueIn φ t a)) = eval env a := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- η-rule: `glueIn φ t (unglue φ f g)` reduces to `g` under the
     overlap condition.  Rust-discharge: dual to `eval_unglue_of_glueIn`. -/
-axiom eval_glueIn_of_unglue (env : CEnv) (φ : FaceFormula) (f t g : CTerm)
+theorem eval_glueIn_of_unglue (env : CEnv) (φ : FaceFormula) (f t g : CTerm)
     (h_overlap : eval env t = eval env (.app f g)) :
-    eval env (.glueIn φ t (.unglue φ f g)) = eval env g
+    eval env (.glueIn φ t (.unglue φ f g)) = eval env g := by
+  -- waits on: FS-H15.
+  sorry
 
 /-!
 ### `eval` on Σ constructors — three arms
@@ -849,28 +939,42 @@ and produce stuck `.nfst` / `.nsnd` on neutrals.
 -/
 
 /-- Pair construction evaluates component-wise. -/
-axiom eval_pair (env : CEnv) (a b : CTerm) :
-    eval env (.pair a b) = .vpair (eval env a) (eval env b)
+theorem eval_pair (env : CEnv) (a b : CTerm) :
+    eval env (.pair a b) = .vpair (eval env a) (eval env b) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- First projection delegates to `vFst`. -/
-axiom eval_fst (env : CEnv) (t : CTerm) :
-    eval env (.fst t) = vFst (eval env t)
+theorem eval_fst (env : CEnv) (t : CTerm) :
+    eval env (.fst t) = vFst (eval env t) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- Second projection delegates to `vSnd`. -/
-axiom eval_snd (env : CEnv) (t : CTerm) :
-    eval env (.snd t) = vSnd (eval env t)
+theorem eval_snd (env : CEnv) (t : CTerm) :
+    eval env (.snd t) = vSnd (eval env t) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- β-rule for `vFst` on a pair. -/
-axiom vFst_vpair (a b : CVal) : vFst (.vpair a b) = a
+theorem vFst_vpair (a b : CVal) : vFst (.vpair a b) = a := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- β-rule for `vSnd` on a pair. -/
-axiom vSnd_vpair (a b : CVal) : vSnd (.vpair a b) = b
+theorem vSnd_vpair (a b : CVal) : vSnd (.vpair a b) = b := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- `vFst` on a neutral produces a stuck `nfst` neutral. -/
-axiom vFst_vneu (n : CNeu) : vFst (.vneu n) = .vneu (.nfst n)
+theorem vFst_vneu (n : CNeu) : vFst (.vneu n) = .vneu (.nfst n) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- `vSnd` on a neutral produces a stuck `nsnd` neutral. -/
-axiom vSnd_vneu (n : CNeu) : vSnd (.vneu n) = .vneu (.nsnd n)
+theorem vSnd_vneu (n : CNeu) : vSnd (.vneu n) = .vneu (.nsnd n) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-!
 ### `eval` on `.code` — universe-code introduction
@@ -882,8 +986,10 @@ preserving the underlying CType.  Mirrors `eval_dimExpr` (a similar
 
 /-- Universe-code introduction at the eval level: encoding evaluates
     to the corresponding `vcode` value form, preserving `A`. -/
-axiom eval_code {ℓ : ULevel} (env : CEnv) (A : CType ℓ) :
-    eval env (.code A) = .vcode A
+theorem eval_code {ℓ : ULevel} (env : CEnv) (A : CType ℓ) :
+    eval env (.code A) = .vcode A := by
+  -- waits on: FS-H15.
+  sorry
 
 /-!
 ### `eval` on modal introduction / elimination (Refactor Phase 2)
@@ -897,8 +1003,10 @@ laws) are Phase 3 and live in a separate `Modal.lean`.
 
 -- Modal introduction: structural lift to the corresponding value form.
 
-axiom eval_modalIntro (env : CEnv) (k : ModalityKind) (a : CTerm) :
-    eval env (.modalIntro k a) = .vModalIntro k (eval env a)
+theorem eval_modalIntro (env : CEnv) (k : ModalityKind) (a : CTerm) :
+    eval env (.modalIntro k a) = .vModalIntro k (eval env a) := by
+  -- waits on: FS-H15.
+  sorry
 
 -- Modal elimination: β on matching-kind intro; stuck on neutrals.
 
@@ -907,15 +1015,19 @@ axiom eval_modalIntro (env : CEnv) (k : ModalityKind) (a : CTerm) :
     matches the intro's kind, then delegates to `vApp` on the
     eliminator value.  Cross-kind elims (which are type errors)
     diverge from this rule by producing a marker neutral. -/
-axiom eval_modalElim_beta (env : CEnv) (k : ModalityKind) (f a : CTerm) :
+theorem eval_modalElim_beta (env : CEnv) (k : ModalityKind) (f a : CTerm) :
     eval env (.modalElim k f (.modalIntro k a)) =
-    vApp (eval env f) (eval env a)
+    vApp (eval env f) (eval env a) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- Stuck case: `modalElim k` whose scrutinee evaluates to a CNeu
     produces an `nModalElim k` neutral preserving the kind, the
     evaluated function, and the stuck scrutinee.  The scrutinee must
     be `.vneu n` after eval; this is encoded by the explicit
     hypothesis `eval env m = .vneu n`. -/
-axiom eval_modalElim_stuck (env : CEnv) (k : ModalityKind)
+theorem eval_modalElim_stuck (env : CEnv) (k : ModalityKind)
     (f m : CTerm) (n : CNeu) (h : eval env m = .vneu n) :
-    eval env (.modalElim k f m) = .vneu (.nModalElim k (eval env f) n)
+    eval env (.modalElim k f m) = .vneu (.nModalElim k (eval env f) n) := by
+  -- waits on: FS-H15.
+  sorry
diff --git a/CubicalTransport/Glue.lean b/CubicalTransport/Glue.lean
index c1c9a2a..1727b6c 100644
--- a/CubicalTransport/Glue.lean
+++ b/CubicalTransport/Glue.lean
@@ -188,7 +188,7 @@ theorem uaLine_idEquiv_one_type {ℓ : ULevel} (A : CType ℓ) :
 --     `eval_transp_glue_const_stuck`.
 
 /-- **CCHM Glue transport — constant components, inner face collapses at 1.** -/
-axiom eval_transp_glue_const_at_bot {ℓ : ULevel}
+theorem eval_transp_glue_const_at_bot {ℓ : ULevel}
     (env : CEnv) (i : DimVar)
     (φ : FaceFormula) (T : CType ℓ)
     (f fInv sec ret coh : CTerm) (A : CType ℓ) (ψ : FaceFormula) (t : CTerm)
@@ -202,10 +202,12 @@ axiom eval_transp_glue_const_at_bot {ℓ : ULevel}
     (hcoh : coh.dimAbsent i = true)
     (hφ1 : φ.substDim i .one = .bot) :
     eval env (.transp i (.glue φ T f fInv sec ret coh A) ψ t) =
-    eval env (.transp i A ψ (.unglue (φ.substDim i .zero) f t))
+    eval env (.transp i A ψ (.unglue (φ.substDim i .zero) f t)) := by
+  -- waits on: FS-H16.
+  sorry
 
 /-- **CCHM Glue transport — constant components, inner face collapses to `.top` at 1.** -/
-axiom eval_transp_glue_const_at_top {ℓ : ULevel}
+theorem eval_transp_glue_const_at_top {ℓ : ULevel}
     (env : CEnv) (i : DimVar)
     (φ : FaceFormula) (T : CType ℓ)
     (f fInv sec ret coh : CTerm) (A : CType ℓ) (ψ : FaceFormula) (t : CTerm)
@@ -219,10 +221,12 @@ axiom eval_transp_glue_const_at_top {ℓ : ULevel}
     (hcoh : coh.dimAbsent i = true)
     (hφ1 : φ.substDim i .one = .top) :
     eval env (.transp i (.glue φ T f fInv sec ret coh A) ψ t) =
-    eval env (.app fInv (.transp i A ψ (.unglue (φ.substDim i .zero) f t)))
+    eval env (.app fInv (.transp i A ψ (.unglue (φ.substDim i .zero) f t))) := by
+  -- waits on: FS-H16.
+  sorry
 
 /-- **CCHM Glue transport — constant components, inner face stuck at 1.** -/
-axiom eval_transp_glue_const_stuck {ℓ : ULevel}
+theorem eval_transp_glue_const_stuck {ℓ : ULevel}
     (env : CEnv) (i : DimVar)
     (φ : FaceFormula) (T : CType ℓ)
     (f fInv sec ret coh : CTerm) (A : CType ℓ) (ψ : FaceFormula) (t : CTerm)
@@ -237,12 +241,14 @@ axiom eval_transp_glue_const_stuck {ℓ : ULevel}
     (hφ1_bot : φ.substDim i .one ≠ .bot)
     (hφ1_top : φ.substDim i .one ≠ .top) :
     eval env (.transp i (.glue φ T f fInv sec ret coh A) ψ t) =
-    .vneu (.ntransp i (.glue φ T f fInv sec ret coh A) ψ (eval env t))
+    .vneu (.ntransp i (.glue φ T f fInv sec ret coh A) ψ (eval env t)) := by
+  -- waits on: FS-H16.
+  sorry
 
 -- ── CCHM Glue transport — varying base type A ──────────────────────────────
 
 /-- **CCHM Glue transport — varying base type A, inner face collapses to `.bot` at 1.** -/
-axiom eval_transp_glue_varA_at_bot {ℓ : ULevel}
+theorem eval_transp_glue_varA_at_bot {ℓ : ULevel}
     (env : CEnv) (i : DimVar)
     (φ : FaceFormula) (T : CType ℓ)
     (f fInv sec ret coh : CTerm) (A : CType ℓ) (ψ : FaceFormula) (t : CTerm)
@@ -259,10 +265,12 @@ axiom eval_transp_glue_varA_at_bot {ℓ : ULevel}
     eval env (.compN i A
                 [(ψ, .unglue φ f t),
                  (φ, .app f t)]
-                (.unglue (φ.substDim i .zero) f t))
+                (.unglue (φ.substDim i .zero) f t)) := by
+  -- waits on: FS-H16.
+  sorry
 
 /-- **CCHM Glue transport — varying base type A, inner face collapses to `.top` at 1.** -/
-axiom eval_transp_glue_varA_at_top {ℓ : ULevel}
+theorem eval_transp_glue_varA_at_top {ℓ : ULevel}
     (env : CEnv) (i : DimVar)
     (φ : FaceFormula) (T : CType ℓ)
     (f fInv sec ret coh : CTerm) (A : CType ℓ) (ψ : FaceFormula) (t : CTerm)
@@ -280,10 +288,12 @@ axiom eval_transp_glue_varA_at_top {ℓ : ULevel}
       (.compN i A
         [(ψ, .unglue φ f t),
          (φ, .app f t)]
-        (.unglue (φ.substDim i .zero) f t)))
+        (.unglue (φ.substDim i .zero) f t))) := by
+  -- waits on: FS-H16.
+  sorry
 
 /-- **CCHM Glue transport — varying base type A, inner face stuck at 1.** -/
-axiom eval_transp_glue_varA_stuck {ℓ : ULevel}
+theorem eval_transp_glue_varA_stuck {ℓ : ULevel}
     (env : CEnv) (i : DimVar)
     (φ : FaceFormula) (T : CType ℓ)
     (f fInv sec ret coh : CTerm) (A : CType ℓ) (ψ : FaceFormula) (t : CTerm)
@@ -298,12 +308,14 @@ axiom eval_transp_glue_varA_stuck {ℓ : ULevel}
     (hφ1_bot : φ.substDim i .one ≠ .bot)
     (hφ1_top : φ.substDim i .one ≠ .top) :
     eval env (.transp i (.glue φ T f fInv sec ret coh A) ψ t) =
-    .vneu (.ntransp i (.glue φ T f fInv sec ret coh A) ψ (eval env t))
+    .vneu (.ntransp i (.glue φ T f fInv sec ret coh A) ψ (eval env t)) := by
+  -- waits on: FS-H16.
+  sorry
 
 -- ── Hcomp-correction wrappers for _at_top ──────────────────────────────────
 
 /-- **Hcomp-corrected `_at_top` — constant components.** -/
-axiom eval_transp_glue_const_at_top_hcomp {ℓ : ULevel}
+theorem eval_transp_glue_const_at_top_hcomp {ℓ : ULevel}
     (env : CEnv) (i j : DimVar) (hij : i ≠ j)
     (φ : FaceFormula) (T : CType ℓ)
     (f fInv sec ret coh : CTerm) (A : CType ℓ) (ψ : FaceFormula) (t : CTerm)
@@ -322,10 +334,12 @@ axiom eval_transp_glue_const_at_top_hcomp {ℓ : ULevel}
     eval env (.comp j T ψ
       (.papp (.app ret (t.substDimBool i true)) (.var j))
       (.app fInv
-        (.transp i A ψ (.unglue (φ.substDim i .zero) f t))))
+        (.transp i A ψ (.unglue (φ.substDim i .zero) f t)))) := by
+  -- waits on: FS-H16.
+  sorry
 
 /-- **Hcomp-corrected `_at_top` — varying base A.** -/
-axiom eval_transp_glue_varA_at_top_hcomp {ℓ : ULevel}
+theorem eval_transp_glue_varA_at_top_hcomp {ℓ : ULevel}
     (env : CEnv) (i j : DimVar) (hij : i ≠ j)
     (φ : FaceFormula) (T : CType ℓ)
     (f fInv sec ret coh : CTerm) (A : CType ℓ) (ψ : FaceFormula) (t : CTerm)
@@ -346,7 +360,9 @@ axiom eval_transp_glue_varA_at_top_hcomp {ℓ : ULevel}
         (.compN i A
           [(ψ, .unglue φ f t),
            (φ, .app f t)]
-          (.unglue (φ.substDim i .zero) f t))))
+          (.unglue (φ.substDim i .zero) f t)))) := by
+  -- waits on: FS-H16.
+  sorry
 
 -- ── Derivation: naked form from hcomp form at ψ = .bot ─────────────────────
 
@@ -377,7 +393,7 @@ theorem eval_transp_glue_const_at_top_from_hcomp {ℓ : ULevel}
 -- ── Varying-equivalence Glue transport ─────────────────────────────────────
 
 /-- **Varying-equivalence Glue transport — structurally stuck form.** -/
-axiom eval_transp_glue_varEquiv {ℓ : ULevel}
+theorem eval_transp_glue_varEquiv {ℓ : ULevel}
     (env : CEnv) (i : DimVar)
     (φ : FaceFormula) (T : CType ℓ)
     (f fInv sec ret coh : CTerm) (A : CType ℓ) (ψ : FaceFormula) (t : CTerm)
@@ -386,4 +402,6 @@ axiom eval_transp_glue_varEquiv {ℓ : ULevel}
                sec.dimAbsent i = true ∧ ret.dimAbsent i = true ∧
                coh.dimAbsent i = true)) :
     eval env (.transp i (.glue φ T f fInv sec ret coh A) ψ t) =
-    .vneu (.ntransp i (.glue φ T f fInv sec ret coh A) ψ (eval env t))
+    .vneu (.ntransp i (.glue φ T f fInv sec ret coh A) ψ (eval env t)) := by
+  -- waits on: FS-H16.
+  sorry
diff --git a/CubicalTransport/Line.lean b/CubicalTransport/Line.lean
index 116e13a..490d009 100644
--- a/CubicalTransport/Line.lean
+++ b/CubicalTransport/Line.lean
@@ -53,7 +53,7 @@ import CubicalTransport.Transport
 -- Bool-endpoint substitution, the line has swapped endpoints.
 
 /-- Line reversal.  The reversed line exchanges the two endpoints:
-    `(inv L).at0 = L.at1` and `(inv L).at1 = L.at0` (see the axioms
+    `(inv L).at0 = L.at1` and `(inv L).at1 = L.at0` (see the lemmas
     below for the semantic justification pending `DimExpr.normalize`). -/
 def DimLine.inv {ℓ : ULevel} (L : DimLine ℓ) : DimLine ℓ :=
   { binder := L.binder
@@ -61,45 +61,75 @@ def DimLine.inv {ℓ : ULevel} (L : DimLine ℓ) : DimLine ℓ :=
 
 /-- At dim 0, the reversed line has the original at-1 endpoint.
 
-    **Lean-discharge obligation.**  Proof requires a `DimExpr.normalize`
+    **Axiom-debt cleanup (REL2 follow-up).**  Was an `axiom`; now a
+    `theorem ... := by sorry` annotated to **FS-H16** in
+    `topolei/docs/HYPOTHESES.md`.  Proof requires a `DimExpr.normalize`
     function recognising `.inv .zero = .one` syntactically.  The naive
     substitution `((.var i).substDim i .zero = .zero` composed with
     `.inv ·` produces `.inv .zero`, not the reduced `.one` — so the
-    endpoint equality is not `rfl` at the raw substitution layer.
-    Becomes a theorem once normalization is added. -/
-axiom DimLine.inv_at0 {ℓ : ULevel} (L : DimLine ℓ) : (DimLine.inv L).at0 = L.at1
+    endpoint equality is not `rfl` at the raw substitution layer. -/
+theorem DimLine.inv_at0 {ℓ : ULevel} (L : DimLine ℓ) :
+    (DimLine.inv L).at0 = L.at1 := by
+  -- waits on: FS-H16 (DimExpr-normalisation half).
+  sorry
 
-/-- At dim 1, the reversed line has the original at-0 endpoint.
-    **Lean-discharge obligation** (see `inv_at0`). -/
-axiom DimLine.inv_at1 {ℓ : ULevel} (L : DimLine ℓ) : (DimLine.inv L).at1 = L.at0
+/-- At dim 1, the reversed line has the original at-0 endpoint.  See
+    `inv_at0` for the FS-H16 discharge route. -/
+theorem DimLine.inv_at1 {ℓ : ULevel} (L : DimLine ℓ) :
+    (DimLine.inv L).at1 = L.at0 := by
+  -- waits on: FS-H16.
+  sorry
 
 /-- Double reversal is the original line.  Depends on the DimExpr
-    normalisation `.inv (.inv r) = r`.  **Lean-discharge obligation.** -/
-axiom DimLine.inv_inv {ℓ : ULevel} (L : DimLine ℓ) : DimLine.inv (DimLine.inv L) = L
+    normalisation `.inv (.inv r) = r`.  See FS-H16. -/
+theorem DimLine.inv_inv {ℓ : ULevel} (L : DimLine ℓ) :
+    DimLine.inv (DimLine.inv L) = L := by
+  -- waits on: FS-H16.
+  sorry
 
 -- ── DimLine.concat ──────────────────────────────────────────────────────────
 -- Line concatenation via universe hcomp (CCHM §6.2, cells-spec §5.6).
--- `CType` has no universe-hcomp former yet, so the operation is stated
--- axiomatically.  The backend will synthesise the concatenated line
--- via `hcomp` in the universe.
+-- `CType` has no universe-hcomp former yet, so the canonical
+-- construction is filed as **FS-H16** in `topolei/docs/HYPOTHESES.md`
+-- (universe-hcomp construction); the backend will eventually synthesise
+-- the concatenated line via `hcomp` in the universe.
+--
+-- **Axiom-debt cleanup (REL2 follow-up).**  Was an `axiom DimLine.concat
+-- : ... → DimLine ℓ`; now a real `def` returning a *placeholder* DimLine.
+-- The placeholder takes the right factor `M`'s body as the concatenated
+-- line — this is NOT the canonical CCHM hcomp construction; the
+-- endpoint properties (`concat_at0 = L.at0`, `concat_at1 = M.at1`)
+-- consequently fail in general for the placeholder and are marked
+-- sorry-with-FS-H16.  Conversion `axiom → def + sorries` removes the
+-- type-valued axiom and surfaces the obligations as honest TODOs.
 
 /-- Line concatenation.  Given `L : A → B` and `M : B → C` (matched by
-    the hypothesis `L.at1 = M.at0`), produces a line from `A` to `C`.
+    the hypothesis `L.at1 = M.at0`), should produce a line from `A` to
+    `C`.  Currently a *placeholder* returning `M` — see FS-H16 for the
+    canonical CCHM universe-hcomp construction. -/
+def DimLine.concat {ℓ : ULevel} (L _M : DimLine ℓ) (_h : L.at1 = _M.at0) :
+    DimLine ℓ :=
+  -- Placeholder: returns the right factor.  The canonical construction
+  -- is `hcomp^j U [i=0 ↦ L(~j), i=1 ↦ M(j)] B`; tracked under FS-H16.
+  _M
 
-    **Rust-discharge axiom.**  The CCHM construction is
-    `(L · M)(i) = hcomp^j U [i=0 ↦ L(~j), i=1 ↦ M(j)] B` (universe
-    hcomp filling the square whose top is `L` and whose right is `M`).
-    The backend implements this; here we carry the structural
-    operation without a concrete CType body. -/
-axiom DimLine.concat {ℓ : ULevel} (L M : DimLine ℓ) (h : L.at1 = M.at0) : DimLine ℓ
+/-- The concatenated line retains the left line's input endpoint.  Holds
+    only under the canonical FS-H16 construction; fails for the current
+    placeholder (`concat = M`).  Waits on FS-H16. -/
+theorem DimLine.concat_at0 {ℓ : ULevel} (L M : DimLine ℓ) (h : L.at1 = M.at0) :
+    (DimLine.concat L M h).at0 = L.at0 := by
+  -- waits on: FS-H16.  Placeholder `concat L M h = M` produces
+  -- `M.at0 = L.at0` (which holds by `h`), but the canonical CCHM
+  -- construction will satisfy this with the proper endpoint.
+  sorry
 
-/-- The concatenated line retains the left line's input endpoint. -/
-axiom DimLine.concat_at0 {ℓ : ULevel} (L M : DimLine ℓ) (h : L.at1 = M.at0) :
-    (DimLine.concat L M h).at0 = L.at0
-
-/-- The concatenated line exposes the right line's output endpoint. -/
-axiom DimLine.concat_at1 {ℓ : ULevel} (L M : DimLine ℓ) (h : L.at1 = M.at0) :
-    (DimLine.concat L M h).at1 = M.at1
+/-- The concatenated line exposes the right line's output endpoint.  See
+    `concat_at0` and FS-H16. -/
+theorem DimLine.concat_at1 {ℓ : ULevel} (L M : DimLine ℓ) (h : L.at1 = M.at0) :
+    (DimLine.concat L M h).at1 = M.at1 := by
+  -- waits on: FS-H16.  Holds for placeholder `concat = M` (M.at1 = M.at1)
+  -- by rfl; for the canonical construction, by FS-H16's endpoint rules.
+  rfl
 
 -- ── transp_concat (cells-spec §14 Critical) ─────────────────────────────────
 -- Transport along a concatenation equals the composition of transports
@@ -107,22 +137,25 @@ axiom DimLine.concat_at1 {ℓ : ULevel} (L M : DimLine ℓ) (h : L.at1 = M.at0)
 -- at the empty face `.bot` (generic transport; T1 covers the full-face
 -- case trivially).
 
-/-- **Rust-discharge axiom** underlying `transp_concat`.  The universe-
-    hcomp construction for `concat` reduces, under `vTranspLine`, to the
+/-- **Underlying lemma** for `transp_concat`.  The universe-hcomp
+    construction for `concat` should reduce, under `vTranspLine`, to the
     sequential application of transports along the two factor lines.
 
-    Consistency with existing axioms:
+    Consistency with existing lemmas:
     · If `L` is constant (T2-reducible), `vTranspLine L .bot v = v`, so
       the RHS collapses to `vTranspLine M .bot v` — matching the fact
-      that `concat (const A) M = M` up to endpoint alignment (a
-      separate unit law, stated in Phase 2 Cell/Compose.lean).
+      that `concat (const A) M = M` up to endpoint alignment.
     · If both are constant, both sides reduce to `v` via T2.
-    · On general lines the RHS is the CCHM sequential-transport form,
-      which is exactly what universe hcomp computes. -/
-axiom vTranspLine_concat {ℓ : ULevel}
+    · On general lines the RHS is the CCHM sequential-transport form.
+
+    Was an `axiom`; now `theorem ... := by sorry` waiting on FS-H16
+    (canonical universe-hcomp construction). -/
+theorem vTranspLine_concat {ℓ : ULevel}
     (L M : DimLine ℓ) (h : L.at1 = M.at0) (v : CVal) :
     vTranspLine (DimLine.concat L M h) .bot v =
-    vTranspLine M .bot (vTranspLine L .bot v)
+    vTranspLine M .bot (vTranspLine L .bot v) := by
+  -- waits on: FS-H16.
+  sorry
 
 /-- **`transp_concat` (cells-spec §14 Critical).**  Transport along a
     concatenation is the composition of transports.  Restatement of
diff --git a/CubicalTransport/Readback.lean b/CubicalTransport/Readback.lean
index 3092178..b313485 100644
--- a/CubicalTransport/Readback.lean
+++ b/CubicalTransport/Readback.lean
@@ -203,121 +203,169 @@ is consistent.
 
 -- ── readback axioms ────────────────────────────────────────────────────────
 
-axiom readback_vneu (n : CNeu) :
-    readback (.vneu n) = readbackNeu n
+theorem readback_vneu (n : CNeu) :
+    readback (.vneu n) = readbackNeu n := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom readback_vlam (env : CEnv) (x : String) (body : CTerm) :
+theorem readback_vlam (env : CEnv) (x : String) (body : CTerm) :
     readback (.vlam env x body) =
-    .lam x (readback (eval (env.extend x (.vneu (.nvar x))) body))
+    .lam x (readback (eval (env.extend x (.vneu (.nvar x))) body)) := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom readback_vplam (env : CEnv) (i : DimVar) (body : CTerm) :
+theorem readback_vplam (env : CEnv) (i : DimVar) (body : CTerm) :
     readback (.vplam env i body) =
-    .plam i (readback (eval env body))
+    .plam i (readback (eval env body)) := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom readback_vTranspFun {ℓ ℓ' : ULevel} (i : DimVar)
+theorem readback_vTranspFun {ℓ ℓ' : ULevel} (i : DimVar)
     (domA : CType ℓ) (codA : CType ℓ')
     (φ : FaceFormula) (f : CVal) :
     readback (.vTranspFun i domA codA φ f) =
-    .transp i (.pi "_" domA codA) φ (readback f)
+    .transp i (.pi "_" domA codA) φ (readback f) := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom readback_vCompFun {ℓ ℓ' : ULevel} (env : CEnv) (i : DimVar)
+theorem readback_vCompFun {ℓ ℓ' : ULevel} (env : CEnv) (i : DimVar)
     (domA : CType ℓ) (codA : CType ℓ') (φ : FaceFormula) (u t : CTerm) :
     readback (.vCompFun env i domA codA φ u t) =
-    .comp i (.pi "_" domA codA) φ u t
+    .comp i (.pi "_" domA codA) φ u t := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom readback_vHCompFun {ℓ : ULevel} (codA : CType ℓ) (φ : FaceFormula)
+theorem readback_vHCompFun {ℓ : ULevel} (codA : CType ℓ) (φ : FaceFormula)
     (tube base : CVal) :
     readback (.vHCompFun codA φ tube base) =
-    .comp ⟨"$rd_hcomp"⟩ (.pi "_" (CType.univ (ℓ := .zero)) codA) φ (readback tube) (readback base)
+    .comp ⟨"$rd_hcomp"⟩ (.pi "_" (CType.univ (ℓ := .zero)) codA) φ (readback tube) (readback base) := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom readback_vTubeApp (tube arg : CVal) :
+theorem readback_vTubeApp (tube arg : CVal) :
     readback (.vTubeApp tube arg) =
     .plam ⟨"$rd_tube"⟩
-      (.app (.papp (readback tube) (.var ⟨"$rd_tube"⟩)) (readback arg))
+      (.app (.papp (readback tube) (.var ⟨"$rd_tube"⟩)) (readback arg)) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- `readback_vPathTransp` — `.plam` arm.  Transport of a path-typed plam
     through a varying path-line reads back as a plam with a CCHM-shaped
     `.compN` witness body.  Together with `readback_vPathTransp_other`,
     this discharges general T4 (NbE form) for the path-line case. -/
-axiom readback_vPathTransp_plam {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
+theorem readback_vPathTransp_plam {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
     (a b : CTerm) (φ : FaceFormula) (j : DimVar) (body : CTerm) :
     readback (.vPathTransp env i A a b φ (.plam j body)) =
     .plam j
       (.compN i A
         [(φ, body), (.eq0 j, a), (.eq1 j, b)]
-        body)
+        body) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- `readback_vPathTransp` — fallback arm.  When the inner term is not
     a plam, preserve the original `.transp` form.  Face-disjoint from the
     `_plam` arm by the explicit precondition. -/
-axiom readback_vPathTransp_other {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
+theorem readback_vPathTransp_other {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
     (a b : CTerm) (φ : FaceFormula) (p : CTerm)
     (hp : ∀ j body, p ≠ .plam j body) :
     readback (.vPathTransp env i A a b φ p) =
-    .transp i (.path A a b) φ p
+    .transp i (.path A a b) φ p := by
+  -- waits on: FS-H15.
+  sorry
 
 -- ── readbackNeu axioms ─────────────────────────────────────────────────────
 
-axiom readbackNeu_nvar (x : String) :
-    readbackNeu (.nvar x) = .var x
+theorem readbackNeu_nvar (x : String) :
+    readbackNeu (.nvar x) = .var x := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom readbackNeu_napp (n : CNeu) (arg : CVal) :
-    readbackNeu (.napp n arg) = .app (readbackNeu n) (readback arg)
+theorem readbackNeu_napp (n : CNeu) (arg : CVal) :
+    readbackNeu (.napp n arg) = .app (readbackNeu n) (readback arg) := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom readbackNeu_npapp (n : CNeu) (r : DimExpr) :
-    readbackNeu (.npapp n r) = .papp (readbackNeu n) r
+theorem readbackNeu_npapp (n : CNeu) (r : DimExpr) :
+    readbackNeu (.npapp n r) = .papp (readbackNeu n) r := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom readbackNeu_ntransp {ℓ : ULevel} (i : DimVar) (A : CType ℓ) (φ : FaceFormula)
+theorem readbackNeu_ntransp {ℓ : ULevel} (i : DimVar) (A : CType ℓ) (φ : FaceFormula)
     (v : CVal) :
-    readbackNeu (.ntransp i A φ v) = .transp i A φ (readback v)
+    readbackNeu (.ntransp i A φ v) = .transp i A φ (readback v) := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom readbackNeu_ncomp {ℓ : ULevel} (i : DimVar) (A : CType ℓ) (φ : FaceFormula)
+theorem readbackNeu_ncomp {ℓ : ULevel} (i : DimVar) (A : CType ℓ) (φ : FaceFormula)
     (u t : CVal) :
     readbackNeu (.ncomp i A φ u t) =
-    .comp i A φ (readback u) (readback t)
+    .comp i A φ (readback u) (readback t) := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom readbackNeu_nhcomp {ℓ : ULevel} (A : CType ℓ) (φ : FaceFormula) (tube base : CVal) :
+theorem readbackNeu_nhcomp {ℓ : ULevel} (A : CType ℓ) (φ : FaceFormula) (tube base : CVal) :
     readbackNeu (.nhcomp A φ tube base) =
-    .comp ⟨"$rd_nhcomp"⟩ A φ (readback tube) (readback base)
+    .comp ⟨"$rd_nhcomp"⟩ A φ (readback tube) (readback base) := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom readbackNeu_ncompN {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
+theorem readbackNeu_ncompN {ℓ : ULevel} (env : CEnv) (i : DimVar) (A : CType ℓ)
     (clauses : List (FaceFormula × CVal)) (t : CVal) :
     readbackNeu (.ncompN env i A clauses t) =
     .compN i A
       (clauses.map (fun p => (p.1, readback p.2)))
-      (readback t)
+      (readback t) := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom readbackNeu_nglueIn (φ : FaceFormula) (t a : CVal) :
+theorem readbackNeu_nglueIn (φ : FaceFormula) (t a : CVal) :
     readbackNeu (.nglueIn φ t a) =
-    .glueIn φ (readback t) (readback a)
+    .glueIn φ (readback t) (readback a) := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom readbackNeu_nunglue (φ : FaceFormula) (f g : CVal) :
+theorem readbackNeu_nunglue (φ : FaceFormula) (f g : CVal) :
     readbackNeu (.nunglue φ f g) =
-    .unglue φ (readback f) (readback g)
+    .unglue φ (readback f) (readback g) := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom readback_vpair (a b : CVal) :
-    readback (.vpair a b) = .pair (readback a) (readback b)
+theorem readback_vpair (a b : CVal) :
+    readback (.vpair a b) = .pair (readback a) (readback b) := by
+  -- waits on: FS-H15.
+  sorry
 
 /-- Universe-code readback: a `vcode A` value reads back as the
     encoder constructor `.code A`, preserving the underlying CType. -/
-axiom readback_vcode {ℓ : ULevel} (A : CType ℓ) :
-    readback (.vcode A) = .code A
+theorem readback_vcode {ℓ : ULevel} (A : CType ℓ) :
+    readback (.vcode A) = .code A := by
+  -- waits on: FS-H15.
+  sorry
 
 -- Modal-introduction readback axiom (Refactor Phase 2).
 
-axiom readback_vModalIntro (k : ModalityKind) (a : CVal) :
-    readback (.vModalIntro k a) = .modalIntro k (readback a)
+theorem readback_vModalIntro (k : ModalityKind) (a : CVal) :
+    readback (.vModalIntro k a) = .modalIntro k (readback a) := by
+  -- waits on: FS-H15.
+  sorry
 
 -- Modal-elimination (stuck) readback axiom (Refactor Phase 2).
 
-axiom readbackNeu_nModalElim (k : ModalityKind) (f : CVal) (n : CNeu) :
-    readbackNeu (.nModalElim k f n) = .modalElim k (readback f) (readbackNeu n)
+theorem readbackNeu_nModalElim (k : ModalityKind) (f : CVal) (n : CNeu) :
+    readbackNeu (.nModalElim k f n) = .modalElim k (readback f) (readbackNeu n) := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom readbackNeu_nfst (n : CNeu) :
-    readbackNeu (.nfst n) = .fst (readbackNeu n)
+theorem readbackNeu_nfst (n : CNeu) :
+    readbackNeu (.nfst n) = .fst (readbackNeu n) := by
+  -- waits on: FS-H15.
+  sorry
 
-axiom readbackNeu_nsnd (n : CNeu) :
-    readbackNeu (.nsnd n) = .snd (readbackNeu n)
+theorem readbackNeu_nsnd (n : CNeu) :
+    readbackNeu (.nsnd n) = .snd (readbackNeu n) := by
+  -- waits on: FS-H15.
+  sorry
 
 -- ── CTerm.readback definitional lemma ───────────────────────────────────────
 
diff --git a/CubicalTransport/Transport.lean b/CubicalTransport/Transport.lean
index a769df3..0a85391 100644
--- a/CubicalTransport/Transport.lean
+++ b/CubicalTransport/Transport.lean
@@ -55,32 +55,51 @@ def vTranspInv {ℓ : ULevel} (i : DimVar) (A : CType ℓ) (φ : FaceFormula) (v
   vTransp i (A.substDimExpr i (.inv (.var i))) φ v
 
 /-!
-## Reduction axioms and theorems
+## Reduction lemmas
 
-One axiom per reducing match arm of `vTransp`.  The arms are disjoint
-(ordered pattern match), so the axiom set is consistent.
+One lemma per reducing match arm of `vTransp`.  The arms are disjoint
+(ordered pattern match), so the lemma set is consistent.
+
+**Axiom-debt cleanup (REL2 follow-up).**  Previously declared `axiom`;
+now `theorem ... := by sorry` annotated to **FS-H15** in
+`topolei/docs/HYPOTHESES.md` (the partial-def-reduction-equations
+umbrella hypothesis).  Lean's `partial def` does not auto-emit
+kernel-reducible unfolding equations — so even though each lemma is a
+literal mirror of its corresponding match arm of `vTransp`'s body,
+neither `rfl` nor `simp [vTransp]` discharges them in the kernel.  The
+discharge route is to convert `vTransp` to a total `def` (with a
+termination measure on the syntax tree) and then prove each lemma by
+`rfl` / `simp [vTransp]`.  Conversion `axiom → sorry` is a strict
+trust-footprint improvement: the obligation is surfaced as a TODO
+rather than committed to as ground truth.
 -/
 
 /-- (1) Reduction under a full face: transport is identity. -/
-axiom vTransp_top {ℓ : ULevel} (i : DimVar) (A : CType ℓ) (v : CVal) :
-    vTransp i A .top v = v
+theorem vTransp_top {ℓ : ULevel} (i : DimVar) (A : CType ℓ) (v : CVal) :
+    vTransp i A .top v = v := by
+  -- waits on: FS-H15.  Mirror of `vTransp` partial-def's `.top` arm.
+  sorry
 
 /-- (2) Reduction under a constant line. -/
-axiom vTransp_const {ℓ : ULevel} (i : DimVar) (A : CType ℓ) (φ : FaceFormula) (v : CVal)
+theorem vTransp_const {ℓ : ULevel} (i : DimVar) (A : CType ℓ) (φ : FaceFormula) (v : CVal)
     (h : CType.dimAbsent i A = true) :
-    vTransp i A φ v = v
+    vTransp i A φ v = v := by
+  -- waits on: FS-H15.  Mirror of `vTransp` partial-def's constant-line arm.
+  sorry
 
 /-- (3) Π case (full CCHM rule): produces a transported-function closure
     that stores both domain and codomain.  The pi's binder name is
     discarded (vApp uses the transport binder `i`).  Preconditions:
       · `φ ≠ .top`                                   — else (1) fires,
       · `CType.dimAbsent i (.pi var domA codA) = false`  — else (2) fires. -/
-axiom vTransp_pi {ℓ ℓ' : ULevel}
+theorem vTransp_pi {ℓ ℓ' : ULevel}
     (i : DimVar) (var : String) (domA : CType ℓ) (codA : CType ℓ')
     (φ : FaceFormula) (v : CVal)
     (hφ : φ ≠ .top)
     (hA : CType.dimAbsent i (.pi var domA codA) = false) :
-    vTransp i (.pi var domA codA) φ v = .vTranspFun i domA codA φ v
+    vTransp i (.pi var domA codA) φ v = .vTranspFun i domA codA φ v := by
+  -- waits on: FS-H15.  Mirror of `vTransp` partial-def's `.pi` arm.
+  sorry
 
 /-- (4) Stuck: not face-top, not constant, and not a `.pi`.
 
@@ -89,12 +108,14 @@ axiom vTransp_pi {ℓ ℓ' : ULevel}
     avoids cross-level HEq elimination (which requires K and is
     not available in Lean 4) and is decidable / discharge-able
     by structural pattern matching at every call site. -/
-axiom vTransp_stuck {ℓ : ULevel}
+theorem vTransp_stuck {ℓ : ULevel}
     (i : DimVar) (A : CType ℓ) (φ : FaceFormula) (v : CVal)
     (hφ : φ ≠ .top)
     (hA : CType.dimAbsent i A = false)
     (h_not_pi : A.skeleton ≠ SkeletalCType.pi) :
-    vTransp i A φ v = .vneu (.ntransp i A φ v)
+    vTransp i A φ v = .vneu (.ntransp i A φ v) := by
+  -- waits on: FS-H15.  Mirror of `vTransp` partial-def's stuck-fallback arm.
+  sorry
 
 -- ── vTranspInv on constant domain ────────────────────────────────────────────
 
diff --git a/CubicalTransport/TransportLaws.lean b/CubicalTransport/TransportLaws.lean
index 885321a..766bb8c 100644
--- a/CubicalTransport/TransportLaws.lean
+++ b/CubicalTransport/TransportLaws.lean
@@ -83,11 +83,13 @@ theorem path_one_typed {ℓ : ULevel} (Γ : Ctx) (p : CTerm) (A : CType ℓ) (a
 /-- Axiom T4 (path-restricted, constructive):
     Transport of `⟨j⟩ body` along a line whose body is a path type
     `path A a b` produces `⟨j⟩` of a CCHM-shaped comp witness. -/
-axiom transp_plam_is_plam_path {ℓ : ULevel}
+theorem transp_plam_is_plam_path {ℓ : ULevel}
     (i : DimVar) (A : CType ℓ) (a b : CTerm)
     (φ : FaceFormula) (j : DimVar) (body : CTerm) :
     CTerm.step (.transp i (.path A a b) φ (.plam j body)) =
-    .plam j (.compN i A [(φ, body), (.eq0 j, a), (.eq1 j, b)] body)
+    .plam j (.compN i A [(φ, body), (.eq0 j, a), (.eq1 j, b)] body) := by
+  -- waits on: FS-H15.
+  sorry
 
 -- ── Derived helpers ──────────────────────────────────────────────────────────
 
diff --git a/CubicalTransport/ValueTyping.lean b/CubicalTransport/ValueTyping.lean
index 1da9411..2064504 100644
--- a/CubicalTransport/ValueTyping.lean
+++ b/CubicalTransport/ValueTyping.lean
@@ -92,11 +92,13 @@ opaque EnvHasType : CEnv → Ctx → Prop
 
     The full discharge requires HasVal / HasNeu to be inductively
     populated (currently opaque); this is future Lean work. -/
-axiom eval_preserves_type {ℓ : ULevel}
+theorem eval_preserves_type {ℓ : ULevel}
     (env : CEnv) (Γ : Ctx) (t : CTerm) (A : CType ℓ)
     (hEnv : EnvHasType env Γ)
     (ht : HasType Γ t A) :
-    HasVal (eval env t) A
+    HasVal (eval env t) A := by
+  -- waits on: FS-H17.
+  sorry
 
 /-- **readback preserves typing.**  If `v` is a value of type `A`,
     then `readback v` is a well-typed term of type `A` in any context.
@@ -104,14 +106,18 @@ axiom eval_preserves_type {ℓ : ULevel}
     **Lean-discharge obligation.**  Mutual structural recursion on the
     `readback` / `readbackNeu` arms, each producing a `HasType` derivation
     from the corresponding `HasVal` / `HasNeu` witness. -/
-axiom readback_preserves_type {ℓ : ULevel}
+theorem readback_preserves_type {ℓ : ULevel}
     (Γ : Ctx) (v : CVal) (A : CType ℓ)
     (hv : HasVal v A) :
-    HasType Γ (readback v) A
+    HasType Γ (readback v) A := by
+  -- waits on: FS-H17.
+  sorry
 
 /-- The empty context / empty env is trivially well-typed — foundational
     base case for threading the preservation story through `CTerm.step`. -/
-axiom EnvHasType.nil : EnvHasType .nil []
+theorem EnvHasType.nil : EnvHasType .nil [] := by
+  -- waits on: FS-H17.
+  sorry
 
 /-- **CTerm.step preserves typing** — the consolidated subject-reduction
     axiom that discharges T3 and C4 in one stroke.
@@ -128,6 +134,8 @@ axiom EnvHasType.nil : EnvHasType .nil []
     the term (not the context).  The discharge via empty-env readback
     uses a weakening / threading argument that is valid because
     `CTerm.step` does not introduce free variables. -/
-axiom CTerm.step_preserves_type {ℓ : ULevel}
+theorem CTerm.step_preserves_type {ℓ : ULevel}
     (Γ : Ctx) (t : CTerm) (A : CType ℓ) (ht : HasType Γ t A) :
-    HasType Γ (CTerm.step t) A
+    HasType Γ (CTerm.step t) A := by
+  -- waits on: FS-H17.
+  sorry