Paper I · Lean source
GraphSourceObstruction.lean
1 claims linked to this Lean module
These links follow the claim index. They do not extend the recorded proof or Lean coverage.
Declared contract recorded Coverage and evidence
The cited release explicitly reports completion of its registered formal contract, under its exact hypotheses.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
Local imports (1)
PaperIRelease/GraphSourceObstruction.lean33 lines
Original source path
formal/current/PaperIRelease/GraphSourceObstruction.leanSkip declarations and read code
1 import PaperIRelease.GraphSources
2 set_option autoImplicit false
3 namespace Komorebi.PaperIRelease
4 open Komorebi.Foundation
5 open Komorebi.PacketNaturalityCompletion.Reachability
6 open Komorebi.PacketNaturalityCompletion.StrictNaturality
7 open FiniteDigraph
8 universe u v w
9 variable {K : Type u} [Field K] {X : Type v} [AddCommGroup X] [Module K X]
10 variable {I : Type w} [Fintype I] [DecidableEq I]
11 theorem generatedAlgebra_source_obstruction
12 (P : LinearProjectorFamily K X I) (ops : Set (Module.End K X))
13 (C : Sources (TransferEdge P ops)) (seeds : Set X)
14 (hseeds : ∀ s ∈ seeds, VectorSupported P {a | component (TransferEdge P ops) a ≠ C.val} s)
15 {x : X} (hx : x ≠ 0)
16 (hxC : VectorSupported P {a | component (TransferEdge P ops) a = C.val} x) :
17 x ∉ AlgebraGeneratedHull (packetGeneratedAlgebra P ops) seeds := by
18 classical
19 have hcoord : ∃ b, P.proj b x ≠ 0 := by
20 by_contra h
21 apply hx
22 calc
23 x = ∑ b, P.proj b x := (P.complete x).symm
24 _ = 0 := Finset.sum_eq_zero (fun b _ => by simpa using not_exists.mp h b)
25 obtain ⟨b, hb⟩ := hcoord
26 have hbC : component (TransferEdge P ops) b = C.val := by
27 by_contra h
28 exact hb (hxC b h)
29 apply generatedAlgebra_unreachable_obstruction P ops _ seeds hseeds ?_ hb
30 rintro ⟨a, ha, hab⟩
31 exact ha (no_reach_into_source (TransferEdge P ops) C hbC hab)
32 end Komorebi.PaperIRelease
33 #print axioms Komorebi.PaperIRelease.generatedAlgebra_source_obstruction
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: 2dd786af3eb2e483890123d459a5a4bd7ee031097f3e1ee67bbb1829aca5d0a3
Back to Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates