P3b PR1: lean width + signedness collapse (admission boundary)

dag/std/integer.dag

@@ -21,6 +21,12 @@ type UInt128 = Compose<UInt, MachineWidth<128>>
 type Int = AbelianGroup<GroupCompletion<Nat>>
 type UInt = Nat
 
+type Signedness
+  = Signed
+  | Unsigned
+
+data std_integer_std_nat_fork_note: String = "PR1 Signedness lift imports std.nat here, co-resolving std.nat with v2.std.nat in whole-tree compile-clean closures. Known two-std-trees fork: std.nat.Nat = CommutativeSemiring<Magnitude> with std.nat.nat_compare versus v2.std.nat.Nat = Zero|Succ with v2.std.nat.nat_compare — not consolidated in this PR. Dissolve-on: two-std-trees consolidation lands a single Nat authority and retires the parallel compare fns; until then ambiguous bare references must qualify by containment path (namespace-resolution-design section 13). Disposition: awaiting an operator dispatch decision — not deferred work; a corpus-wide std carrier consolidation cannot be self-assigned by the session that found it, so the trigger and acceptance condition above are fixed and what is missing is only the dispatch; naming a fabricated owner would assert an ownership fact that is not true. The bound on the deferral, which is what keeps it tracked rather than parked: until the trigger fires, a bare reference to a Nat operation in a closure containing both authorities is ambiguous by construction and must be qualified — no consumer may assume a bare Nat name resolves, and the two Nat types are not interchangeable at any call site even where the name matches."
+
 type IntPlatform  = Compose<Int,  MachineWidth<PointerWidth>>
 type UIntPlatform = Compose<UInt, MachineWidth<PointerWidth>>
 

src/v1/stage0/src/std_integer.rs

@@ -1,6 +1,7 @@
 // Generated by v1 compiler -- do not edit.
 // Source module: std.integer
 
+use self::Signedness::*;
 pub use crate::std_algebra::{AbelianGroup, GroupCompletion};
 pub use crate::std_induction::int_pow_bounded;
 pub use crate::std_machine_constraints::{Compose, MachineWidth, PointerWidth};
@@ -47,6 +48,24 @@ pub type Int = i64;
 
 pub type UInt = i64;
 
+#[derive(
+    Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize,
+)]
+#[serde(tag = "_variant")]
+pub enum Signedness {
+    Signed,
+    Unsigned,
+}
+
+pub fn std_integer_std_nat_fork_note() -> String {
+    thread_local! {
+        static CACHED: String = {
+            "PR1 Signedness lift imports std.nat here, co-resolving std.nat with v2.std.nat in whole-tree compile-clean closures. Known two-std-trees fork: std.nat.Nat = CommutativeSemiring<Magnitude> with std.nat.nat_compare versus v2.std.nat.Nat = Zero|Succ with v2.std.nat.nat_compare — not consolidated in this PR. Dissolve-on: two-std-trees consolidation lands a single Nat authority and retires the parallel compare fns; until then ambiguous bare references must qualify by containment path (namespace-resolution-design section 13). Disposition: awaiting an operator dispatch decision — not deferred work; a corpus-wide std carrier consolidation cannot be self-assigned by the session that found it, so the trigger and acceptance condition above are fixed and what is missing is only the dispatch; naming a fabricated owner would assert an ownership fact that is not true. The bound on the deferral, which is what keeps it tracked rather than parked: until the trigger fires, a bare reference to a Nat operation in a closure containing both authorities is ambiguous by construction and must be qualified — no consumer may assume a bare Nat name resolves, and the two Nat types are not interchangeable at any call site even where the name matches.".to_string()
+        };
+    }
+    CACHED.with(|c: &String| c.clone())
+}
+
 pub type IntPlatform = crate::std_machine_constraints::Compose<
     i64,
     crate::std_machine_constraints::MachineWidth<PointerWidth>,
@@ -71,3 +90,8 @@ pub fn uint8_channel_inclusive_max_value_derived() -> Option<Int> {
         None => None,
     }
 }
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
+pub struct Signed;
+#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
+pub struct Unsigned;