chore: sync main with development

lean/ProofAtlas/Astrolabe/Nerve.lean

@@ -3,6 +3,7 @@ Copyright (c) 2026 MathNetwork. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: MathNetwork
 -/
+import ProofAtlas.Util.Linter
 
 /-!
 # AstroNerve — a node in a content-addressable hypergraph
@@ -11,9 +12,9 @@ Identity is computed from record + refs (Merkle property).
 Each reference carries an abstract role tag.
 -/
 
--- Two fields: refs (ordered references with roles) and record (content).
--- Id, Role, Record are abstract types. identify computes id from
--- record + refs — content-addressing by construction.
+/-- A node in a content-addressable hypergraph.
+`refs`: ordered references with role tags. `record`: content.
+Identity computed from record + refs via `identify`. -/
 structure AstroNerve {Id : Type} {Role : Type} {Record : Type}
     (identify : Record → Array (Role × Id) → Id) where
   refs : Array (Role × Id)
@@ -25,43 +26,42 @@ namespace AstroNerve
 variable {Id : Type} {Role : Type} {Record : Type}
     {identify : Record → Array (Role × Id) → Id}
 
--- Compute identity from record + refs. Not stored — always derived.
+/-- Compute identity from record + refs. Not stored — always derived. -/
 def id (n : AstroNerve identify) : Id := identify n.record n.refs
 
--- Number of references this nerve has.
+/-- Number of references this nerve has. -/
 def width (n : AstroNerve identify) : Nat := n.refs.size
 
--- True if the nerve has no references (an atom / leaf node).
+/-- True if the nerve has no references (an atom / leaf node). -/
 def isAtom (n : AstroNerve identify) : Bool := n.refs.isEmpty
 
--- All referenced ids, in order, without roles.
+/-- All referenced ids, in order, without roles. -/
 def refIds (n : AstroNerve identify) : Array Id := n.refs.map (·.2)
 
--- All roles, in order, without ids.
+/-- All roles, in order, without ids. -/
 def refRoles (n : AstroNerve identify) : Array Role := n.refs.map (·.1)
 
--- Does this nerve reference a given id?
+/-- Does this nerve reference a given id? -/
 def containsRef [BEq Id] (n : AstroNerve identify) (i : Id) : Bool :=
   n.refs.any (fun ref => ref.2 == i)
 
--- Get the i-th ref (returns Option to handle out-of-bounds).
+/-- Get the i-th ref. Returns `none` if out of bounds. -/
 def refAt (n : AstroNerve identify) (i : Nat) : Option (Role × Id) :=
   n.refs[i]?
 
--- Add a ref at the end. Returns a new nerve (new id, Merkle property).
+/-- Add a ref at the end. Returns a new nerve with a new id. -/
 def pushRef (n : AstroNerve identify) (ref : Role × Id) : AstroNerve identify :=
   { refs := n.refs.push ref, record := n.record }
 
--- Remove the last ref. Returns a new nerve (new id).
+/-- Remove the last ref. Returns a new nerve with a new id. -/
 def popRef (n : AstroNerve identify) : AstroNerve identify :=
   { refs := n.refs.pop, record := n.record }
 
--- Keep only refs matching a predicate. Returns a new nerve (new id).
+/-- Keep only refs matching a predicate. Returns a new nerve. -/
 def filterRefs (n : AstroNerve identify) (p : (Role × Id) → Bool) : AstroNerve identify :=
   { refs := n.refs.filter p, record := n.record }
 
--- Swap two refs by index. Returns a new nerve (new id).
--- Panics if indices out of bounds.
+/-- Swap two refs by index. Returns a new nerve with a new id. -/
 def swapRefs [Inhabited Role] [Inhabited Id]
     (n : AstroNerve identify) (i j : Nat) : AstroNerve identify :=
   let a := n.refs
@@ -70,18 +70,17 @@ def swapRefs [Inhabited Role] [Inhabited Id]
   let a := a.set! j tmp
   { refs := a, record := n.record }
 
--- Reverse the order of all refs. Returns a new nerve (new id).
+/-- Reverse the order of all refs. Returns a new nerve. -/
 def reverseRefs (n : AstroNerve identify) : AstroNerve identify :=
   { refs := n.refs.reverse, record := n.record }
 
--- Replace ref at position i. Returns a new nerve (new id).
--- Panics if index out of bounds.
+/-- Replace ref at position i. Returns a new nerve with a new id. -/
 def setRef (n : AstroNerve identify) (i : Nat) (ref : Role × Id) : AstroNerve identify :=
   { refs := n.refs.set! i ref, record := n.record }
 
 end AstroNerve
 
