Add Atlas semantic documentation graph support

Author: yuechen-li-dev

Experiments/PolicyLab/M0/Atlas.oct

@@ -0,0 +1,101 @@
+package PolicyLab
+
+import Atlas
+
+fn AtlasDocument() -> Atlas.TableDocument {
+    let policy = Atlas.AdvisoryPolicy() with {
+        RequireRequirementImplementation: true
+        RequireRequirementVerifier: true
+        RequireInterpretationCitation: true
+        RequireClaimSupport: true
+    }
+    return Atlas.TableDocument {
+        Authorities: Atlas.AuthorityTable {
+            ID:["Authority.US.FLSA", "Authority.US.FOIA"]
+            Title:["Fair Labor Standards Act", "Freedom of Information Act"]
+            URI:["https://uscode.house.gov/view.xhtml?req=granuleid:USC-prelim-title29-section207", "https://uscode.house.gov/view.xhtml?req=granuleid:USC-prelim-title5-section552"]
+            Version:["2023", "2023"]
+            Digest:["", ""]
+        }
+        Citations: Atlas.CitationTable {
+            ID:["Citation.US.FLSA.207a1", "Citation.US.FOIA.552a6"]
+            Authority:["Authority.US.FLSA", "Authority.US.FOIA"]
+            Locator:["29 U.S.C. § 207(a)(1)", "5 U.S.C. § 552(a)(6)(A)(i)-(ii)"]
+        }
+        Requirements: Atlas.RequirementTable {
+            ID:["Requirement.Policy.FLSA.OvertimeThreshold", "Requirement.Policy.FOIA.TimelyAppealEntersReview"]
+            Text:["Hours above 40 in the modeled workweek enter overtime calculation.", "A timely modeled appeal enters review before disposition."]
+        }
+        Interpretations: Atlas.InterpretationTable {
+            ID:["Interpretation.Policy.FLSA.WeeklyThreshold", "Interpretation.Policy.FOIA.BoundedProcedure"]
+            Text:["Policy Lab models the weekly threshold as hours greater than 40 under its bounded assumptions.", "Policy Lab models the cited response and appeal windows with explicit supplied day indexes."]
+        }
+        Claims: Atlas.ClaimTable {
+            ID:["Claim.Policy.FLSA.TimeAndAHalf", "Claim.Policy.AmendmentImpactIsLocalized"]
+            Text:["Eligible overtime hours use one and one-half the supplied regular rate under the bounded integer-cent interpretation.", "Changing only the modeled threshold changes boundary cases and their dependent evidence without rewriting unrelated procedure."]
+        }
+        Symbols: Atlas.SymbolRefTable {
+            ID:["Symbol.PolicyLab.EvaluateOvertime", "Symbol.PolicyLab.DOJAppealProcess", "Symbol.PolicyLab.WorkweekHours"]
+            Symbol:["PolicyLab.EvaluateOvertime", "PolicyLab.DOJAppealProcess", "PolicyLab.WorkweekHours"]
+            Kind:[Atlas.SymbolKind.Function, Atlas.SymbolKind.Flow, Atlas.SymbolKind.Concept]
+        }
+        Evidence: Atlas.EvidenceRefTable {
+            ID:["Evidence.PolicyLab.ApplicantAboveThresholdReceivesOneAndOneHalfRate", "Evidence.PolicyLab.ThresholdBoundaryClassifiesOvertime", "Evidence.PolicyLab.TimelyAppealCannotSkipReview"]
+            Evidence:["PolicyLab.ApplicantAboveThresholdReceivesOneAndOneHalfRate", "PolicyLab.ThresholdBoundaryClassifiesOvertime", "PolicyLab.TimelyAppealCannotSkipReview"]
+            Kind:[Atlas.EvidenceKind.Fact, Atlas.EvidenceKind.Theory, Atlas.EvidenceKind.Fact]
+        }
+        Artifacts: Atlas.ArtifactRefTable {
+            ID:["Artifact.PolicyLab.Audit"]
+            Artifact:["PolicyLab.EmitPolicyLabAudit"]
+            Output:["policy_lab_audit.md"]
+        }
+        Links: Atlas.LinkTable {
+            From:[
+            "Citation.US.FLSA.207a1",
+            "Interpretation.Policy.FLSA.WeeklyThreshold",
+            "Symbol.PolicyLab.EvaluateOvertime",
+            "Symbol.PolicyLab.WorkweekHours",
+            "Evidence.PolicyLab.ApplicantAboveThresholdReceivesOneAndOneHalfRate",
+            "Evidence.PolicyLab.ThresholdBoundaryClassifiesOvertime",
+            "Requirement.Policy.FLSA.OvertimeThreshold",
+            "Requirement.Policy.FLSA.OvertimeThreshold",
+            "Artifact.PolicyLab.Audit",
+            "Interpretation.Policy.FOIA.BoundedProcedure",
+            "Symbol.PolicyLab.DOJAppealProcess",
+            "Evidence.PolicyLab.TimelyAppealCannotSkipReview",
+            "Claim.Policy.AmendmentImpactIsLocalized"
+            ]
+            Relation:[
+            Atlas.Relation.Supports,
+            Atlas.Relation.Interprets,
+            Atlas.Relation.Implements,
+            Atlas.Relation.Implements,
+            Atlas.Relation.Verifies,
+            Atlas.Relation.Verifies,
+            Atlas.Relation.Supports,
+            Atlas.Relation.Supports,
+            Atlas.Relation.Explains,
+            Atlas.Relation.Interprets,
+            Atlas.Relation.Implements,
+            Atlas.Relation.Verifies,
+            Atlas.Relation.DependsOn
+            ]
+            To:[
+            "Requirement.Policy.FLSA.OvertimeThreshold",
+            "Citation.US.FLSA.207a1",
+            "Requirement.Policy.FLSA.OvertimeThreshold",
+            "Requirement.Policy.FLSA.OvertimeThreshold",
+            "Requirement.Policy.FLSA.OvertimeThreshold",
+            "Requirement.Policy.FLSA.OvertimeThreshold",
+            "Claim.Policy.FLSA.TimeAndAHalf",
+            "Claim.Policy.AmendmentImpactIsLocalized",
+            "Requirement.Policy.FLSA.OvertimeThreshold",
+            "Citation.US.FOIA.552a6",
+            "Requirement.Policy.FOIA.TimelyAppealEntersReview",
+            "Requirement.Policy.FOIA.TimelyAppealEntersReview",
+            "Requirement.Policy.FLSA.OvertimeThreshold"
+            ]
+        }
+        Policy: policy
+    }
+}

