From 035475af1da9a1928aa70a6d9c467887408aa6c3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 05:23:13 +0000 Subject: [PATCH 1/7] WIP: W0.1 lens de-fork: unify effect/idempotency/ownership/parallelism classi --- src/v2/lens/common/algebraic_composition.dag | 101 +++++++++++++++++++ src/v2/lens/effect.dag | 9 +- src/v2/lens/idempotency.dag | 32 ++---- src/v2/lens/ownership.dag | 39 ++----- src/v2/lens/parallelism.dag | 66 +++++------- 5 files changed, 143 insertions(+), 104 deletions(-) create mode 100644 src/v2/lens/common/algebraic_composition.dag diff --git a/src/v2/lens/common/algebraic_composition.dag b/src/v2/lens/common/algebraic_composition.dag new file mode 100644 index 00000000000..d8ffc24e3bc --- /dev/null +++ b/src/v2/lens/common/algebraic_composition.dag @@ -0,0 +1,101 @@ +module v2.lens.common.algebraic_composition + +import v2.compiler.infer { InferredFacts } +import v2.std.dependency { DependencyKindClassifier } +import v2.std.diagnostic { Diagnostic } +import v2.std.witness { Witness } + +type EffectClassification {} + +type IdempotencyVerdict + = AlgebraicIdempotenceProven { law: Witness } + | RequiresAlgebraWitness + +type OwnershipMode + = OwnedContainment + | SharedRead + | RequiresAccessWitness + | BorrowedDependency + | UnknownOwnership + +type ParallelismRelation + = DataDependent + | EffectCoupled + | BarrierCoupled + | UnresolvedCoupling { diagnostic: Diagnostic } + +type ParallelismKindPolicy + = KnownParallelismRelation { relation: ParallelismRelation } + | ReadsParallelismFacts + +data effect_classifier: DependencyKindClassifier = DependencyKindClassifier { + contains: EffectClassification {}, + binds_to: EffectClassification {}, + type_depends_on: EffectClassification {}, + data_depends_on: EffectClassification {}, + effect_depends_on: EffectClassification {}, + resource_depends_on: EffectClassification {}, + module_depends_on: EffectClassification {}, + barrier_before: EffectClassification {}, + placement_depends_on: EffectClassification {}, + model_depends_on: EffectClassification {}, + projection_depends_on: EffectClassification {}, + generated_from: EffectClassification {}, + verified_by: EffectClassification {}, + promoted_by: EffectClassification {}, + bootstrap_depends_on: EffectClassification {} +} + +data idempotency_classifier: DependencyKindClassifier = DependencyKindClassifier { + contains: RequiresAlgebraWitness, + binds_to: RequiresAlgebraWitness, + type_depends_on: RequiresAlgebraWitness, + data_depends_on: RequiresAlgebraWitness, + effect_depends_on: RequiresAlgebraWitness, + resource_depends_on: RequiresAlgebraWitness, + module_depends_on: RequiresAlgebraWitness, + barrier_before: RequiresAlgebraWitness, + placement_depends_on: RequiresAlgebraWitness, + model_depends_on: RequiresAlgebraWitness, + projection_depends_on: RequiresAlgebraWitness, + generated_from: RequiresAlgebraWitness, + verified_by: RequiresAlgebraWitness, + promoted_by: RequiresAlgebraWitness, + bootstrap_depends_on: RequiresAlgebraWitness +} + +data ownership_classifier: DependencyKindClassifier = DependencyKindClassifier { + contains: OwnedContainment, + binds_to: BorrowedDependency, + type_depends_on: UnknownOwnership, + data_depends_on: SharedRead, + effect_depends_on: RequiresAccessWitness, + resource_depends_on: RequiresAccessWitness, + module_depends_on: UnknownOwnership, + barrier_before: UnknownOwnership, + placement_depends_on: UnknownOwnership, + model_depends_on: UnknownOwnership, + projection_depends_on: UnknownOwnership, + generated_from: UnknownOwnership, + verified_by: UnknownOwnership, + promoted_by: UnknownOwnership, + bootstrap_depends_on: UnknownOwnership +} + +data parallelism_classifier: DependencyKindClassifier = DependencyKindClassifier { + contains: KnownParallelismRelation { relation: DataDependent }, + binds_to: KnownParallelismRelation { relation: DataDependent }, + type_depends_on: ReadsParallelismFacts, + data_depends_on: KnownParallelismRelation { relation: DataDependent }, + effect_depends_on: KnownParallelismRelation { relation: EffectCoupled }, + resource_depends_on: KnownParallelismRelation { relation: EffectCoupled }, + module_depends_on: ReadsParallelismFacts, + barrier_before: KnownParallelismRelation { relation: BarrierCoupled }, + placement_depends_on: ReadsParallelismFacts, + model_depends_on: ReadsParallelismFacts, + projection_depends_on: ReadsParallelismFacts, + generated_from: ReadsParallelismFacts, + verified_by: ReadsParallelismFacts, + promoted_by: ReadsParallelismFacts, + bootstrap_depends_on: ReadsParallelismFacts +} diff --git a/src/v2/lens/effect.dag b/src/v2/lens/effect.dag index d5cfd505c27..567ab3dfd92 100644 --- a/src/v2/lens/effect.dag +++ b/src/v2/lens/effect.dag @@ -1,5 +1,6 @@ module v2.lens.effect import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding } +import v2.lens.common.algebraic_composition { EffectClassification, effect_classifier } import std.disposition { SingleAuthority } import v2.compiler.infer { InferredFacts, InferredTree } @@ -15,6 +16,7 @@ import v2.std.collection { import v2.std.dependency { ClassifiedDependencyView, DependencyView, + classify_dependency_view, classified_dependency_view_eq } import v2.std.diagnostic { @@ -28,8 +30,6 @@ import v2.std.logic { Bool } import v2.std.node { Node, Symbol } import v2.std.witness { Holds, Violates, Witness } -type EffectClassification {} - type EffectFact { dependencies: List> } @@ -38,10 +38,7 @@ fn effect_classify( tree: InferredTree, view: DependencyView ) -> ClassifiedDependencyView { - ClassifiedDependencyView { - dependency: view, - classification: EffectClassification {} - } + classify_dependency_view(classifier: effect_classifier, view: view) } fn effect_fact(tree: InferredTree, dependencies: List) -> EffectFact { diff --git a/src/v2/lens/idempotency.dag b/src/v2/lens/idempotency.dag index e066e3222c7..7727b4ac8a5 100644 --- a/src/v2/lens/idempotency.dag +++ b/src/v2/lens/idempotency.dag @@ -1,5 +1,10 @@ module v2.lens.idempotency import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding } +import v2.lens.common.algebraic_composition { + IdempotencyVerdict, + RequiresAlgebraWitness, + idempotency_classifier +} import std.disposition { SingleAuthority } import v2.compiler.infer { InferredFacts, InferredTree } @@ -14,7 +19,6 @@ import v2.std.collection { } import v2.std.dependency { ClassifiedDependencyView, - DependencyKindClassifier, DependencyView, classify_dependency_view, classified_dependency_view_eq @@ -30,36 +34,12 @@ import v2.std.logic { Bool } import v2.std.node { Symbol } import v2.std.witness { Holds, Violates, Witness } -type IdempotencyVerdict - = AlgebraicIdempotenceProven { law: Witness } - | RequiresAlgebraWitness - type IdempotencyFact { dependencies: List> } -fn idempotency_dependency_kind_classifier() -> DependencyKindClassifier { - DependencyKindClassifier { - contains: RequiresAlgebraWitness, - binds_to: RequiresAlgebraWitness, - type_depends_on: RequiresAlgebraWitness, - data_depends_on: RequiresAlgebraWitness, - effect_depends_on: RequiresAlgebraWitness, - resource_depends_on: RequiresAlgebraWitness, - module_depends_on: RequiresAlgebraWitness, - barrier_before: RequiresAlgebraWitness, - placement_depends_on: RequiresAlgebraWitness, - model_depends_on: RequiresAlgebraWitness, - projection_depends_on: RequiresAlgebraWitness, - generated_from: RequiresAlgebraWitness, - verified_by: RequiresAlgebraWitness, - promoted_by: RequiresAlgebraWitness, - bootstrap_depends_on: RequiresAlgebraWitness - } -} - fn idempotency_classify(view: DependencyView) -> ClassifiedDependencyView { - classify_dependency_view(classifier: idempotency_dependency_kind_classifier(), view: view) + classify_dependency_view(classifier: idempotency_classifier, view: view) } fn idempotency_fact(tree: InferredTree, dependencies: List) -> IdempotencyFact { diff --git a/src/v2/lens/ownership.dag b/src/v2/lens/ownership.dag index 1f7aa2a8548..ac567f51c12 100644 --- a/src/v2/lens/ownership.dag +++ b/src/v2/lens/ownership.dag @@ -1,5 +1,14 @@ module v2.lens.ownership import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding } +import v2.lens.common.algebraic_composition { + BorrowedDependency, + OwnedContainment, + OwnershipMode, + RequiresAccessWitness, + SharedRead, + UnknownOwnership, + ownership_classifier +} import std.disposition { SingleAuthority } import v2.compiler.infer { InferredTree } @@ -7,7 +16,6 @@ import v2.std.algebra { bag_eq, list_snoc_item } import v2.std.collection { List } import v2.std.dependency { ClassifiedDependencyView, - DependencyKindClassifier, DependencyView, classify_dependency_view, classified_dependency_view_eq @@ -23,39 +31,12 @@ import v2.std.logic { Bool } import v2.std.node { Symbol } import v2.std.witness { Holds, Violates, Witness } -type OwnershipMode - = OwnedContainment - | SharedRead - | RequiresAccessWitness - | BorrowedDependency - | UnknownOwnership - type OwnershipFact { dependencies: List> } -fn ownership_dependency_kind_classifier() -> DependencyKindClassifier { - DependencyKindClassifier { - contains: OwnedContainment, - binds_to: BorrowedDependency, - type_depends_on: UnknownOwnership, - data_depends_on: SharedRead, - effect_depends_on: RequiresAccessWitness, - resource_depends_on: RequiresAccessWitness, - module_depends_on: UnknownOwnership, - barrier_before: UnknownOwnership, - placement_depends_on: UnknownOwnership, - model_depends_on: UnknownOwnership, - projection_depends_on: UnknownOwnership, - generated_from: UnknownOwnership, - verified_by: UnknownOwnership, - promoted_by: UnknownOwnership, - bootstrap_depends_on: UnknownOwnership - } -} - fn ownership_classify(view: DependencyView) -> ClassifiedDependencyView { - classify_dependency_view(classifier: ownership_dependency_kind_classifier(), view: view) + classify_dependency_view(classifier: ownership_classifier, view: view) } fn ownership_fact(tree: InferredTree, dependencies: List) -> OwnershipFact { diff --git a/src/v2/lens/parallelism.dag b/src/v2/lens/parallelism.dag index 438465a65e0..4677dc40b61 100644 --- a/src/v2/lens/parallelism.dag +++ b/src/v2/lens/parallelism.dag @@ -1,5 +1,16 @@ module v2.lens.parallelism import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding } +import v2.lens.common.algebraic_composition { + BarrierCoupled, + DataDependent, + EffectCoupled, + KnownParallelismRelation, + ParallelismKindPolicy, + ParallelismRelation, + ReadsParallelismFacts, + UnresolvedCoupling, + parallelism_classifier +} import std.disposition { SingleAuthority } import v2.compiler.infer { InferredFacts, InferredTree, inferred_facts_descent } @@ -14,7 +25,6 @@ import v2.std.collection { } import v2.std.dependency { ClassifiedDependencyView, - DependencyKindClassifier, DependencyView, classify_dependency_kind, classified_dependency_view_eq @@ -31,38 +41,22 @@ import v2.std.logic { Bool } import v2.std.node { Symbol } import v2.std.witness { Holds, Violates, Witness } -type ParallelismRelation - = DataDependent - | EffectCoupled - | BarrierCoupled - | UnresolvedCoupling { diagnostic: Diagnostic } - -type ParallelismKindPolicy - = KnownParallelismRelation { relation: ParallelismRelation } - | ReadsParallelismFacts - type ParallelismFact { dependencies: List> } -fn parallelism_dependency_kind_classifier() -> DependencyKindClassifier { - DependencyKindClassifier { - contains: KnownParallelismRelation { relation: DataDependent }, - binds_to: KnownParallelismRelation { relation: DataDependent }, - type_depends_on: ReadsParallelismFacts, - data_depends_on: KnownParallelismRelation { relation: DataDependent }, - effect_depends_on: KnownParallelismRelation { relation: EffectCoupled }, - resource_depends_on: KnownParallelismRelation { relation: EffectCoupled }, - module_depends_on: ReadsParallelismFacts, - barrier_before: KnownParallelismRelation { relation: BarrierCoupled }, - placement_depends_on: ReadsParallelismFacts, - model_depends_on: ReadsParallelismFacts, - projection_depends_on: ReadsParallelismFacts, - generated_from: ReadsParallelismFacts, - verified_by: ReadsParallelismFacts, - promoted_by: ReadsParallelismFacts, - bootstrap_depends_on: ReadsParallelismFacts - } +fn parallelism_relation_for_view( + tree: InferredTree, + view: DependencyView +) -> ParallelismRelation { + parallelism_relation_for_policy( + tree: tree, + view: view, + policy: classify_dependency_kind( + classifier: parallelism_classifier, + kind: view.kind + ) + ) } fn parallelism_witness_diagnostic() -> Diagnostic { @@ -121,20 +115,6 @@ fn parallelism_relation_for_policy( } } -fn parallelism_relation_for_view( - tree: InferredTree, - view: DependencyView -) -> ParallelismRelation { - parallelism_relation_for_policy( - tree: tree, - view: view, - policy: classify_dependency_kind( - classifier: parallelism_dependency_kind_classifier(), - kind: view.kind - ) - ) -} - fn parallelism_classify( tree: InferredTree, view: DependencyView From a5d4960d33e7ec96d945ddaa99c85967595c2db6 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 05:49:01 +0000 Subject: [PATCH 2/7] WIP: W0.1 lens de-fork: unify effect/idempotency/ownership/parallelism classi --- docs/plans/inert-layer-lens.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/docs/plans/inert-layer-lens.md b/docs/plans/inert-layer-lens.md index abe43320760..2b36cf23d49 100644 --- a/docs/plans/inert-layer-lens.md +++ b/docs/plans/inert-layer-lens.md @@ -95,8 +95,6 @@ The reading: the **schedule/width** arm of the realization layer is now wired; t ## 8. Generalization — one rule, N substrates (code · docs · lenses) -> **Sibling family (§2 redundancy, the other half).** Inertness is *"nothing reaches this concept"* (0 authorities/consumers). Its dual is *"this concept is reached but duplicates an authority that already exists"* (≥2 authorities) — the **redundancy / degenerate-work** family, whose test-substrate instance is the [vacuity lens](vacuity-lens-design.md) (a test whose expected value duplicates a code authority = `AuthoredDuplication` on the authored-fact substrate of the `materialization_ladder`). Same §2/§3 root, opposite end of the plurality axis (0 vs ≥2). - Reachability-completeness is **not specific to code** — it is a §2-horizontal "one concept, every breadth": *every declared node in a graph must be reachable from a root, on an exception roster, or deleted.* It already runs over the **lens** graph (#5433). It applies unchanged to the **doc** graph — and the doc instance is the **cheapest wall of all** (pure link reachability — no reflective edges *needed for the dangling half*, and far simpler than the code substrate): | substrate | nodes | edges | roots | inert = | dangling = | From c7c3ddc016dfa2ab1ec4386f692aead94b4d177b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 06:04:51 +0000 Subject: [PATCH 3/7] Import AlgebraicIdempotenceProven in idempotency lens after de-fork. The variant moved to algebraic_composition.dag with the classifier rows; idempotency.dag still pattern-matches it in witness/equality helpers. Co-authored-by: Cursor --- src/v2/lens/idempotency.dag | 1 + 1 file changed, 1 insertion(+) diff --git a/src/v2/lens/idempotency.dag b/src/v2/lens/idempotency.dag index 7727b4ac8a5..93250b1d49f 100644 --- a/src/v2/lens/idempotency.dag +++ b/src/v2/lens/idempotency.dag @@ -1,6 +1,7 @@ module v2.lens.idempotency import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding } import v2.lens.common.algebraic_composition { + AlgebraicIdempotenceProven, IdempotencyVerdict, RequiresAlgebraWitness, idempotency_classifier From f39f5bd0cf56025ba38d18d96a1b647525dc0b4b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 06:29:23 +0000 Subject: [PATCH 4/7] Drop stale-base revert of inert-layer-lens.md (not part of W0.1). Restore the vacuity sibling-family blockquote from main; the prior regenerated-artifact drift fix was an unrelated lane change that would orphan vacuity-lens-design.md from the doc graph. Co-authored-by: Cursor --- docs/plans/inert-layer-lens.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/docs/plans/inert-layer-lens.md b/docs/plans/inert-layer-lens.md index 2b36cf23d49..abe43320760 100644 --- a/docs/plans/inert-layer-lens.md +++ b/docs/plans/inert-layer-lens.md @@ -95,6 +95,8 @@ The reading: the **schedule/width** arm of the realization layer is now wired; t ## 8. Generalization — one rule, N substrates (code · docs · lenses) +> **Sibling family (§2 redundancy, the other half).** Inertness is *"nothing reaches this concept"* (0 authorities/consumers). Its dual is *"this concept is reached but duplicates an authority that already exists"* (≥2 authorities) — the **redundancy / degenerate-work** family, whose test-substrate instance is the [vacuity lens](vacuity-lens-design.md) (a test whose expected value duplicates a code authority = `AuthoredDuplication` on the authored-fact substrate of the `materialization_ladder`). Same §2/§3 root, opposite end of the plurality axis (0 vs ≥2). + Reachability-completeness is **not specific to code** — it is a §2-horizontal "one concept, every breadth": *every declared node in a graph must be reachable from a root, on an exception roster, or deleted.* It already runs over the **lens** graph (#5433). It applies unchanged to the **doc** graph — and the doc instance is the **cheapest wall of all** (pure link reachability — no reflective edges *needed for the dangling half*, and far simpler than the code substrate): | substrate | nodes | edges | roots | inert = | dangling = | From 9296c0628b2fd76158a5822c2c9d071c03b88ff0 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 06:47:30 +0000 Subject: [PATCH 5/7] WIP: W0.1 lens de-fork: unify effect/idempotency/ownership/parallelism classi --- dag/gunbc/plans/inert_layer_lens.dag | 3 +++ 1 file changed, 3 insertions(+) diff --git a/dag/gunbc/plans/inert_layer_lens.dag b/dag/gunbc/plans/inert_layer_lens.dag index 422e7c9bccb..1d0470e7690 100644 --- a/dag/gunbc/plans/inert_layer_lens.dag +++ b/dag/gunbc/plans/inert_layer_lens.dag @@ -97,6 +97,9 @@ fn inert_layer_lens_body() -> List { li(text: "**Dissolution:** the lens itself never dissolves (inertness is a standing property); its *exception roster* dissolves to empty as the realization loop wires each carrier, at which point the lens flips from advisory ② to fail-closed ① wall."), ]), h2(text: "8. Generalization — one rule, N substrates (code · docs · lenses)"), + quote(blocks: [ + p(text: "**Sibling family (§2 redundancy, the other half).** Inertness is *\"nothing reaches this concept\"* (0 authorities/consumers). Its dual is *\"this concept is reached but duplicates an authority that already exists\"* (≥2 authorities) — the **redundancy / degenerate-work** family, whose test-substrate instance is the [vacuity lens](vacuity-lens-design.md) (a test whose expected value duplicates a code authority = `AuthoredDuplication` on the authored-fact substrate of the `materialization_ladder`). Same §2/§3 root, opposite end of the plurality axis (0 vs ≥2)."), + ]), p(text: "Reachability-completeness is **not specific to code** — it is a §2-horizontal \"one concept, every breadth\": *every declared node in a graph must be reachable from a root, on an exception roster, or deleted.* It already runs over the **lens** graph (#5433). It applies unchanged to the **doc** graph — and the doc instance is the **cheapest wall of all** (pure link reachability — no reflective edges *needed for the dangling half*, and far simpler than the code substrate):"), TableBlock { header: row(cells: [cell(text: "substrate"), cell(text: "nodes"), cell(text: "edges"), cell(text: "roots"), cell(text: "inert ="), cell(text: "dangling =")]), From 34705a1cbf468cf240593aba005fd25680d133b0 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 14:47:25 +0000 Subject: [PATCH 6/7] WIP: W0.1 lens de-fork: unify effect/idempotency/ownership/parallelism classi --- docs/plans/inert-layer-lens.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/docs/plans/inert-layer-lens.md b/docs/plans/inert-layer-lens.md index 2b36cf23d49..abe43320760 100644 --- a/docs/plans/inert-layer-lens.md +++ b/docs/plans/inert-layer-lens.md @@ -95,6 +95,8 @@ The reading: the **schedule/width** arm of the realization layer is now wired; t ## 8. Generalization — one rule, N substrates (code · docs · lenses) +> **Sibling family (§2 redundancy, the other half).** Inertness is *"nothing reaches this concept"* (0 authorities/consumers). Its dual is *"this concept is reached but duplicates an authority that already exists"* (≥2 authorities) — the **redundancy / degenerate-work** family, whose test-substrate instance is the [vacuity lens](vacuity-lens-design.md) (a test whose expected value duplicates a code authority = `AuthoredDuplication` on the authored-fact substrate of the `materialization_ladder`). Same §2/§3 root, opposite end of the plurality axis (0 vs ≥2). + Reachability-completeness is **not specific to code** — it is a §2-horizontal "one concept, every breadth": *every declared node in a graph must be reachable from a root, on an exception roster, or deleted.* It already runs over the **lens** graph (#5433). It applies unchanged to the **doc** graph — and the doc instance is the **cheapest wall of all** (pure link reachability — no reflective edges *needed for the dangling half*, and far simpler than the code substrate): | substrate | nodes | edges | roots | inert = | dangling = | From 1551d22edb5039d2b585e45c859e017f06c19d22 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 15 Jul 2026 14:48:55 +0000 Subject: [PATCH 7/7] Drop inert_layer_lens changes from W0.1 PR scope. Note restoration is owned by #6671; revert dag and md to origin/main so this PR stays the pure 5-file classifier de-fork and drift-green. Co-authored-by: Cursor --- dag/gunbc/plans/inert_layer_lens.dag | 3 --- docs/plans/inert-layer-lens.md | 2 -- 2 files changed, 5 deletions(-) diff --git a/dag/gunbc/plans/inert_layer_lens.dag b/dag/gunbc/plans/inert_layer_lens.dag index 1d0470e7690..422e7c9bccb 100644 --- a/dag/gunbc/plans/inert_layer_lens.dag +++ b/dag/gunbc/plans/inert_layer_lens.dag @@ -97,9 +97,6 @@ fn inert_layer_lens_body() -> List { li(text: "**Dissolution:** the lens itself never dissolves (inertness is a standing property); its *exception roster* dissolves to empty as the realization loop wires each carrier, at which point the lens flips from advisory ② to fail-closed ① wall."), ]), h2(text: "8. Generalization — one rule, N substrates (code · docs · lenses)"), - quote(blocks: [ - p(text: "**Sibling family (§2 redundancy, the other half).** Inertness is *\"nothing reaches this concept\"* (0 authorities/consumers). Its dual is *\"this concept is reached but duplicates an authority that already exists\"* (≥2 authorities) — the **redundancy / degenerate-work** family, whose test-substrate instance is the [vacuity lens](vacuity-lens-design.md) (a test whose expected value duplicates a code authority = `AuthoredDuplication` on the authored-fact substrate of the `materialization_ladder`). Same §2/§3 root, opposite end of the plurality axis (0 vs ≥2)."), - ]), p(text: "Reachability-completeness is **not specific to code** — it is a §2-horizontal \"one concept, every breadth\": *every declared node in a graph must be reachable from a root, on an exception roster, or deleted.* It already runs over the **lens** graph (#5433). It applies unchanged to the **doc** graph — and the doc instance is the **cheapest wall of all** (pure link reachability — no reflective edges *needed for the dangling half*, and far simpler than the code substrate):"), TableBlock { header: row(cells: [cell(text: "substrate"), cell(text: "nodes"), cell(text: "edges"), cell(text: "roots"), cell(text: "inert ="), cell(text: "dangling =")]), diff --git a/docs/plans/inert-layer-lens.md b/docs/plans/inert-layer-lens.md index abe43320760..2b36cf23d49 100644 --- a/docs/plans/inert-layer-lens.md +++ b/docs/plans/inert-layer-lens.md @@ -95,8 +95,6 @@ The reading: the **schedule/width** arm of the realization layer is now wired; t ## 8. Generalization — one rule, N substrates (code · docs · lenses) -> **Sibling family (§2 redundancy, the other half).** Inertness is *"nothing reaches this concept"* (0 authorities/consumers). Its dual is *"this concept is reached but duplicates an authority that already exists"* (≥2 authorities) — the **redundancy / degenerate-work** family, whose test-substrate instance is the [vacuity lens](vacuity-lens-design.md) (a test whose expected value duplicates a code authority = `AuthoredDuplication` on the authored-fact substrate of the `materialization_ladder`). Same §2/§3 root, opposite end of the plurality axis (0 vs ≥2). - Reachability-completeness is **not specific to code** — it is a §2-horizontal "one concept, every breadth": *every declared node in a graph must be reachable from a root, on an exception roster, or deleted.* It already runs over the **lens** graph (#5433). It applies unchanged to the **doc** graph — and the doc instance is the **cheapest wall of all** (pure link reachability — no reflective edges *needed for the dangling half*, and far simpler than the code substrate): | substrate | nodes | edges | roots | inert = | dangling = |