--- ToString: show nerve as "Nerve(id=..., width=N)".
+/-- Show nerve as `Nerve(id=..., width=N)`. -/
 instance {Id Role Record : Type} {identify : Record → Array (Role × Id) → Id}
     [ToString Id] : ToString (AstroNerve identify) where
   toString n := s!"Nerve(id={n.id}, width={n.width})"

lean/ProofAtlas/Astrolabe/Net.lean

@@ -12,7 +12,7 @@ Built incrementally via `empty` and `addNerve!`.
 Injectivity and closure checked at compile time.
 -/
 
--- A net is an array of nerves sharing the same identify function.
+/-- A net is an array of nerves sharing the same identify function. -/
 structure AstroNet {Id : Type} [DecidableEq Id]
     {Role : Type} {Record : Type}
     (identify : Record → Array (Role × Id) → Id) where
@@ -24,129 +24,132 @@ variable {Id : Type} [DecidableEq Id]
     {Role : Type} [DecidableEq Role] {Record : Type} [DecidableEq Record]
     {identify : Record → Array (Role × Id) → Id}
 
--- Create an empty net.
+/-- Create an empty net. -/
 def empty (identify : Record → Array (Role × Id) → Id) : AstroNet identify where
   nerves := #[]
 
--- Number of nerves in the net.
+/-- Number of nerves in the net. -/
 def size (net : AstroNet identify) : Nat := net.nerves.size
 
--- Check if any nerve in the net has this id.
+/-- Check if any nerve in the net has this id. -/
 def hasId (net : AstroNet identify) (i : Id) : Bool :=
   net.nerves.any (fun n => n.id == i)
 
--- Find the nerve with this id. Returns none if not found.
+/-- Find the nerve with this id. Returns none if not found. -/
 def findById (net : AstroNet identify) (i : Id) : Option (AstroNerve identify) :=
   net.nerves.find? (fun n => n.id == i)
 
--- Get the record of the nerve with this id. Returns none if not found.
+/-- Get the record of the nerve with this id. Returns none if not found. -/
 def getRecord (net : AstroNet identify) (i : Id) : Option Record :=
   (net.findById i).map (·.record)
 
--- Check if a nerve can be safely added:
--- all refs must exist in the net (closure), and id must be fresh (injectivity).
+/-- Check if a nerve can be safely added:
+all refs must exist in the net (closure), and id must be fresh (injectivity). -/
 def canAdd (net : AstroNet identify) (n : AstroNerve identify) : Bool :=
   n.refs.all (fun ref => net.hasId ref.2) &&
   !net.hasId n.id
 
--- Add a nerve. Closure + injectivity checked at compile time.
--- If the check fails, the file won't compile.
+/-- Add a nerve. Closure + injectivity checked at compile time.
+If the check fails, the file won't compile. -/
 def addNerve! (net : AstroNet identify) (n : AstroNerve identify)
     (_h : net.canAdd n = true := by native_decide) :
     AstroNet identify where
   nerves := net.nerves.push n
 
--- All ids in the net, in insertion order.
+/-- All ids in the net, in insertion order. -/
 def ids (net : AstroNet identify) : Array Id :=
   net.nerves.map (·.id)
 
--- All atoms (nerves with no refs).
+/-- All atoms (nerves with no refs). -/
 def atoms (net : AstroNet identify) : Array (AstroNerve identify) :=
   net.nerves.filter (·.isAtom)
 
--- All non-atoms (nerves with refs).
+/-- All non-atoms (nerves with refs). -/
 def edges (net : AstroNet identify) : Array (AstroNerve identify) :=
   net.nerves.filter (!·.isAtom)
 
--- All nerves that reference a given id (reverse lookup).
+/-- All nerves that reference a given id (reverse lookup). -/
 def refsTo (net : AstroNet identify) (i : Id) : Array (AstroNerve identify) :=
   net.nerves.filter (·.containsRef i)
 
--- Does the net contain a nerve with this id?
+/-- Does the net contain a nerve with this id? -/
 def contains (net : AstroNet identify) (n : AstroNerve identify) : Bool :=
   net.hasId n.id
 
--- Is the net empty?
+/-- Is the net empty? -/
 def isEmpty (net : AstroNet identify) : Bool := net.nerves.isEmpty
 
--- Number of atoms.
+/-- Number of atoms. -/
 def atomCount (net : AstroNet identify) : Nat := net.atoms.size
 
--- Number of non-atoms (edges).
+/-- Number of non-atoms (edges). -/
 def edgeCount (net : AstroNet identify) : Nat := net.edges.size
 
