feat(v3): T-Numeric-Construction S9 Slice 2.5 — predicate registry + PB-1 shim retirement

dsl/std/integer.dag

@@ -110,27 +110,31 @@ type UInt128 = Semiring<Word128>
 type Int = AbelianGroup<GroupCompletion<Nat>>
 type UInt = Nat
 
-// Nat-alignment refinement (S9 Slice 2 / Phase-4, partial).
+// Nat-alignment refinements (S9 Slice 2 / Slice 2.5 / Phase-4).
+//
 // NonNegativeInt formerly lived in dsl/std/types.dag refining Int with a
-// non-negative range predicate. Slice 2 Nat-alignment (dispatch
-// gunbc#1739 issuecomment-4389870320) migrates the algebra-side carrier to
-// Nat: non-negativity is structural to Nat by construction (the canonical
-// natural-number carrier), not a refinement over Int. Refining Int for
-// non-negativity projects out Nat's structural property — the same modeling
-// fault Codex's BLOCKING review on PR #1818 caught for UInt as a
-// CommutativeMonoid wrap of Nat. Declared here (not in std.types) because
-// this module imports std.nat directly; locating in std.types would require
-// an std.types to std.nat import edge that triggers a circular-dependency
-// false-positive during transitive load of test fixtures via std.render
-// chains.
-//
-// PositiveInt remains in std.types refining Int for this slice — the
-// resolver does not currently entail predicate ranges over Nat (only over
-// Int and Int-row carriers). Per dispatch STOP-AND-ESCALATE bullet 2
-// (predicate-entailment failure), surfacing as a gap; PositiveInt's
-// Nat-alignment sequences after predicate-entailment substrate supports
-// ranges over Nat.
+// non-negative range predicate. Slice 2 Nat-alignment migrates the
+// algebra-side carrier to Nat: non-negativity is structural to Nat by
+// construction (the canonical natural-number carrier), not a refinement
+// over Int. Refining Int for non-negativity projects out Nat's structural
+// property — the same modeling fault Codex's BLOCKING review on PR #1818
+// caught for UInt as a CommutativeMonoid wrap of Nat. Declared here (not
+// in std.types) because this module imports std.nat directly; locating in
+// std.types would require an std.types to std.nat import edge that
+// triggers a circular-dependency false-positive during transitive load of
+// test fixtures via std.render chains.
+//
+// PositiveInt migrates to Nat-where-gt_zero per S9 Slice 2.5 (Path 3
+// RATIFIED at gunbc#828 issuecomment-4390333451). The gt_zero primitive
+// IS the reason for "Nat without zero" / "Nat above structural bound"
+// (Director Option 2 ratification at gunbc#828 issuecomment-4390199218);
+// the prior range(min: 1) over Int was a misleading label that treated
+// Nat's lower-bound = 0 as a contingent rather than structural fact.
+// gt_zero is enrolled in the lowerer's predicate registry
+// (KNOWN_PREDICATES in src/v3/compiler/src/lower.rs), which
+// retired the prior PB-1 file-path special case.
 type NonNegativeInt = Nat
+type PositiveInt    = Nat where gt_zero
 
 // ─── Diagnostic enumeration order (Modeling problem 4; slice 2) ─────────────
 //

dsl/std/types.dag

@@ -227,32 +227,43 @@ type Map<key, value> = PartialFunction<key, value>
 //   2. Auto-generation of test inputs (valid from [T], invalid from [T]^c)
 //   3. Documentation of expected shapes
 
-type CommitSha    = String where pattern("^[a-f0-9]\{40\}$")
-type Sha256       = String where pattern("^[a-f0-9]\{64\}$")
+// S9 Slice 2.5 (Director Option A revised RATIFIED at gunbc#828
+// `issuecomment-4392245968`): pattern / format / content predicates are
+// structurally absent from the predicate registry until Q-Regex-Primitive
+// substrate-fact-introduction lands. The where-clauses on the types below
+// dropped from this slice; restore the original predicate when the
+// registry re-includes pattern / format / content. The original
+// where-clause text appears in each type's preceding comment for the
+// restoration receipt.
+//
+// CommitSha: restore `where pattern("^[a-f0-9]{40}$")` post-Q-Regex.
+type CommitSha    = String
+// Sha256: restore `where pattern("^[a-f0-9]{64}$")` post-Q-Regex.
+type Sha256       = String
 type RetryCount   = Int where range(min: 1, max: 5)
 type HttpStatus   = Int where range(min: 100, max: 599)
-type Email        = String where pattern("^[^@]+@[^@]+\\.[^@]+$")
+// Email: restore `where pattern("^[^@]+@[^@]+\\.[^@]+$")` post-Q-Regex.
+type Email        = String
 type Port         = Int where range(min: 1, max: 65535)
-type GistId       = String where format(uuid)
+// GistId: restore `where format(uuid)` post-Q-Regex (format predicate
+// re-enrolled).
+type GistId       = String
 type Secret       nominal_opaque = String
 type SecretValue  = Secret where non_empty
