Converge construction_justification onto std.disposition (Phase 1: typed dissolves_to + prose fold; interim, bind deferred)

src/v2/lens/affected_set.dag

@@ -1,5 +1,6 @@
 module v2.lens.affected_set
 import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
+import std.disposition { SingleAuthority }
 
 import v2.std.collection { Absent, List, Map, Present, list_at_optional, map_get, map_insert }
 import v2.std.algebra { TailAbsent, TailFound, contains, length, list_append, list_snoc_item, list_tail }
@@ -1342,9 +1343,6 @@ fn repo_process_universe() -> RepoProcessUniverse {
 }
 
 data construction_justification: ConstructionJustification = ConstructionJustification {
-  class: WallAfterGrounding {
-    grounding_authority: "the v2 scheduler consuming the re-execution frontier natively (B-4/B-5 node-precision closure)",
-    dissolve_on: "the scheduler derives incremental re-execution from the changed-subgraph fold by construction"
-  },
-  rationale: "Changed-subgraph reachability is a decidable fold (re_exec_frontier_from_diff); it is a lens today only because the scheduler does not yet consume the frontier as a construction."
+  class: WallAfterGrounding { dissolves_to: SingleAuthority },
+  rationale: "Changed-subgraph reachability is a decidable fold (re_exec_frontier_from_diff); it is a lens today only because the scheduler does not yet consume the frontier as a construction. Grounding authority: the v2 scheduler consuming the re-execution frontier natively (B-4/B-5 node-precision closure). Dissolves on: the scheduler derives incremental re-execution from the changed-subgraph fold by construction"
 }

src/v2/lens/affected_set_examples.dag

@@ -1,5 +1,6 @@
 module v2.lens.affected_set_examples
 import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