Experiments/PolicyLab/M0/policy_lab_m0.oct

@@ -100,15 +100,6 @@ record AppealOutcome {
     Explanation: String
 }
 
-record SourceMapTable {
-    RuleID: String[]
-    Authority: String[]
-    Section: String[]
-    Interpretation: String[]
-    Symbol: String[]
-    Facts: String[]
-}
-
 fn AdmitWorkweekHours(raw: Int) -> WorkweekHours ! Error {
     return WorkweekHours(raw) ?
 }
@@ -274,17 +265,6 @@ fn ResolveRuleEffects(effects: RuleEffect[]) -> ConflictResult {
     }
 }
 
-fn BuildSourceMap() -> SourceMapTable {
-    return SourceMapTable {
-        RuleID:["PL-A-DOMAIN-1", "PL-A-207A1", "PL-A-213A1", "PL-B-APPEAL-90", "PL-B-DECISION-20"]
-        Authority:["Experiment domain", "Fair Labor Standards Act", "Fair Labor Standards Act", "Freedom of Information Act", "Freedom of Information Act"]
-        Section:["Structural assumption", "29 U.S.C. 207(a)(1)", "29 U.S.C. 213(a)(1)", "5 U.S.C. 552(a)(6)(A)(i)", "5 U.S.C. 552(a)(6)(A)(ii)"]
-        Interpretation:["Elapsed whole hours 0 through 168", "Whole-hour covered employment only", "Caller supplies already-classified exemption status", "Elapsed calendar-day index; day 90 is timely", "Supplied working-day index; day 20 is on time"]
-        Symbol:["WorkweekHours", "EvaluateOvertime", "Section213A1ExceptionApplies", "DOJAppealProcess", "DecisionTimelinessForWorkingDay"]
-        Facts:["InvalidWorkweekHoursAreRejected", "ThresholdBoundaryClassifiesOvertime", "DisqualifyingExceptionOverridesBaseRule", "AppealDeadlineBoundaryIsExplicit", "AppealDecisionTimelinessBoundaryIsExplicit"]
-    }
-}
-
 fn DecisionTimelinessForWorkingDay(day: Int) -> DecisionTimeliness {
     if day <= 20 {
         return DecisionTimeliness.OnTime
@@ -380,12 +360,10 @@ fn BuildPolicyAuditMarkdown() -> String[] {
     }
     let decision = EvaluateOvertime(sample)
     let history = RunSampleAppealHistory()
-    let sourceMap = BuildSourceMap()
     let settings = Markdown.KeyValueTable(
     ["specimen_a", "specimen_b", "law_status", "rounding", "convergence"],
     ["FLSA overtime, bounded", "DOJ FOIA administrative appeal, bounded", "executable interpretation, not law", "explicit half-cent ceiling", "static/runtime forms remain separate"]
     )
-    let sourceTable = Markdown.Table(sourceMap)
     let trace = Markdown.KeyValueTable(
     ["coverage", "exception", "threshold", "overtime_hours", "overtime_cents", "final"],
     [decision.Trace[0], decision.Trace[1], decision.Trace[2], String.From<Int>(decision.OvertimeHours), String.From<Int>(decision.OvertimeCompensationCents), decision.Trace[4]]
@@ -399,7 +377,7 @@ fn BuildPolicyAuditMarkdown() -> String[] {
     Markdown.H1("Policy Lab M0 audit"),
     Markdown.Paragraph("Research artifact only. This is an executable interpretation of cited authority, not legal advice or an authoritative statement of law."),
     Markdown.Section("Experiment",[settings]),
-    Markdown.Section("Source map",[sourceTable]),
+    Markdown.Section("Traceability",[Markdown.Paragraph("The package's canonical AtlasDocument links authorities, citations, bounded interpretations, requirements, implementation symbols, Facts, Theories, and this audit Artifact. Use oct atlas explain for the compiled source map.")]),
     Markdown.Section("Substantive decision trace",[trace]),
     Markdown.Section("Procedural history",[historyTable]),
     Markdown.Section("Exceptions and conflicts",[Markdown.Paragraph("The FLSA probe evaluates assumed coverage, then an explicit section 213(a)(1) exemption, then the hour threshold. Synthetic conflict probes return ConflictingRules instead of relying on first-match order.")]),

Experiments/PolicyLab/M0/policy_lab_m0.octest

@@ -270,17 +270,6 @@ fn ProceduralHistoryRecordsNoticeAppealReviewAndDecision() -> Void {
     Assert.Equal(first[4], second[4], "same case produces deterministic history")
 }
 
-/// PL-SOURCE-MAP: every major implemented rule has authority and Fact linkage.
-[Fact]
-fn SourceMapRetainsRuleAuthorityAndFactNames() -> Void {
-    let map = BuildSourceMap()
-    Assert.Equal(5, Len(map.RuleID), "source map row count")
-    Assert.Equal("PL-A-207A1", map.RuleID[1], "substantive rule ID")
-    Assert.Equal("29 U.S.C. 207(a)(1)", map.Section[1], "exact substantive section")
-    Assert.Equal("PL-B-APPEAL-90", map.RuleID[3], "procedural rule ID")
-    Assert.Equal("AppealDeadlineBoundaryIsExplicit", map.Facts[3], "source-to-Fact linkage")
-}
-
 /// PL-ARTIFACT: the explanation source is deterministic before filesystem write.
 [Fact]
 fn ExplanationArtifactSourceIsDeterministic() -> Void {

Experiments/PolicyLab/README.md

@@ -55,7 +55,7 @@ change; current authority must be checked before any real-world use.
 ## Corpus
 
 - `M0/policy_lab_m0.oct` — records, enums, refined Concepts, policy functions,
-  explicit exception/conflict logic, templates, captured callables, source map,
+  explicit exception/conflict logic, templates, captured callables, Atlas graph,
   Octomata procedure, and deterministic artifact builder.
 - `M0/policy_lab_m0.octest` — normative Facts, boundary Theories, negative
   propositions, amendment cases, procedural invariants, history, and artifact.
@@ -86,7 +86,9 @@ out/test-artifacts/experiments_policy_lab_m0/policy_lab_audit.md
 
 ## Known ambiguities and gaps
 
-- Literate source-law proximity and first-class provenance are absent.
+- Literate source-law proximity remains absent; first-class project provenance
+  now lives in the package's ordinary `AtlasDocument()` and is checked by
+  `oct atlas verify`.
 - Money, currency, calendar date, working-day, and holiday types are absent from
   the core surface used here.
 - Default/exception priority and conflict resolution are ordinary explicit code,

Experiments/PolicyLab/manifest.oct

@@ -23,7 +23,8 @@ fn Manifest() -> PackageManifest {
         Date: "2026-08-30"
         Dependencies:[
         Dependency {Name: "OctStd" VersionRequirement: "0.1.0"},
-        Dependency {Name: "Algorithms" VersionRequirement: "0.1.0"}
+        Dependency {Name: "Algorithms" VersionRequirement: "0.1.0"},
+        Dependency {Name: "Atlas" VersionRequirement: "0.1.0"}
         ]
     }
 }

Experiments/RiemannAtlas/M0/Atlas.oct

@@ -0,0 +1,46 @@
+package RiemannAtlas
+
+import Atlas
+
+fn AtlasDocument() -> Atlas.Document {
+    return Atlas.Document {
+        Authorities:[
+        Atlas.Authority {ID: "Authority.Riemann.M23Report" Title: "M23 certified variable-radius two-atom local optimum" URI: "https://github.com/yuechen-li-dev/Riemann/blob/7afc3c35a50610459a63088e88a91ebe86aa7d79/docs/m23-variable-radius-local-optimum.md" Version: "7afc3c35a50610459a63088e88a91ebe86aa7d79" Digest: "sha256:44cfcfa5c961143edd804317a4f4baf22ad0a3a3f0b9faaf1059c96670155453"},
+        Atlas.Authority {ID: "Authority.Riemann.M24Report" Title: "M24 global control of the contact-preserving two-atom component" URI: "https://github.com/yuechen-li-dev/Riemann/blob/7afc3c35a50610459a63088e88a91ebe86aa7d79/docs/m24-two-atom-component-control.md" Version: "7afc3c35a50610459a63088e88a91ebe86aa7d79" Digest: "sha256:bbd09ce3660491c63148a96fc953a6c8f954b46750331062d9517e0301ecf65b"},
+        Atlas.Authority {ID: "Authority.Riemann.M25Report" Title: "M25 B1 control and component optimum" URI: "https://github.com/yuechen-li-dev/Riemann/blob/7afc3c35a50610459a63088e88a91ebe86aa7d79/docs/m25-b1-component-global-optimum.md" Version: "7afc3c35a50610459a63088e88a91ebe86aa7d79" Digest: "sha256:68eb81168bce0e243e62f60217778a59cc6b153875295e573e2a016d28d883c5"}
+        ]
+        Citations:[
+        Atlas.Citation {ID: "Citation.Riemann.M23.Outcome" Authority: "Authority.Riemann.M23Report" Locator: "Outcome and certified optimizer sections"},
+        Atlas.Citation {ID: "Citation.Riemann.M24.ResidualWindow" Authority: "Authority.Riemann.M24Report" Locator: "Outcome and final residual-window conclusion"},
+        Atlas.Citation {ID: "Citation.Riemann.M25.Composition" Authority: "Authority.Riemann.M25Report" Locator: "M23/M24/M25 composition and whole-line feasibility sections"}
+        ]
+        Requirements:[]
+        Interpretations:[]
+        Claims:[
+        Atlas.Claim {ID: "Claim.Riemann.M23.LocalStationaryOptimizer" Text: "M23 establishes the bounded local stationary optimizer used by the later component argument."},
+        Atlas.Claim {ID: "Claim.Riemann.M24.OutsideWindowExclusion" Text: "M24 excludes improving candidates outside the bounded residual window used by the component argument."},
+        Atlas.Claim {ID: "Claim.Riemann.M25.B1GlobalWindowControl" Text: "M25 supplies B1 control across the remaining bounded global window."},
+        Atlas.Claim {ID: "Claim.Riemann.ContactPreservingTwoAtomComponentGlobalOptimum" Text: "The completed M23-M25 chain establishes the named contact-preserving two-atom component optimum; it is not a proof of the Riemann Hypothesis."}
+        ]
+        Symbols:[]
+        Evidence:[]
+        Artifacts:[]
+        Links:[
+        Atlas.Link {From: "Citation.Riemann.M23.Outcome" Relation: Atlas.Relation.Supports To: "Claim.Riemann.M23.LocalStationaryOptimizer"},
+        Atlas.Link {From: "Citation.Riemann.M24.ResidualWindow" Relation: Atlas.Relation.Supports To: "Claim.Riemann.M24.OutsideWindowExclusion"},
+        Atlas.Link {From: "Citation.Riemann.M25.Composition" Relation: Atlas.Relation.Supports To: "Claim.Riemann.M25.B1GlobalWindowControl"},
+        Atlas.Link {From: "Citation.Riemann.M25.Composition" Relation: Atlas.Relation.Supports To: "Claim.Riemann.ContactPreservingTwoAtomComponentGlobalOptimum"},
+        Atlas.Link {From: "Claim.Riemann.ContactPreservingTwoAtomComponentGlobalOptimum" Relation: Atlas.Relation.DerivedFrom To: "Claim.Riemann.M23.LocalStationaryOptimizer"},
+        Atlas.Link {From: "Claim.Riemann.ContactPreservingTwoAtomComponentGlobalOptimum" Relation: Atlas.Relation.DerivedFrom To: "Claim.Riemann.M24.OutsideWindowExclusion"},
+        Atlas.Link {From: "Claim.Riemann.ContactPreservingTwoAtomComponentGlobalOptimum" Relation: Atlas.Relation.DerivedFrom To: "Claim.Riemann.M25.B1GlobalWindowControl"},
+        Atlas.Link {From: "Claim.Riemann.M25.B1GlobalWindowControl" Relation: Atlas.Relation.DependsOn To: "Claim.Riemann.M24.OutsideWindowExclusion"},
+        Atlas.Link {From: "Claim.Riemann.M24.OutsideWindowExclusion" Relation: Atlas.Relation.DependsOn To: "Claim.Riemann.M23.LocalStationaryOptimizer"}
+        ]
+        Policy: Atlas.Policy {
+            RequireRequirementImplementation: false
+            RequireRequirementVerifier: false
+            RequireInterpretationCitation: false
+            RequireClaimSupport: false
+        }
+    }
+}

Experiments/RiemannAtlas/M0/riemann_atlas_m0.octest

@@ -0,0 +1,10 @@
+package RiemannAtlas
+
+[Fact]
+fn GlobalComponentClaimNamesThreeDerivedInputsWithoutClaimingFullRHProof() -> Void {
+    let document = AtlasDocument()
+    Assert.Equal(Len(document.Claims), 4, "three inputs plus the bounded component claim")
+    Assert.Equal(Len(document.Authorities), 3, "commit-pinned M23-M25 reports")
+    Assert.Equal(Len(document.Links), 9, "four source supports, three derivations, and two dependency links")
+    Assert.True(document.Claims[3].Text != "The Riemann Hypothesis is proved.", "scope remains bounded")
+}

Experiments/RiemannAtlas/README.md

@@ -0,0 +1,17 @@
+# Riemann Atlas M0 slice
+
+This is a deliberately narrow handoff graph for the M23 local optimizer, M24
+outside-window exclusion, M25 B1 global control, and the resulting named
+component optimum supplied in the Atlas M0 brief.
+
+The local Riemann checkout was inspected at commit
+`7afc3c35a50610459a63088e88a91ebe86aa7d79`. Its three milestone reports are
+commit-pinned Authorities with SHA-256 digests and precise Citations. The
+implementation, Go certificates, and separate Oct experiment packages are not
+part of this loaded Oct project, so M0 does not create string-only SymbolRef or
+EvidenceRef nodes for them: doing so would defeat resolution validation. The
+claim dependency graph remains useful and honest, while cross-package/repository
+Atlas federation is recorded as future work rather than simulated here.
+
+The final claim is explicitly component-scoped and makes no claim of a proof of
+the Riemann Hypothesis.

Experiments/RiemannAtlas/manifest.oct

@@ -0,0 +1,23 @@
+package Manifest
+
+record PackageManifest {
+    Name: String
+    Version: String
+    Description: String
+    Authors: String[]
+    Date: String
+    Dependencies: Dependency[]
+}
+
+record Dependency {Name: String VersionRequirement: String}
+
+fn Manifest() -> PackageManifest {
+    return PackageManifest {
+        Name: "RiemannAtlas"
+        Version: "0.1.0"
+        Description: "Atlas M0 handoff graph for the completed external Riemann M23-M25 slice"
+        Authors:["Codex"]
+        Date: "2026-08-30"
+        Dependencies:[Dependency {Name: "Atlas" VersionRequirement: "0.1.0"}]
+    }
+}

Language/reference/README.md

@@ -49,3 +49,4 @@ Start with [00-overview.md](./00-overview.md).
 - [34 octagon](./tooling/34-octagon.md)
 - [35 CLI](./tooling/35-cli.md)
 - [36 VSCode en-human view](./tooling/36-vscode.md)
+- [37 Atlas semantic documentation graphs](./tooling/37-atlas.md)