--- Convert to List.
+/-- Convert to List. -/
 def toList (net : AstroNet identify) : List (AstroNerve identify) :=
   net.nerves.toList
 
--- Map a function over all nerves' records, producing a list of results.
+/-- Map a function over all nerves' records, producing a list of results. -/
 def mapRecords (net : AstroNet identify) (f : Record → α) : Array α :=
   net.nerves.map (fun n => f n.record)
 
--- Filter nerves by a predicate. Returns a plain array (not a net,
--- since filtered result may violate closure).
+/-- Filter nerves by a predicate. Returns a plain array (not a net,
+since filtered result may violate closure). -/
 def filterNerves (net : AstroNet identify) (p : AstroNerve identify → Bool) :
     Array (AstroNerve identify) :=
   net.nerves.filter p
 
--- Remove a nerve by id. Returns a plain array (not a net,
--- since removing a nerve may break closure for nerves that referenced it).
+/-- Remove a nerve by id. Returns a plain array (not a net,
+since removing a nerve may break closure for nerves that referenced it). -/
 def removeById (net : AstroNet identify) (i : Id) : Array (AstroNerve identify) :=
   net.nerves.filter (fun n => n.id != i)
 
--- Merge two nets. Returns a plain array (not a net,
--- since duplicates / broken closure must be resolved by the caller).
+/-- Merge two nets. Returns a plain array (not a net,
+since duplicates / broken closure must be resolved by the caller). -/
 def mergeNerves (net1 net2 : AstroNet identify) : Array (AstroNerve identify) :=
   net1.nerves ++ net2.nerves
 
--- Is every nerve in net1 also in net2 (by id)?
+/-- Is every nerve in net1 also in net2 (by id)? -/
 def isSubnetOf (net1 net2 : AstroNet identify) : Bool :=
   net1.nerves.all (fun n => net2.hasId n.id)
 
--- Get the i-th nerve by insertion order.
+/-- Get the i-th nerve by insertion order. -/
 def nerveAt (net : AstroNet identify) (i : Nat) : Option (AstroNerve identify) :=
   net.nerves[i]?
 
--- Total number of refs across all nerves.
+/-- Total number of refs across all nerves. -/
 def totalRefs (net : AstroNet identify) : Nat :=
   net.nerves.foldl (fun acc n => acc + n.width) 0
 
--- How many times is this id referenced across all nerves (in-degree).
+/-- How many times is this id referenced across all nerves (in-degree). -/
 def degree (net : AstroNet identify) (i : Id) : Nat :=
   net.nerves.foldl (fun acc n =>
     acc + n.refs.foldl (fun c ref => if ref.2 == i then c + 1 else c) 0) 0
 
--- Nerves that no other nerve references (root nodes).
+/-- Nerves that no other nerve references (root nodes). -/
 def orphans (net : AstroNet identify) : Array (AstroNerve identify) :=
   net.nerves.filter (fun n => net.degree n.id == 0)
 
--- Fold over all nerves from left.
+/-- Fold over all nerves from left. -/
 def foldl (net : AstroNet identify) (f : α → AstroNerve identify → α) (init : α) : α :=
   net.nerves.foldl f init
 
--- Map a function over all nerves.
+/-- Map a function over all nerves. -/
 def map (net : AstroNet identify) (f : AstroNerve identify → α) : Array α :=
   net.nerves.map f
 
--- Result of depth computation: finite depth, cycle, or not found.
+/-- Result of depth computation: finite depth, cycle, or not found. -/
 inductive DepthResult where
-  | depth (n : Nat)  -- finite depth
-  | cycle            -- participates in a cycle (infinite depth)
-  | notFound         -- id not in the net
+  /-- Finite depth. -/
+  | depth (n : Nat)
+  /-- Participates in a cycle (infinite depth). -/
+  | cycle
+  /-- Id not in the net. -/
+  | notFound
   deriving Repr, BEq, Inhabited
 
--- Compute depth of a nerve in the net.
--- atom = .depth 0, others = .depth (1 + max of refs), cycle = .cycle
+/-- Compute depth of a nerve in the net.
+atom = `.depth 0`, others = `.depth (1 + max of refs)`, cycle = `.cycle`. -/
 partial def depthOf (net : AstroNet identify) (i : Id) : DepthResult :=
   go i #[]
 where
@@ -167,38 +170,41 @@ where
               match d with | .depth n => max acc n | _ => acc) 0
             .depth (maxD + 1)
 
--- Is the net acyclic? (all nerves have finite depth)
+/-- Is the net acyclic? (all nerves have finite depth) -/
 def isAcyclic (net : AstroNet identify) : Bool :=
   net.nerves.all (fun n => match net.depthOf n.id with | .depth _ => true | _ => false)
 