+import std.disposition { SingleAuthority }
 
 import v2.std.diagnostic {
   Accepted,
@@ -176,9 +177,6 @@ data affected_set_example_two_edit_diff: Diff = Diff {
 }
 
 data construction_justification: ConstructionJustification = ConstructionJustification {
-  class: WallAfterGrounding {
-    grounding_authority: "v2.lens.affected_set owning its example values as a sub-module / test fixture",
-    dissolve_on: "the affected-set frontier examples fold into v2.lens.affected_set as a sub-module, not a top-level lens"
-  },
-  rationale: "Example frontier values for the affected-set lens: carries no independent bad-state class; its single-authority home (DESIGN sec 3) is a sub-module of affected_set, not a separate top-level lens."
+  class: WallAfterGrounding { dissolves_to: SingleAuthority },
+  rationale: "Example frontier values for the affected-set lens: carries no independent bad-state class; its single-authority home (DESIGN sec 3) is a sub-module of affected_set, not a separate top-level lens. Grounding authority: v2.lens.affected_set owning its example values as a sub-module / test fixture. Dissolves on: the affected-set frontier examples fold into v2.lens.affected_set as a sub-module, not a top-level lens"
 }

src/v2/lens/application.dag

@@ -1,5 +1,6 @@
 module v2.lens.application
 import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
+import std.disposition { RealizationDispatch }
 
 import v2.std.algebra { Cons, Empty, is_empty, fold_list, list_snoc_item }
 import v2.std.collection { List }
@@ -499,9 +500,6 @@ fn apply_advisory_lens(
 }
 
 data construction_justification: ConstructionJustification = ConstructionJustification {
-  class: WallAfterGrounding {
-    grounding_authority: "the substrate lens-attachment surface (apply_lens / CompileLens pipeline-gate adapter) plus section-ref-identity-evidence",
-    dissolve_on: "lens application is a substrate mechanism (the advisory-to-fail-closed bridge by construction) and section_subject resolves via section-ref identity"
-  },
-  rationale: "The lens-application surface is a mechanism, not a bad-state detector; it is staged pending section-ref-identity-evidence and the compile-pipeline gate adapter wiring."
+  class: WallAfterGrounding { dissolves_to: RealizationDispatch },
+  rationale: "The lens-application surface is a mechanism, not a bad-state detector; it is staged pending section-ref-identity-evidence and the compile-pipeline gate adapter wiring. Grounding authority: the substrate lens-attachment surface (apply_lens / CompileLens pipeline-gate adapter) plus section-ref-identity-evidence. Dissolves on: lens application is a substrate mechanism (the advisory-to-fail-closed bridge by construction) and section_subject resolves via section-ref identity"
 }

src/v2/lens/common/construction_justification.dag

@@ -2,11 +2,13 @@ module v2.lens.common.construction_justification
 
 import v2.std.text { String }
 
+import std.disposition { ConstructionMechanism }
+
 type ConstructionClass
 
   = WallNow { construction: String }
 
-  | WallAfterGrounding { grounding_authority: String, dissolve_on: String }
+  | WallAfterGrounding { dissolves_to: ConstructionMechanism }
 
   | RatchetForever { undecidable_because: String }
 

src/v2/lens/complexity_lowering.dag

@@ -1,5 +1,6 @@
 module v2.lens.complexity_lowering
 import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
+import std.disposition { SingleAuthority }
 
 import v2.lens.cost {
   AsymptoticClass,
@@ -72,9 +73,6 @@ fn minimized_class(c: SymbolicCost) -> AsymptoticClass {
 }
 
 data construction_justification: ConstructionJustification = ConstructionJustification {
-  class: WallAfterGrounding {
-    grounding_authority: "the dependency-coupling carrier on InferredFacts that v2.lens.parallelism waits on (feature:T-13-parallelism-relation-unresolved) -- it decides loop-invariance / independence",
-    dissolve_on: "a catalogued lowering fires on a LIVE realized cost once independence is read from the coupling carrier by construction; until then matching the realized asymptotic class against a lowering's before-class (O(n^2) = ClassPolynomial degree 2) is the decidable NECESSARY condition and the row over-approximates -- sufficiency (genuine loop-invariant hoist O(n^2)->O(n), not a real all-pairs O(n^2)) waits on the carrier"
-  },
-  rationale: "The DECIDABLE lowering catalog -- the wall-half carved out of v2.lens.complexity's RatchetForever optimality residue. complexity.dag projects a realized cost onto an AsymptoticClass and surfaces an undecidable GAP (Rice); this module formalizes the opposite-direction decidable fragment: a finite whitelist of cost-recurrence lowerings each PROVABLY strictly lowering the class (the §5 'O(n^2)->O(n)' lowerings). §5 partition: (1) every catalogued lowering strictly lowers the class -- decidable now, enforced by catalog_is_sound (the lowering-catalog wall); (2) whether a realized cost matches a lowering is decided by class-equality against cost.dag's exhaustive asymptotic_class_of_cost (no hand-rolled wildcard match -- single authority, total), but its SUFFICIENCY is grounded by the independence carrier above; (3) global optimality stays the RatchetForever in v2.lens.complexity / v2.lens.synthesis. One catalog, N rows -- the RunTime axis of v2.lens.intent_linearity (the ChangeTime axis is anti-unification)."
+  class: WallAfterGrounding { dissolves_to: SingleAuthority },
+  rationale: "The DECIDABLE lowering catalog -- the wall-half carved out of v2.lens.complexity's RatchetForever optimality residue. complexity.dag projects a realized cost onto an AsymptoticClass and surfaces an undecidable GAP (Rice); this module formalizes the opposite-direction decidable fragment: a finite whitelist of cost-recurrence lowerings each PROVABLY strictly lowering the class (the §5 'O(n^2)->O(n)' lowerings). §5 partition: (1) every catalogued lowering strictly lowers the class -- decidable now, enforced by catalog_is_sound (the lowering-catalog wall); (2) whether a realized cost matches a lowering is decided by class-equality against cost.dag's exhaustive asymptotic_class_of_cost (no hand-rolled wildcard match -- single authority, total), but its SUFFICIENCY is grounded by the independence carrier above; (3) global optimality stays the RatchetForever in v2.lens.complexity / v2.lens.synthesis. One catalog, N rows -- the RunTime axis of v2.lens.intent_linearity (the ChangeTime axis is anti-unification). Grounding authority: the dependency-coupling carrier on InferredFacts that v2.lens.parallelism waits on (feature:T-13-parallelism-relation-unresolved) -- it decides loop-invariance / independence. Dissolves on: a catalogued lowering fires on a LIVE realized cost once independence is read from the coupling carrier by construction; until then matching the realized asymptotic class against a lowering's before-class (O(n^2) = ClassPolynomial degree 2) is the decidable NECESSARY condition and the row over-approximates -- sufficiency (genuine loop-invariant hoist O(n^2)->O(n), not a real all-pairs O(n^2)) waits on the carrier"
 }

src/v2/lens/coverage.dag

@@ -1,5 +1,6 @@
 module v2.lens.coverage
 import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
+import std.disposition { SubstrateMandatoryTag }
 
 import v2.std.algebra {
   Cons,
@@ -115,9 +116,6 @@ fn missing_coverage<C>(
 }
 
 data construction_justification: ConstructionJustification = ConstructionJustification {
-  class: WallAfterGrounding {
-    grounding_authority: "corpus-as-type: the substrate seeing an unhandled declared-data corpus member as a compile error (the mock_totality consumer)",
-    dissolve_on: "the published corpus is a closed type the compiler totality-checks, not declared data"
-  },
-  rationale: "Expected-vs-actual missing-set is a decidable set-difference over declared corpora (consumed by mock_totality); it is a lens because the corpus is data, not a type the compiler can see is unhandled."
+  class: WallAfterGrounding { dissolves_to: SubstrateMandatoryTag },
+  rationale: "Expected-vs-actual missing-set is a decidable set-difference over declared corpora (consumed by mock_totality); it is a lens because the corpus is data, not a type the compiler can see is unhandled. Grounding authority: corpus-as-type: the substrate seeing an unhandled declared-data corpus member as a compile error (the mock_totality consumer). Dissolves on: the published corpus is a closed type the compiler totality-checks, not declared data"
 }

src/v2/lens/discrimination.dag

@@ -1,5 +1,6 @@
 module v2.lens.discrimination
 import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
+import std.disposition { SubstrateMandatoryTag }
 
 import v2.std.witness { Holds, Violates, Witness }
 import v2.std.verification {
@@ -120,9 +121,6 @@ fn unit_is_discriminating(unit: List<TestClaim>) -> Bool {
 }
 
 data construction_justification: ConstructionJustification = ConstructionJustification {
-  class: WallAfterGrounding {
-    grounding_authority: "the witness-authoring surface requiring a discriminating red-arm (the DESIGN sec 5 discrimination gate, PR #5116)",
-    dissolve_on: "a green-only TestClaim unit becomes unwritable: the authoring surface mandates a perturbed-red assertion by construction"
-  },
-  rationale: "Whether a witness unit asserts both green and a perturbed-red is decidable over TestClaim polarity; it is a lens until the witness-authoring surface makes a green-only unit unwritable."
+  class: WallAfterGrounding { dissolves_to: SubstrateMandatoryTag },
+  rationale: "Whether a witness unit asserts both green and a perturbed-red is decidable over TestClaim polarity; it is a lens until the witness-authoring surface makes a green-only unit unwritable. Grounding authority: the witness-authoring surface requiring a discriminating red-arm (the DESIGN sec 5 discrimination gate, PR #5116). Dissolves on: a green-only TestClaim unit becomes unwritable: the authoring surface mandates a perturbed-red assertion by construction"
 }

src/v2/lens/disposition_redundancy.dag

@@ -2,7 +2,7 @@ module v2.lens.disposition_redundancy
 
 import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
 
-import std.disposition { Disposition, Scaffold, Terminal, DeclLocator, ScaffoldTarget, WholeDeclaration, NamedField }
+import std.disposition { Disposition, Scaffold, Terminal, DeclLocator, ScaffoldTarget, WholeDeclaration, NamedField, SubstrateMandatoryTag }
 import v2.std.collection { List }
 import v2.std.algebra { count_where, any }
 import v2.std.logic { Bool }
@@ -41,9 +41,6 @@ fn disposition_redundancy_violation_count(dispositions: List<Disposition>, prese
 }
 
 data construction_justification: ConstructionJustification = ConstructionJustification {
-  class: WallAfterGrounding {
-    grounding_authority: "the parse/resolve walk enumerating every declared decl + field across the corpus as DeclLocator facts (so present-construction membership is read from the live tree, not passed in), plus the SubstrateMandatoryTag end-state where the substrate requires a Disposition at every coproduct/scaffold definition",
-    dissolve_on: "disposition_redundancy_violation_count runs over live dsl/** + src/v2/** Disposition marks against corpus-enumerated DeclLocator facts; until then it is a lens_unit predicate over explicit (dispositions, present) inputs. The ratcheting redundancy lens itself dissolves once Disposition is a substrate-mandatory field and the bad state is unwritable by construction"
-  },
-  rationale: "A Scaffold whose named successor (bind) already exists in the corpus is decidable redundancy (DESIGN sec 2 parallel-representation debt): scaffold + its successor both alive. It is a wall, not a ratchet -- the membership test is exact equality of a field-granular declaration locator. It is a lens rather than a construction only because enumerating the present successors as substrate facts (and ultimately mandating the tag) are not yet available; both are named in grounding_authority."
+  class: WallAfterGrounding { dissolves_to: SubstrateMandatoryTag },
+  rationale: "A Scaffold whose named successor (bind) already exists in the corpus is decidable redundancy (DESIGN sec 2 parallel-representation debt): scaffold + its successor both alive. It is a wall, not a ratchet -- the membership test is exact equality of a field-granular declaration locator. It is a lens rather than a construction only because enumerating the present successors as substrate facts (and ultimately mandating the tag) are not yet available; both are named in grounding_authority. Grounding authority: the parse/resolve walk enumerating every declared decl + field across the corpus as DeclLocator facts (so present-construction membership is read from the live tree, not passed in), plus the SubstrateMandatoryTag end-state where the substrate requires a Disposition at every coproduct/scaffold definition. Dissolves on: disposition_redundancy_violation_count runs over live dsl/** + src/v2/** Disposition marks against corpus-enumerated DeclLocator facts; until then it is a lens_unit predicate over explicit (dispositions, present) inputs. The ratcheting redundancy lens itself dissolves once Disposition is a substrate-mandatory field and the bad state is unwritable by construction"
 }

src/v2/lens/edit_locus.dag

@@ -1,5 +1,6 @@
 module v2.lens.edit_locus
 import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
+import std.disposition { SingleAuthority }
 
 import v2.compiler.infer { InferredTree }
 import v2.lens.affected_set { AffectedSetReading, affected_set_reading }
@@ -255,9 +256,6 @@ fn affected_set_reading_from_git_diff_provenance(
 }
 
 data construction_justification: ConstructionJustification = ConstructionJustification {
-  class: WallAfterGrounding {
-    grounding_authority: "NodeArtifactProvenance -- the modeled path-to-Node authority",
-    dissolve_on: "the EditLocusRead/PathRegex shim is replaced once Q-Regex-Primitive lands and provenance owns the path-to-Node mapping"
-  },
-  rationale: "Diff path to substrate Node edit_locus is decidable; the lens is a compatibility shim over NodeArtifactProvenance until the regex primitive lands."
+  class: WallAfterGrounding { dissolves_to: SingleAuthority },
+  rationale: "Diff path to substrate Node edit_locus is decidable; the lens is a compatibility shim over NodeArtifactProvenance until the regex primitive lands. Grounding authority: NodeArtifactProvenance -- the modeled path-to-Node authority. Dissolves on: the EditLocusRead/PathRegex shim is replaced once Q-Regex-Primitive lands and provenance owns the path-to-Node mapping"
 }

src/v2/lens/effect.dag

@@ -1,5 +1,6 @@
 module v2.lens.effect
 import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
+import std.disposition { SingleAuthority }
 
 import v2.compiler.infer { InferredFacts, InferredTree }
 import v2.std.algebra { bag_eq, list_snoc_item, non_empty }
@@ -113,9 +114,6 @@ fn effect_fact_eq(a: EffectFact, b: EffectFact) -> Bool {
 }
 
 data construction_justification: ConstructionJustification = ConstructionJustification {
-  class: WallAfterGrounding {
-    grounding_authority: "the signature-derived closed effect-kind set (#3468 BLOCKING follow-up)",
-    dissolve_on: "effect kinds are derived from the type signature by construction (single authority, B3), closing the per-edge classification ratchet"
-  },
-  rationale: "Effects are a decidable projection of type-signature shape; the lens is a per-edge ratchet until the signature-derived effect-kind set is closed (re-authoring from DependencyKind would be a second authority)."
+  class: WallAfterGrounding { dissolves_to: SingleAuthority },
+  rationale: "Effects are a decidable projection of type-signature shape; the lens is a per-edge ratchet until the signature-derived effect-kind set is closed (re-authoring from DependencyKind would be a second authority). Grounding authority: the signature-derived closed effect-kind set (#3468 BLOCKING follow-up). Dissolves on: effect kinds are derived from the type signature by construction (single authority, B3), closing the per-edge classification ratchet"
 }