-type Url          = String where pattern("^https?://")
-type SemVer       = String where pattern("^\\d+\\.\\d+\\.\\d+")
+// Url: restore `where pattern("^https?://")` post-Q-Regex.
+type Url          = String
+// SemVer: restore `where pattern("^\\d+\\.\\d+\\.\\d+")` post-Q-Regex.
+type SemVer       = String
 type NonEmptyStr     = String where non_empty
 type LanguageId      = String where non_empty
 type SecretName      = String where non_empty
-// `NonNegativeInt` migrated to `Nat` (canonical-instance alias) per S9 Slice 2
-// Nat-alignment — declaration moved to `dsl/std/integer.dag` (which already
-// imports `std.nat { Nat }`); locating it here would require an
-// `std.types -> std.nat` import edge that triggers a circular-dependency
-// false-positive during transitive load of test fixtures via `std.render`
-// chains. Consumers should `import std.integer { NonNegativeInt }`.
-//
-// `PositiveInt` STAYS on `Int where range(min: 1)` here for this slice;
-// resolver does not currently entail `where range(min: …)` predicates over
-// `Nat`. Surfaced as a gap per dispatch STOP-AND-ESCALATE; migration
-// sequences after predicate-entailment substrate supports `range` over Nat.
-type PositiveInt     = Int where range(min: 1)
+// `NonNegativeInt` and `PositiveInt` migrated to Nat-based shapes per S9
+// Slice 2 / Slice 2.5; declarations now live in `dsl/std/integer.dag`
+// (which already imports `std.nat { Nat }`) — locating them here would
+// require an `std.types -> std.nat` import edge that triggers a
+// circular-dependency false-positive during transitive load of test
+// fixtures via `std.render` chains. Consumers should
+// `import std.integer { NonNegativeInt, PositiveInt }`.
 
 // Path modeling (EX-2):
 // - FilePath remains a compatibility alias for existing modules.
@@ -287,7 +298,8 @@ type SourceSpan {
   end: Int
 }
 
-type Timestamp    = String where pattern("^\\d\{4\}-\\d\{2\}-\\d\{2\}T\\d\{2\}:\\d\{2\}:\\d\{2\}")
+// Timestamp: restore `where pattern("^\\d{4}-\\d{2}-\\d{2}T\\d{2}:\\d{2}:\\d{2}")` post-Q-Regex.
+type Timestamp    = String
 type EpochMs       = Int where range(min: 0)
 type Duration      = Int where range(min: 0)
 type Milliseconds  = Int where range(min: 0), brand("Milliseconds")
@@ -320,8 +332,11 @@ type GitRef       = String where non_empty
 // but a ref is not always a SHA (e.g., "main", "HEAD~1").
 
 // --- GCP / OIDC types (refinements for cloud identifiers) ----------------
-type GcpProjectId = String where non_empty, pattern("^[a-z][a-z0-9-]{4,28}[a-z0-9]$")
-type ServiceAccountEmail = String where pattern("^[a-z][a-z0-9-]*@[a-z0-9-]+\\.iam\\.gserviceaccount\\.com$")
+// GcpProjectId: restore `where non_empty, pattern("^[a-z][a-z0-9-]{4,28}[a-z0-9]$")` post-Q-Regex.
+// Pattern half dropped; non_empty half kept as it migrates via the registry.
+type GcpProjectId = String where non_empty
+// ServiceAccountEmail: restore `where pattern("^[a-z][a-z0-9-]*@[a-z0-9-]+\\.iam\\.gserviceaccount\\.com$")` post-Q-Regex.
+type ServiceAccountEmail = String
 
 // Refinement chain example (transitive subtyping):
 //   [Url] < [NonEmptyStr] < [String] < [Json]
@@ -413,13 +428,18 @@ type SymlinkTarget
 //   [FilePath] !<= [TextFilePath]  ->  "cannot prove content is text"
 // The developer must insert an explicit classification step.
 
-type TextFilePath   = FilePath where content(Text)
-type BinaryFilePath = FilePath where content(Binary)
+// TextFilePath: restore `where content(Text)` post-Q-Regex / content-typing
+// substrate. Content-typing carved with regex predicate as parallel
+// substrate-fact-introduction.
+type TextFilePath   = FilePath
+// BinaryFilePath: restore `where content(Binary)` post-content-typing landing.
+type BinaryFilePath = FilePath
 
 // FileEntry / FileClassification: std/filesystem.dag — one record, alias
 // name for probe-shaped API; Encoding from std/encoding.dag.
 
-type MimeType = String where pattern("^[a-z]+/[a-z0-9.+-]+$")
+// MimeType: restore `where pattern("^[a-z]+/[a-z0-9.+-]+$")` post-Q-Regex.
+type MimeType = String
 
 // File type rules -- declarative extension-to-encoding mapping.
 // This is compile-time data the compiler uses for: