docs(abi): propagate open-ended progressive framing to source-level comments

ROADMAP.adoc and README.adoc already have the correct framing (TypeLL is
open-ended, L1-L10 is the initial checked set, not a ceiling).  This commit
propagates that framing into the source files that still described L10 as
the permanent top:

- LevelMonotonicity.idr: "defines 10 levels" → "initial checked set (L1-L10);
  open-ended — new levels added as theory demands; L10 is current top, not cap"
- Soundness.idr: "(10 levels, QTT …)" → "(initial L1-L10 levels; open-ended …)"
- src/abi/README.md: "10-level hierarchy" → "L1-L10 initial checked set; open-ended";
  "L10 is top" → "L10 is current top (open-ended above)"
- tests/integration_test.rs: "all 10 levels" → "all L1-L10 levels (initial checked set)"

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

src/abi/LevelMonotonicity.idr

@@ -1,10 +1,13 @@
 -- SPDX-License-Identifier: PMPL-1.0-or-later
 -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 --
-||| TypeLL 10-Level Type Safety Hierarchy — Monotonicity Proofs
+||| TypeLL Progressive Type Safety Hierarchy — Monotonicity Proofs
 |||
-||| The TypeLL level system defines 10 levels of type safety:
+||| TypeLL is an open-ended progressive framework: levels are added as the
+||| type theory demands, with no fixed upper bound.  The initial checked
+||| set (L1-L10) is defined below; L10 is the current top, not a ceiling.
 |||
+||| Initial checked set (L1-L10):
 |||   L1  : Parse-time safety         (well-formed AST)
 |||   L2  : Schema-binding safety     (named type resolution)
 |||   L3  : Type-compatible operations (unification + operator checking)

src/abi/README.md

@@ -15,7 +15,7 @@ abi/
 ├── Foreign.idr             # FFI declarations for the Zig layer (libtypell)
 ├── Soundness.idr           # Progress + Preservation proofs for core calculus
 ├── InferenceSoundness.idr  # Unification + type inference soundness proofs
-└── LevelMonotonicity.idr   # 10-level hierarchy monotonicity proofs (L1-L10)
+└── LevelMonotonicity.idr   # L1-L10 hierarchy monotonicity proofs (initial checked set; open-ended above)
 ```
 
 ## Soundness Proofs
@@ -33,13 +33,14 @@ Models unification (`unify.rs`) and inference (`infer.rs`).
 - **Substitution idempotence**: MGU applied twice equals MGU applied once
 - **Arrow decomposition**: unifying function types decomposes to component unification
 
-### LevelMonotonicity.idr — 10-Level Hierarchy
-Models the L1-L10 type safety hierarchy from `ROADMAP.adoc`.
+### LevelMonotonicity.idr — Progressive Level Hierarchy (initial L1-L10)
+Models the L1-L10 type safety hierarchy from `ROADMAP.adoc`. TypeLL is open-ended;
+L1-L10 is the current checked set, not a fixed ceiling.
 - **Level total order**: any two levels are comparable
 - **Strict increase**: each level strictly subsumes the previous
 - **Feature monotonicity**: higher levels include all lower-level features
 - **No downgrade**: programs requiring level N features cannot be checked at level M < N
-- **Lattice bounds**: L1 is bottom, L10 is top
+- **Lattice bounds**: L1 is bottom, L10 is the current top (open-ended above)
 
 ## Planned Modules
 

src/abi/Soundness.idr

@@ -18,9 +18,10 @@
 ||| Together these establish type safety: well-typed programs do not get stuck.
 |||
 ||| These proofs model the core calculus underlying typell-core's check.rs,
-||| infer.rs, and unify.rs. The full TypeLL type system (10 levels, QTT,
-||| sessions, effects, dimensions) extends this core; level-specific proofs
-||| are in LevelMonotonicity.idr.
+||| infer.rs, and unify.rs. The full TypeLL type system (initial L1-L10
+||| levels; open-ended progressive — new levels added as theory demands;
+||| QTT, sessions, effects, dimensions) extends this core; level-specific
+||| proofs are in LevelMonotonicity.idr.
 |||
 ||| @see check.rs  — TypeChecker orchestration
 ||| @see infer.rs  — Bidirectional type inference

tests/integration_test.rs

@@ -5,7 +5,7 @@
 //
 // Exercises the full pipeline: TypeLL core -> VCL bridge -> level checking.
 // Verifies that:
-// - A VCL query type-checks through all 10 levels
+// - A VCL query type-checks through all L1-L10 levels (initial checked set; TypeLL is open-ended above)
 // - Higher levels require lower levels to pass first
 // - The TypeChecker, VCL bridge, and safety level determination work together
 // - Full round-trip: VCL query -> UnifiedType -> TypeChecker -> CheckResult
@@ -37,8 +37,8 @@ use typell_vql::rules::{
 // Full pipeline: VCL -> TypeLL core -> level checking
 // ============================================================================
 
-/// Build a fully-annotated VCL query that passes all 10 levels,
-/// then verify it through the full TypeLL pipeline.
+/// Build a fully-annotated VCL query that passes all L1-L10 levels
+/// (the initial checked set), then verify it through the full TypeLL pipeline.
 #[test]
 fn test_full_pipeline_level_10_query() {
     // Step 1: Construct a VCL query with all extensions.