--- Maximum depth in the net (none if any nerve has a cycle).
+/-- Maximum depth in the net (none if any nerve has a cycle). -/
 def maxDepth (net : AstroNet identify) : Option Nat :=
   let depths := net.nerves.map (fun n => net.depthOf n.id)
   if depths.any (· == .cycle) then none
   else some (depths.foldl (fun acc d =>
     match d with | .depth n => max acc n | _ => acc) 0)
 
--- Build a net directly from an array, without checking axioms.
--- Use this for testing or when you guarantee correctness externally.
+/-- Build a net directly from an array, without checking axioms.
+Use this for testing or when you guarantee correctness externally. -/
 def ofArray (nerves : Array (AstroNerve identify)) : AstroNet identify where
   nerves := nerves
 
--- Count the number of nerves involved in cycles.
+/-- Count the number of nerves involved in cycles. -/
 def cycleCount (net : AstroNet identify) : Nat :=
   net.nerves.filter (fun n => net.depthOf n.id == .cycle) |>.size
 
--- All nerves that are part of a cycle.
+/-- All nerves that are part of a cycle. -/
 def cyclicNerves (net : AstroNet identify) : Array (AstroNerve identify) :=
   net.nerves.filter (fun n => net.depthOf n.id == .cycle)
 
--- Depth of every nerve: list of (id, depth result) pairs.
+/-- Depth of every nerve: list of (id, depth result) pairs. -/
 def depthMap (net : AstroNet identify) [ToString Id] : Array (String × DepthResult) :=
   net.nerves.map (fun n => (toString n.id, net.depthOf n.id))
 
 end AstroNet
 
--- SCC support: outside namespace to avoid implicit parameter issues.
+/-! ## SCC support
 
+Outside namespace to avoid implicit parameter issues. -/
+
+/-- Can we reach `to_` from `from_` following refs? -/
 partial def _root_.AstroNet.canReach {α β γ : Type} [DecidableEq α]
     {f : γ → Array (β × α) → α}
     (net : AstroNet f) (from_ to_ : α) : Bool :=
@@ -213,6 +219,7 @@ where
       | some n =>
         (n.refs.map Prod.snd).any (fun rid => go rid (visited.push cur))
 
+/-- Compute strongly connected components of the net. -/
 def _root_.AstroNet.sccs {α β γ : Type} [DecidableEq α]
     {f : γ → Array (β × α) → α}
     (net : AstroNet f) : Array (Array α) := Id.run do
@@ -231,24 +238,26 @@ def _root_.AstroNet.sccs {α β γ : Type} [DecidableEq α]
     components := components.push comp
   return components
 
+/-- Number of non-trivial SCCs (size > 1, i.e. actual cycles). -/
 def _root_.AstroNet.sccCount {α β γ : Type} [DecidableEq α]
     {f : γ → Array (β × α) → α}
     (net : AstroNet f) : Nat :=
   (net.sccs.filter (·.size > 1)).size
 
+/-- All non-trivial SCCs (cycles) as arrays of ids. -/
 def _root_.AstroNet.printCycles {α β γ : Type} [DecidableEq α]
     {f : γ → Array (β × α) → α}
     (net : AstroNet f) : Array (Array α) :=
   net.sccs.filter (·.size > 1)
 
--- BEq: two nets are equal if they have the same nerves.
+/-- Two nets are equal if they have the same nerves. -/
 instance {α β γ : Type} [DecidableEq α]
     {f : γ → Array (β × α) → α}
     [BEq (AstroNerve f)] :
     BEq (AstroNet f) where
   beq a b := a.nerves == b.nerves
 
--- ToString: show net as "AstroNet(n nerves)".
+/-- Show net as `AstroNet(n nerves)`. -/
 instance {α β γ : Type} [DecidableEq α]
     {f : γ → Array (β × α) → α} :
     ToString (AstroNet f) where

lean/lakefile.toml

@@ -6,16 +6,12 @@ name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
 rev = "b2958bc1a0e2db353d06d6c019cd3f8bb8a1163c"
 
-[[lean_lib]]
-name = "ProofAtlasUtil"
-roots = ["ProofAtlas.Util.Linter.MathTag"]
-
 [[lean_lib]]
 name = "ProofAtlas"
 roots = ["ProofAtlas"]
 leanOptions = [
   { name = "weak.linter.mathlibStandardSet", value = true },
-  { name = "weak.linter.proofAtlasMathTag", value = true },
+  { name = "weak.linter.proofAtlasDocstringRequired", value = true },
 ]
 
 [[lean_lib]]