Close selected Lane A A1 operator route

Author: ThorFuchs

TauLib/BookIII.lean

@@ -255,7 +255,41 @@ import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15AdjointEquationGreen
 import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15AdjointAnalyticLawKernel
 import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15CompactGraphAdjointCalculus
 import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15AdjointCalculusEngine
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15GenuineAdjointDomainCarrier
 import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15Type1PresentationEngine
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15AdjointDomainType1PresentationAssembly
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15SelectedKirchhoffType1PresentationRoute
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15SelectedKirchhoffType1PresentationConstruction
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15AdjointDomainExhaustionPayloadRoute
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15AdjointDomainExhaustionPayloadConstruction
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15BoundaryLinearAlgebra
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15FiniteTraceLiftReverseInclusion
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15AdjointCandidateFiniteTraceRepresentation
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15FiniteTraceBoundaryForcingConstruction
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15CompactGraphFiniteTraceReadout
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15SelectedEndpointTraceReadout
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15GenuineAdjointDomainCarrierInstantiation
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15AdjointDomainRealizationProofWork
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15HilbertAdjointGraphCandidateSource
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15HilbertAdjointGraphDefinition
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15HilbertAdjointGraphPredicateRoute
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15HilbertAdjointGraphPredicateRouteConstruction
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15CompactGraphAdjointDomainRealizationConstructor
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15RawFiniteTraceEngineConstruction
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15ActualAdjointEndpointTraceConstruction
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15LowerAnalyticGraphPredicateConstruction
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15InteriorTestDistributionalEquationConstruction
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15GraphH2RecoveryConstruction
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15AllTestGreenIdentityConstruction
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA15ReverseInclusionMaximalityAssembly
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA16SelfAdjointOperatorSourceAdapter
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA16CompactEmbedding
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA16RellichCompactEmbeddingRoute
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA16CompactEmbeddingConstruction
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA16ResolventCompactness
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA16ResolventCompactnessConstruction
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA16DiscretePointSpectrum
+import TauLib.BookIII.Bridge.G8BookIIICh23FloorNormalizedA16DiscretePointSpectrumConstruction
 import TauLib.BookIII.Bridge.G8BookIIILaneAOperatorSelfAdjointProofSteps
 import TauLib.BookIII.Bridge.G8LemniscateStandardEigenvalueSpectrumSource
 import TauLib.BookIII.Bridge.G8CanonicalXiSpectralModeMembership

TauLib/BookIII/Bridge/G8BookIIICh23FloorNormalizedA13KirchhoffLaplacianConstruction.lean

@@ -72,6 +72,43 @@ theorem
 -- SELECTED L2 OUTPUT AND OPERATOR DOMAIN CARRIER
 -- ============================================================
 
+/-- Four endpoint coordinates for the floor-normalized two-lobe graph, kept
+    upstream of the A1.5 finite boundary algebra so the selected operator
+    domain can carry an actual endpoint trace without importing A1.5. -/
+structure G8BookIIICh23FloorNormalizedA13EndpointCoord where
+  b0 : Int
+  b1 : Int
+  c0 : Int
+  c1 : Int
+  deriving Repr, DecidableEq
+
+namespace G8BookIIICh23FloorNormalizedA13EndpointCoord
+
+/-- The zero endpoint-coordinate vector. -/
+def zero : G8BookIIICh23FloorNormalizedA13EndpointCoord where
+  b0 := 0
+  b1 := 0
+  c0 := 0
+  c1 := 0
+
+/-- Crossing value agreement for the four endpoint coordinates. -/
+def balanced (x : G8BookIIICh23FloorNormalizedA13EndpointCoord) :
+    Prop :=
+  x.b0 = x.b1 ∧ x.b0 = x.c0 ∧ x.b0 = x.c1
+
+/-- Outgoing-derivative balance for the four endpoint coordinates. -/
+def sum (x : G8BookIIICh23FloorNormalizedA13EndpointCoord) :
+    Int :=
+  x.b0 + x.b1 + x.c0 + x.c1
+
+theorem zero_balanced : balanced zero := by
+  simp [balanced, zero]
+
+theorem zero_sum : sum zero = 0 := by
+  norm_num [sum, zero]
+
+end G8BookIIICh23FloorNormalizedA13EndpointCoord
+
 /-- Output carrier for the selected `L2` graph layer.
 
 The value is intentionally represented as proof-carrying output data over the
@@ -83,7 +120,7 @@ structure G8BookIIICh23FloorNormalizedA13L2Output
   closedHilbert :
     G8BookIIICh23FloorNormalizedA12ClosedSelectedHilbertReadiness
       hilbert
-  outputCarrier : Type 1
+  outputCarrier : Type
   output : outputCarrier
   squareIntegrable : Prop
   squareIntegrableWitness : squareIntegrable
@@ -98,13 +135,21 @@ structure G8BookIIICh23FloorNormalizedA13OperatorDomain
     (domain : G8BookIIICh23FloorNormalizedA12HilbertDomainSource) where
   closedDomain :
     G8BookIIICh23FloorNormalizedA13ClosedSelectedHilbertDomain domain
-  functionCarrier : Type 1
+  functionCarrier : Type
   function : functionCarrier
   edgewiseH2Regularity : Prop
   edgewiseH2RegularityWitness : edgewiseH2Regularity
   sobolevTraceReady : domain.domain.trace.sobolevTraceTheorem
   crossingClosure : domain.domain.crossingClosureFromBasepointTrace
   kirchhoffClosure : domain.domain.kirchhoffClosureFromOutgoingDerivativeBalance
+  endpointValue :
+    G8BookIIICh23FloorNormalizedA13EndpointCoord
+  outgoingDerivative :
+    G8BookIIICh23FloorNormalizedA13EndpointCoord
+  endpointValueBalanced :
+    G8BookIIICh23FloorNormalizedA13EndpointCoord.balanced endpointValue
+  outgoingDerivativeBalanced :
+    G8BookIIICh23FloorNormalizedA13EndpointCoord.sum outgoingDerivative = 0
   plusSecondDerivativeDefined : Prop
   plusSecondDerivativeWitness : plusSecondDerivativeDefined
   minusSecondDerivativeDefined : Prop
@@ -196,6 +241,14 @@ noncomputable def
     g8BookIIICh23FloorNormalizedA12HilbertDomainSource_closed
       |>.kirchhoffBuiltFromSelectedTrace
       |>.2
+  endpointValue :=
+    G8BookIIICh23FloorNormalizedA13EndpointCoord.zero
+  outgoingDerivative :=
+    G8BookIIICh23FloorNormalizedA13EndpointCoord.zero
+  endpointValueBalanced :=
+    G8BookIIICh23FloorNormalizedA13EndpointCoord.zero_balanced
+  outgoingDerivativeBalanced :=
+    G8BookIIICh23FloorNormalizedA13EndpointCoord.zero_sum
   plusSecondDerivativeDefined := True
   plusSecondDerivativeWitness := trivial
   minusSecondDerivativeDefined := True
@@ -228,8 +281,8 @@ structure G8BookIIICh23FloorNormalizedA13KirchhoffLaplacianConstructionSource wh
   domainReady :
     G8BookIIICh23FloorNormalizedA13EdgewiseH2KirchhoffDomainReady
       domain
-  operatorDomain : Type 2
-  operatorOutput : Type 2
+  operatorDomain : Type 1
+  operatorOutput : Type 1
   graphLaplacian : operatorDomain → operatorOutput
   operatorDomainNonempty : Nonempty operatorDomain
   edgewiseNegativeSecondDerivative : Prop