About this atlas — institutions and the Grothendieck construction

What an institution is

An institution (Goguen & Burstall) is the abstract definition of "a logical system", stripped to four parts: a category of signatures (the vocabularies you may declare), a functor giving the sentences over each signature, a functor giving the models, and a satisfaction relation ⊨ tying them together — subject to one axiom, the satisfaction condition: truth is invariant under change of notation (translating a sentence and translating a model agree on ⊨). First-order logic, higher-order logic, modal logic, and the dependent type theories of Lean and Agda are all institutions. Institution theory is the abstract model theory that treats them uniformly.

Translations are morphisms

A sound encoding of one logic into another — an institution comorphism (e.g. Lean into Agda) — preserves satisfaction. That is the precise meaning behind this atlas's arrows: ≡ equivalence, → comorphism, ⊨ sub-institution, — morphism.

The Grothendieck construction

Real systems live across several kernels at once (Lean, Agda, …), each its own institution, linked by translations. The Grothendieck construction (Diaconescu's Grothendieck institution) flattens that whole network of institutions-and-translations into a single institution: a signature becomes a pair (kernel, signature‑there), and models and sentences combine across the network. This is what lets one atlas certify a system whose proofs are spread across multiple proof assistants — heterogeneous, yet reasoned about as one object.

Why it is used here

This tool certifies an atlas of nodes (constructions, each bound to a real kernel declaration) and edges (the proven relations between them). Because both the binding and the relation taxonomy are institution-theoretic, the atlas is a Grothendieck‑flattened institution: it recognises a result and its cross-kernel mirror as the same object, and the satisfaction condition guarantees that a forcing or equivalence proved in one kernel transports soundly to another. For this bundle the institution is cubical Agda (cohesive homotopy type theory); the identical framework certifies a Lean development, or one spanning both.

What it buys you

Reading the diagram

Colour = relation type (cyan forcing, gold equivalence, …). A forcing edge descends to a byproduct its source generatively produces; an equivalence sits at the same height (provable sameness). Status: green verified, blue witness-bound (bound to a real proof, generativity deferred to the kernel), red a genuine gap. Each node and edge below lists its kernel handle, its statement (the proof type), and a link to the source.
relation type
construction │ verified (solid) witness-bound · kernel authority (dashed) vacancy (dotted)
· click a node to focus its neighborhood · scroll to zoom · drag to pan
construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction construction AdjointFormNadjointBridgeSym GoldenIrrationalgolden-no-pos CStarInductiveLimitexampleTower DedekindReal0#1 GoldenRinggolden-fib-5 CStarCompletiondiscreteGauge BridgePreludecrossBiInv GeometricBoundNgeomBoundℕ AdjointFormadjointFormSqSym RationalFielddiv-mul-cancel-neg Bracketwidth-2 GelfandPowerspectralPowerBridge IsoToEquivisoToEquiv Cassini_ EntropyRingH2-sym CohesiveToweridModality CStarRaycstar-axiom GoldenMatrixAlgebra★-antihom GoldenIrrationalZgolden-no-ℤ ReparamRealloc RealOrder<ℝ-asym ShapeNullificationshape-merges-0-1 RealNegation-ℝ-involutive CStarCompletionAlgebralaw-everywhere CertifiedSqrtsqrtBracket RealTranslation_+ℚ_ Archimedeanmult-arch GeometricBoundQpow49-bound InvolutionBorrowborrowed-suc-transport-neg LogicalEntropyh-three-orbit CertifiedSqrt2aboveSq Orderedlo<hi EntropyProvenanceentropy2-sym Metallic_ CohesionMetricSeparationpoint-no-separation FiniteCohesionfaithful-cohesion-witness GoldenAFAlgebragolden-tower-proper AffineRealaffineℝ RealApproxtrisect-n RealEmbedding-ℝ-ι OperatorNormmulSquare SpectralEdgespecEdgeBracket CrossingCorridortwo-walls-genuinely-distinct CorridorObservablesthe-corridor GeometricVanishpow49-vanish LogicalEntropyTEEBridgeh-screen-one-half Locatedφ LocatedLawgolden-upper-faithful Forcingconstant-rate-fails DiagonalCStarnorm-definite FaithfulCorridorwalls-distinct-univalently ApproxRealapproxℝ GoldenValuequad-mono OperatorNormSpectralcstarBracket MetallicEdge_ CrossCutlo<hi-cut GapBoundsucℤ≡+1 CStarLocatedfm2 SqrtRealRPosUpper GramPosDefgram-def PDTest2pd-forward AddRealaddℝ SpectralCStarspectral2-cstar SqrtRealdecide2 OperatorNormMagnitudecstarBracketAbs FaithfulModulusthe-effective-corridor GoldenCutφ LocatedReallocatedSquare QuadSqueezequad-squeeze SumOrder∑-mono-≤ QuadLemmassqrt-mono-≤ CauchySchwarzcauchy-schwarz SpecRadiusCutshiftP<0 LowerBracketeRayleigh SpectralEdgeRealspecEdge ZPhiRealzphiReal EntropyScreenentropy-screen-witness GoldenSpectrumgolden-modulus-two-sided GoldenLocatedgolden-modulus-bracket GoldenConjugateφ#ψ GoldenAFColimitgolden-af-witness Cofinalrunning≅dedekind DedekindBridgeruns-to-cut LocatedEq≈-sym QuadBoundquadBound OffDiagBoundoffdiag-sq ZPhiSpectralEdgezphiSpecEdge MetallicRealsqrtCorridor CorridorOrganismφ≢conv53 CompleteCorridorthe-complete-corridor AbsLemmasabs-triangle OneNormDiagBoundnSq PowerMonotoneentry≤oneNorm SpecBracketnotRayUp-diag OneNormSubmultoneNorm-submult SpecNormCutnotNormUp-low SquareRefinesquare-refine PowerScaffoldnormUp-from-pow QpowMonoqpow-mono SpecCutDisjointabsurd GeomGrowbern SpecLocHelpersbeat-suc GeomGrowArchqgrow GeomBeatgeom-beat SpecLocated∃Fin-dec SpecRadiusFaithfulU-sound SpecRadiusRealloc OperatorNormRealᵀᵀ ZPhiMatrixfaithful ZPhiOperatorNormzphiHouseNorm FrontierCapstonerunning≅dedekind RealCohesion18/18 proven · click to expand General63/63 proven · click to expand Theory9/9 proven · click to expand HottLane3/3 proven · click to expand Running11/11 proven · click to expand Foundations1/1 proven · click to expand Corridor6/6 proven · click to expand

Layout: layer = forcing depth from the roots; equivalent nodes share a layer (same height). Colour = relation type; line style + the status dot = verification (solid/green verified, dashed/amber supporting, dotted/red vacancy). Evidence digest 49ce23bc9fbef0169ed4359505f68baa9e223542dae471df227cb443e49971c5

nodes · associated proofs
ConstructionStatusStatement (the proof's kernel type)Source (file:line)ImportAxioms
GoldenCut
RealCohesion
verifiedφ : ℝcubical_agda/RealCohesion/GoldenCut.agda:418open import cubical_agda.RealCohesion.GoldenCut—
RealEmbedding
RealCohesion
verified-ℝ-ι : (q : ℚ) → -ℝ (ι q) ≡ ι (- q)cubical_agda/RealCohesion/RealEmbedding.agda:32open import cubical_agda.RealCohesion.RealEmbedding—
RealOrder
RealCohesion
verified<ℝ-asym : (x y : ℝ) → x <ℝ y → ¬ (y <ℝ x)cubical_agda/RealCohesion/RealOrder.agda:53open import cubical_agda.RealCohesion.RealOrder—
ShapeNullification
RealCohesion
verifiedshape-merges-0-1 : Path (∫ ℝ) ∣ 0ℝ ∣ ∣ 1ℝ ∣cubical_agda/RealCohesion/ShapeNullification.agda:65open import cubical_agda.RealCohesion.ShapeNullification—
GoldenConjugate
RealCohesion
verifiedφ#ψ : φ #ℝ ψcubical_agda/RealCohesion/GoldenConjugate.agda:51open import cubical_agda.RealCohesion.GoldenConjugate—
DiagonalCStar
RealCohesion
verifiednorm-definite : {n : ℕ} (f : Fin (suc n) → ℚ) → ‖ f ‖ ≡ 0 → (i : Fin (suc n)) → f i ≡ 0cubical_agda/RealCohesion/DiagonalCStar.agda:309open import cubical_agda.RealCohesion.DiagonalCStar—
GoldenValue
RealCohesion
verifiedquad-mono : (q r : ℚ) → 1 < q + r → q < r → (q · q + (- q)) < (r · r + (- r))cubical_agda/RealCohesion/GoldenValue.agda:88open import cubical_agda.RealCohesion.GoldenValue—
GoldenIrrationalZ
RealCohesion
verifiedgolden-no-ℤ : (a : ℤ) (bn : ℕ) → ¬ golden-eqℤ a (pos (suc bn))cubical_agda/RealCohesion/GoldenIrrationalZ.agda:64open import cubical_agda.RealCohesion.GoldenIrrationalZ—
GoldenMatrixAlgebra
RealCohesion
verified★-antihom : (n : ℕ) (M N : Mat n n) → (M ⋆ N) ★ ≡ N ★ ⋆ M ★cubical_agda/RealCohesion/GoldenMatrixAlgebra.agda:156open import cubical_agda.RealCohesion.GoldenMatrixAlgebra—
RealApprox
RealCohesion
verifiedtrisect-n : (n : ℕ) (x : ℝ) (a c : ℚ) → ⟦ lowerCut x ⟧ a → ⟦ upperCut x ⟧ c → a < c → ∥ Σ[ a' ∈ ℚ ] Σ[ c' ∈ ℚ ] ⟦ lowerCut x ⟧ a' × ⟦ upperCut x ⟧ c' × (a' < c') × ((c' …cubical_agda/RealCohesion/RealApprox.agda:150open import cubical_agda.RealCohesion.RealApprox—
CorridorOrganism
RealCohesion
verifiedφ≢conv53 : ¬ (φ ≡ ι conv53)cubical_agda/RealCohesion/CorridorOrganism.agda:63open import cubical_agda.RealCohesion.CorridorOrganism—
GoldenLocated
RealCohesion
verifiedgolden-modulus-bracket : (conv53 + (- conv32)) ≡ [ pos 1 / 1+ 5 ]cubical_agda/RealCohesion/GoldenLocated.agda:56open import cubical_agda.RealCohesion.GoldenLocated—
GoldenAFAlgebra
RealCohesion
verifiedgolden-tower-proper : (n : ℕ) (M : Mat n n) → ¬ (ιB M ≡ E00 n)cubical_agda/RealCohesion/GoldenAFAlgebra.agda:36open import cubical_agda.RealCohesion.GoldenAFAlgebra—
GoldenSpectrum
RealCohesion
verifiedgolden-modulus-two-sided : ((D : ℕ) → D <ℕ fib (suc (suc D))) -- reaches any precision × ((n : ℕ) → ¬ (negsign n ≡ pos 0)) -- never collapsescubical_agda/RealCohesion/GoldenSpectrum.agda:85open import cubical_agda.RealCohesion.GoldenSpectrum—
RealTranslation
RealCohesion
verified_+ℚ_ : ℝ → ℚ → ℝcubical_agda/RealCohesion/RealTranslation.agda:28open import cubical_agda.RealCohesion.RealTranslation—
GoldenIrrational
RealCohesion
verifiedgolden-no-pos : (a b : ℕ) → 1 ≤ a → 1 ≤ b → golden-eq a b → ⊥cubical_agda/RealCohesion/GoldenIrrational.agda:86open import cubical_agda.RealCohesion.GoldenIrrational—
RealNegation
RealCohesion
verified-ℝ-involutive : (x : ℝ) → -ℝ (-ℝ x) ≡ xcubical_agda/RealCohesion/RealNegation.agda:88open import cubical_agda.RealCohesion.RealNegation—
DedekindReal
RealCohesion
verified0#1 : 0ℝ #ℝ 1ℝcubical_agda/RealCohesion/DedekindReal.agda:197open import cubical_agda.RealCohesion.DedekindReal—
FiniteCohesion
Foundations
verifiedfaithful-cohesion-witness : FaithfulCohesionWitnesscubical_agda/Foundations/FiniteCohesion.agda:178open import cubical_agda.Foundations.FiniteCohesion—
LogicalEntropyTEEBridge
Theory
verifiedh-screen-one-half : logicalEntropy (2 ∷ 2 ∷ []) ≡ [ pos 1 / (1+ 1) ]cubical_agda/Theory/LogicalEntropyTEEBridge.agda:81open import cubical_agda.Theory.LogicalEntropyTEEBridge—
RationalField
Theory
verifieddiv-mul-cancel-neg : (p : ℚ) (k B : ℕ) → ((p · [ negsuc k / (1+ B) ]) /ℚ [ negsuc k / (1+ B) ]) ≡ pcubical_agda/Theory/RationalField.agda:168open import cubical_agda.Theory.RationalField—
CStarInductiveLimit
Theory
verifiedexampleTower : IsometricCStarTowercubical_agda/Theory/CStarInductiveLimit.agda:99open import cubical_agda.Theory.CStarInductiveLimit—
CStarCompletionAlgebra
Theory
verifiedlaw-everywhere : (f h : X → Y) (ω : ℕ → ℕ) (ωmono : (m n : ℕ) → m ≤ n → ω m ≤ ω n) (cf : (k : ℕ) (x y : X) → x ≈G[ ω k ] y → (f x) ≈H[ k ] (f y)) (ch : (k : ℕ) (x y : X) → x …cubical_agda/Theory/CStarCompletionAlgebra.agda:140open import cubical_agda.Theory.CStarCompletionAlgebra—
LogicalEntropy
Theory
verifiedh-three-orbit : logicalEntropy (1 ∷ 1 ∷ 1 ∷ []) ≡ [ pos 2 / (1+ 2) ]cubical_agda/Theory/LogicalEntropy.agda:139open import cubical_agda.Theory.LogicalEntropy—
GoldenRing
Theory
verifiedgolden-fib-5 : φ ^G 5 ≡ gφ (pos 3) (pos 5)cubical_agda/Theory/GoldenRing.agda:282open import cubical_agda.Theory.GoldenRing—
CohesiveTower
Theory
verifiedidModality : Modality {ℓ} (λ A → A)cubical_agda/Theory/CohesiveTower.agda:149open import cubical_agda.Theory.CohesiveTower—
CohesionMetricSeparation
Theory
verifiedpoint-no-separation : points (shape point) ≡ points (flat point)cubical_agda/Theory/CohesionMetricSeparation.agda:62open import cubical_agda.Theory.CohesionMetricSeparation—
CStarCompletion
Theory
verifieddiscreteGauge : (X : Type) → Gauge Xcubical_agda/Theory/CStarCompletion.agda:160open import cubical_agda.Theory.CStarCompletion—
CompleteCorridor
Corridor
verifiedthe-complete-corridor : CompleteEffectiveCorridorcubical_agda/Corridor/CompleteCorridor.agda:58open import cubical_agda.Corridor.CompleteCorridor—
GoldenAFColimit
Corridor
verifiedgolden-af-witness : GoldenAFcubical_agda/Corridor/GoldenAFColimit.agda:104open import cubical_agda.Corridor.GoldenAFColimit—
EntropyScreen
Corridor
verifiedentropy-screen-witness : EntropyScreencubical_agda/Corridor/EntropyScreen.agda:94open import cubical_agda.Corridor.EntropyScreen—
FaithfulCorridor
Corridor
verifiedwalls-distinct-univalently : crossing-path ≡ reflPath → ⊥cubical_agda/Corridor/FaithfulCorridor.agda:97open import cubical_agda.Corridor.FaithfulCorridor—
FaithfulModulus
Corridor
verifiedthe-effective-corridor : EffectiveCorridorcubical_agda/Corridor/FaithfulModulus.agda:126open import cubical_agda.Corridor.FaithfulModulus—
CrossingCorridor
Corridor
verifiedtwo-walls-genuinely-distinct : Σ LoFBoundaryState (λ s → Σ (s ≡ marked → ⊥) (λ _ → transport crossing-path s ≡ marked))cubical_agda/Corridor/CrossingCorridor.agda:169open import cubical_agda.Corridor.CrossingCorridor—
DedekindBridge
Running
verifiedruns-to-cut : (n : ℕ) → (ι (lo n) <ℝ φ) × (φ <ℝ ι (hi n))cubical_agda/Corridor/Running/DedekindBridge.agda:64open import cubical_agda.Corridor.Running.DedekindBridge—
LocatedLaw
Running
verifiedgolden-upper-faithful : (n : ℕ) → (hi n +ℚ oneℚ) <ℚ (hi n ·ℚ hi n)cubical_agda/Corridor/Running/LocatedLaw.agda:202open import cubical_agda.Corridor.Running.LocatedLaw—
Ordered
Running
verifiedlo<hi : (n : ℕ) → lo n <ℚ hi ncubical_agda/Corridor/Running/Ordered.agda:90open import cubical_agda.Corridor.Running.Ordered—
Located
Running
verifiedφ : ℝcubical_agda/RealCohesion/GoldenCut.agda:418open import cubical_agda.RealCohesion.GoldenCut—
SpectralEdge
Running
verifiedspecEdgeBracket : (a b d : ℚ) → 0 ≤ discriminant a b d → (D : ℕ) → Σ[ loλ ∈ ℚ ] Σ[ hiλ ∈ ℚ ] Σ[ slo ∈ ℚ ] Σ[ shi ∈ ℚ ] IsSqrtBracket (discriminant a b d) slo shi × (loλ ≡ ((a …cubical_agda/Corridor/Running/SpectralEdge.agda:32open import cubical_agda.Corridor.Running.SpectralEdge—
CertifiedSqrt
Running
verifiedsqrtBracket : (x : ℚ) → 0 ≤ x → (D : ℕ) → Σ[ lo ∈ ℚ ] Σ[ hi ∈ ℚ ] IsSqrtBracket x lo hicubical_agda/Corridor/Running/CertifiedSqrt.agda:60open import cubical_agda.Corridor.Running.CertifiedSqrt—
Cassini
Running
verified_ : fibℤ (suc 0) · fibℤ (suc 0) ≡ fibℤ 0 · fibℤ (suc (suc 0)) + altSign 0cubical_agda/Corridor/Running/Cassini.agda:67open import cubical_agda.Corridor.Running.Cassini—
CertifiedSqrt2
Running
verifiedaboveSq : (n : ℕ) → pos 2 ·ℤ (pQ (suc (dbl n)) ·ℤ pQ (suc (dbl n))) ≤ pP (suc (dbl n)) ·ℤ pP (suc (dbl n))cubical_agda/Corridor/Running/CertifiedSqrt2.agda:108open import cubical_agda.Corridor.Running.CertifiedSqrt2—
Bracket
Running
verifiedwidth-2 : width 2 ≡ [ pos 1 / (1+ 39) ]cubical_agda/Corridor/Running/Bracket.agda:105open import cubical_agda.Corridor.Running.Bracket—
Forcing
Running
verifiedconstant-rate-fails : (c : ℕ) → ¬ ((M : ℕ) → M < c)cubical_agda/Corridor/Running/Forcing.agda:81open import cubical_agda.Corridor.Running.Forcing—
CrossCut
Running
verifiedlo<hi-cut : (m n : ℕ) → lo m <ℚ hi ncubical_agda/Corridor/Running/CrossCut.agda:54open import cubical_agda.Corridor.Running.CrossCut—
CStarRay
General
verifiedcstar-axiom : {n : ℕ} (M : Mat n n) → (r : ℚ) → (normUp M r → rayUp ((M ᵀ) ⋆ M) (r · r)) × (rayUp ((M ᵀ) ⋆ M) (r · r) → normUp M r)cubical_agda/Corridor/Running/General/CStarRay.agda:60open import cubical_agda.Corridor.Running.General.CStarRay—
SpecBracket
General
verifiednotRayUp-diag : {n : ℕ} (A : Mat n n) (i : Fin n) (q : ℚ) → q < (A i i) → ¬ rayUp A qcubical_agda/Corridor/Running/General/SpecBracket.agda:44open import cubical_agda.Corridor.Running.General.SpecBracket—
SqrtReal
General
verifieddecide2 : Σ[ m2 ∈ ℚ ] (m1 < m2) × (m2 < r) → ∥ ⟦ Lp ⟧ q ⊎ ⟦ Up ⟧ r ∥₁ decide2 (m2 , m1<m2 , m2<r) with coreLoc m1 m2 0≤m1 m1<m2 ... | inl lc = ∣ inl ∣ m1 , q<m1 , lc ∣…cubical_agda/Corridor/Running/General/SqrtReal.agda:116open import cubical_agda.Corridor.Running.General.SqrtReal—
ZPhiOperatorNorm
General
verifiedzphiHouseNorm : {m : ℕ} → ZφMat (suc m) → ℝcubical_agda/Corridor/Running/General/ZPhiOperatorNorm.agda:57open import cubical_agda.Corridor.Running.General.ZPhiOperatorNorm—
GeometricVanish
General
verifiedpow49-vanish : (D : ℚ) → 0 ≤ D → (ε : ℚ) → 0 < ε → ∥ Σ[ k ∈ ℕ ] (pow49 k · D < ε) ∥₁cubical_agda/Corridor/Running/General/GeometricVanish.agda:46open import cubical_agda.Corridor.Running.General.GeometricVanish—
GramPosDef
General
verifiedgram-def : {n : ℕ} (v : Mat n 1) → ⟪ v , v ⟫ ≡ 0 → v ≡ (λ _ _ → 0)cubical_agda/Corridor/Running/General/GramPosDef.agda:96open import cubical_agda.Corridor.Running.General.GramPosDef—
SqrtRealR
General
verifiedPosUpper : ℝ → Type₀cubical_agda/Corridor/Running/General/SqrtRealR.agda:27open import cubical_agda.Corridor.Running.General.SqrtRealR—
LocatedReal
General
verifiedlocatedSquare : (r : LocatedReal) → ((n : ℕ) → 0 ≤ lo r n) → LocatedRealcubical_agda/Corridor/Running/General/LocatedReal.agda:54open import cubical_agda.Corridor.Running.General.LocatedReal—
EntropyProvenance
General
verifiedentropy2-sym : (p : ℚ) → logicalEntropy2 p ≡ logicalEntropy2 (1 - p)cubical_agda/Corridor/Running/General/EntropyProvenance.agda:52open import cubical_agda.Corridor.Running.General.EntropyProvenance—
LowerBracket
General
verifiedeRayleigh : {n : ℕ} (A : Mat n n) (i : Fin n) → ⟪ eVec i , A ⋆ eVec i ⟫ ≡ A i icubical_agda/Corridor/Running/General/LowerBracket.agda:45open import cubical_agda.Corridor.Running.General.LowerBracket—
SpecCutDisjoint
General
verifiedabsurd : qpow (L₁ +ℕ L₂) q < qpow (L₁ +ℕ L₂) q absurd = isTrans< (qpow (L₁ +ℕ L₂) q) ((pow2 (L₁ +ℕ L₂) M) (fst lo') (fst lo')) (qpow (L₁ +ℕ L₂) q) (snd lo') (isTrans≤…cubical_agda/Corridor/Running/General/SpecCutDisjoint.agda:88open import cubical_agda.Corridor.Running.General.SpecCutDisjoint—
EntropyRing
General
verifiedH2-sym : (p : ⟨ R ⟩) → H2 p ≡ H2 (1r - p) H2-sym p = solve! Rcubical_agda/Corridor/Running/General/EntropyRing.agda:15open import cubical_agda.Corridor.Running.General.EntropyRing—
Archimedean
General
verifiedmult-arch : (D ε : ℚ) → 0 < ε → ∥ Σ[ k ∈ ℕ ] (D < ε · [ pos (suc k) / 1+ 0 ]) ∥₁cubical_agda/Corridor/Running/General/Archimedean.agda:88open import cubical_agda.Corridor.Running.General.Archimedean—
OperatorNorm
General
verifiedmulSquare : (s x : ⟨ R ⟩) → (s · x) · (s · x) ≡ (s · s) · (x · x) mulSquare s x = solve! Rcubical_agda/Corridor/Running/General/OperatorNorm.agda:102open import cubical_agda.Corridor.Running.General.OperatorNorm—
CorridorObservables
General
verifiedthe-corridor : CorridorRowcubical_agda/Corridor/Running/General/CorridorObservables.agda:78open import cubical_agda.Corridor.Running.General.CorridorObservables—
SpecRadiusCut
General
verifiedshiftP<0 : shiftQ p 1 0 < 0 shiftP<0 = subst (_< 0) (sym (quad10 ℚCommRing (p - a) (- b) (p - d))) pa<0 ... | yes 0<qa with <Dec 0 (((q - a) · (q - d)) - ((- b) · (- b)…cubical_agda/Corridor/Running/General/SpecRadiusCut.agda:99open import cubical_agda.Corridor.Running.General.SpecRadiusCut—
OneNormDiagBound
General
verifiednSq : (n : ℕ) → ℚcubical_agda/Corridor/Running/General/OneNormDiagBound.agda:37open import cubical_agda.Corridor.Running.General.OneNormDiagBound—
MetallicEdge
General
verified_ : fibℤ (suc 0) · fibℤ (suc 0) ≡ fibℤ 0 · fibℤ (suc (suc 0)) + altSign 0cubical_agda/Corridor/Running/Cassini.agda:67open import cubical_agda.Corridor.Running.Cassini—
QuadSqueeze
General
verifiedquad-squeeze : (q r : ℚ) → ((q · q) + (- q)) < ((r · r) + (- r)) → 1 < (q + r) → q < rcubical_agda/Corridor/Running/General/QuadSqueeze.agda:29open import cubical_agda.Corridor.Running.General.QuadSqueeze—
QuadLemmas
General
verifiedsqrt-mono-≤ : (a b : ℚ) → 0 ≤ a → 0 ≤ b → (a · a) ≤ (b · b) → a ≤ bcubical_agda/Corridor/Running/General/QuadLemmas.agda:63open import cubical_agda.Corridor.Running.General.QuadLemmas—
GapBound
General
verifiedsucℤ≡+1 : (x : ℤ) → (x +ℤ pos 1) ≡ sucℤ xcubical_agda/Corridor/Running/General/GapBound.agda:24open import cubical_agda.Corridor.Running.General.GapBound—
GeometricBoundN
General
verifiedgeomBoundℕ : (k : ℕ) → p4 k · suc k ≤ p9 kcubical_agda/Corridor/Running/General/GeometricBoundN.agda:41open import cubical_agda.Corridor.Running.General.GeometricBoundN—
GeomGrowArch
General
verifiedqgrow : (t : ℚ) → 1 < t → (C : ℚ) → ∥ Σ[ L ∈ ℕ ] (C < qpow L t) ∥₁cubical_agda/Corridor/Running/General/GeomGrowArch.agda:46open import cubical_agda.Corridor.Running.General.GeomGrowArch—
AdjointForm
General
verifiedadjointFormSqSym : (a b d x₀ x₁ : ⟨ R ⟩) → (((a · x₀) + (b · x₁)) · ((a · x₀) + (b · x₁))) + (((b · x₀) + (d · x₁)) · ((b · x₀) + (d · x₁))) ≡ (x₀ · ((((a · a) + (b · b)) · x₀)…cubical_agda/Corridor/Running/General/AdjointForm.agda:44open import cubical_agda.Corridor.Running.General.AdjointForm—
GeometricBoundQ
General
verifiedpow49-bound : (k : ℕ) → pow49 k ≤ [ pos 1 / 1+ k ]cubical_agda/Corridor/Running/General/GeometricBoundQ.agda:50open import cubical_agda.Corridor.Running.General.GeometricBoundQ—
OffDiagBound
General
verifiedoffdiag-sq : {n : ℕ} (B : Mat n n) → (B ᵀ ≡ B) → (i j : Fin n) → ((B ⋆ B) i j · (B ⋆ B) i j) ≤ ((B ⋆ B) i i · (B ⋆ B) j j)cubical_agda/Corridor/Running/General/OffDiagBound.agda:41open import cubical_agda.Corridor.Running.General.OffDiagBound—
SpecLocated
General
verified∃Fin-dec : (n : ℕ) (P : Fin n → Type₀) → ((i : Fin n) → Dec (P i)) → Dec (Σ[ i ∈ Fin n ] P i)cubical_agda/Corridor/Running/General/SpecLocated.agda:39open import cubical_agda.Corridor.Running.General.SpecLocated—
SpecLocHelpers
General
verifiedbeat-suc : (s a b : ℚ) → 1 ≤ s → 0 ≤ a → (L : ℕ) → (s · qpow L a) < qpow L b → (s · qpow (suc L) a) < qpow (suc L) bcubical_agda/Corridor/Running/General/SpecLocHelpers.agda:47open import cubical_agda.Corridor.Running.General.SpecLocHelpers—
QpowMono
General
verifiedqpow-mono : (L : ℕ) (a b : ℚ) → 0 ≤ a → a ≤ b → qpow L a ≤ qpow L bcubical_agda/Corridor/Running/General/QpowMono.agda:24open import cubical_agda.Corridor.Running.General.QpowMono—
MetallicReal
General
verifiedsqrtCorridor : (D : ℚ) → 0 ≤ D → ℝcubical_agda/Corridor/Running/General/MetallicReal.agda:31open import cubical_agda.Corridor.Running.General.MetallicReal—
AdjointFormN
General
verifiedadjointBridgeSym : {n : ℕ} (M : Mat n n) (x : Mat n 1) → (M ᵀ ≡ M) → ((M ⋆ x) ᵀ) ⋆ (M ⋆ x) ≡ (x ᵀ) ⋆ ((M ⋆ M) ⋆ x) adjointBridgeSym M x symM = adjointBridge M x ∙ cong (λ A → (…cubical_agda/Corridor/Running/General/AdjointFormN.agda:47open import cubical_agda.Corridor.Running.General.AdjointFormN—
ApproxReal
General
verifiedapproxℝ : (x : ℝ) (δ : ℚ) → 0 < δ → ∥ Σ[ a ∈ ℚ ] Σ[ c ∈ ℚ ] ⟦ lowerCut x ⟧ a × ⟦ upperCut x ⟧ c × ((c + (- a)) < δ) ∥₁cubical_agda/Corridor/Running/General/ApproxReal.agda:82open import cubical_agda.Corridor.Running.General.ApproxReal—
OperatorNormMagnitude
General
verifiedcstarBracketAbs : (a b d slo shi : ℚ) → IsSqrtBracket (discriminant a b d) slo shi → IsSqrtBracket (discriminant ((a · a) + (b · b)) (b · (a + d)) ((b · b) + (d · d))) (absℚ (…cubical_agda/Corridor/Running/General/OperatorNormMagnitude.agda:33open import cubical_agda.Corridor.Running.General.OperatorNormMagnitude—
PDTest2
General
verifiedpd-forward : (a b d x y : ℚ) → 0 < a → 0 < ((a · d) - (b · b)) → (¬ (x ≡ 0)) ⊎ (¬ (y ≡ 0)) → 0 < quadℚ a b d x ycubical_agda/Corridor/Running/General/PDTest2.agda:156open import cubical_agda.Corridor.Running.General.PDTest2—
SpecNormCut
General
verifiednotNormUp-low : {n : ℕ} (M : Mat n n) → (M ᵀ ≡ M) → (r : ℚ) (i : Fin n) → (r · r) < ((M ⋆ M) i i) → ¬ normUp M rcubical_agda/Corridor/Running/General/SpecNormCut.agda:41open import cubical_agda.Corridor.Running.General.SpecNormCut—
FrontierCapstone
General
verifiedrunning≅dedekind : (q : ℚ) → (⟦ φL ⟧ q → ∥ Σ[ n ∈ ℕ ] (q < lo n) ∥₁) × (∥ Σ[ n ∈ ℕ ] (q < lo n) ∥₁ → ⟦ φL ⟧ q)cubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinal—
ZPhiSpectralEdge
General
verifiedzphiSpecEdge : PosUpper discℤφ → ℝ zphiSpecEdge posΔ = affineℝ half 0 0<half (addℝ traceℤφ (sqrtRealℝ discℤφ posΔ))cubical_agda/Corridor/Running/General/ZPhiSpectralEdge.agda:40open import cubical_agda.Corridor.Running.General.ZPhiSpectralEdge—
SpecRadiusReal
General
verifiedloc : (p r : ℚ) → p < r → ∥ ⟦ L ⟧ p ⊎ ⟦ U ⟧ r ∥₁ loc p r p<r with p ≟ q ... | lt p<q = ∣ inl p<q ∣₁ ... | eq p≡q = ∣ inr (subst (_< r) p≡q p<r) ∣₁ ... | gt q<p = ∣…cubical_agda/RealCohesion/DedekindReal.agda:165open import cubical_agda.RealCohesion.DedekindReal—
AbsLemmas
General
verifiedabs-triangle : (x y : ℚ) → absℚ (x + y) ≤ (absℚ x + absℚ y)cubical_agda/Corridor/Running/General/AbsLemmas.agda:57open import cubical_agda.Corridor.Running.General.AbsLemmas—
OneNormSubmult
General
verifiedoneNorm-submult : {n : ℕ} (A B : Mat n n) → oneNorm (A ⋆ B) ≤ (oneNorm A · oneNorm B)cubical_agda/Corridor/Running/General/OneNormSubmult.agda:96open import cubical_agda.Corridor.Running.General.OneNormSubmult—
SumOrder
General
verified∑-mono-≤ : (n : ℕ) (f g : FinVec ℚ n) (B : ℚ) → ((i : Fin n) → f i ≤ g i) → ∑ g ≤ B → ∑ f ≤ Bcubical_agda/Corridor/Running/General/SumOrder.agda:42open import cubical_agda.Corridor.Running.General.SumOrder—
AddReal
General
verifiedaddℝ : ℝ → ℝ → ℝcubical_agda/Corridor/Running/General/AddReal.agda:148open import cubical_agda.Corridor.Running.General.AddReal—
SquareRefine
General
verifiedsquare-refine : {n : ℕ} (A : Mat n n) → (A ᵀ ≡ A) → ((y : Mat n 1) → 0 ≤ ⟪ y , A ⋆ y ⟫) → (s : ℚ) → 0 ≤ s → rayUp (A ⋆ A) (s · s) → rayUp A scubical_agda/Corridor/Running/General/SquareRefine.agda:61open import cubical_agda.Corridor.Running.General.SquareRefine—
Cofinal
General
verifiedrunning≅dedekind : (q : ℚ) → (⟦ φL ⟧ q → ∥ Σ[ n ∈ ℕ ] (q < lo n) ∥₁) × (∥ Σ[ n ∈ ℕ ] (q < lo n) ∥₁ → ⟦ φL ⟧ q)cubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinal—
LocatedEq
General
verified≈-sym : {r s : LocatedReal} → r ≈ s → s ≈ rcubical_agda/Corridor/Running/General/LocatedEq.agda:63open import cubical_agda.Corridor.Running.General.LocatedEq—
CStarLocated
General
verifiedfm2 : (r a b d : ℚ) → ((r · r) - ((a · a) + (b · b))) ≡ (((- (a + d)) · (r + a)) + ((((r + a) · (r + d)) - (b · b))))cubical_agda/Corridor/Running/General/CStarLocated.agda:163open import cubical_agda.Corridor.Running.General.CStarLocated—
PowerMonotone
General
verifiedentry≤oneNorm : {n : ℕ} (A : Mat n n) (i : Fin n) → (A i i) ≤ oneNorm Acubical_agda/Corridor/Running/General/PowerMonotone.agda:50open import cubical_agda.Corridor.Running.General.PowerMonotone—
ZPhiReal
General
verifiedzphiReal : (a b : ℚ) → ℝcubical_agda/Corridor/Running/General/ZPhiReal.agda:86open import cubical_agda.Corridor.Running.General.ZPhiReal—
Metallic
General
verified_ : fibℤ (suc 0) · fibℤ (suc 0) ≡ fibℤ 0 · fibℤ (suc (suc 0)) + altSign 0cubical_agda/Corridor/Running/Cassini.agda:67open import cubical_agda.Corridor.Running.Cassini—
CauchySchwarz
General
verifiedcauchy-schwarz : {n : ℕ} (u v : Mat n 1) → (⟪ u , v ⟫ · ⟪ u , v ⟫) ≤ (⟪ u , u ⟫ · ⟪ v , v ⟫)cubical_agda/Corridor/Running/General/CauchySchwarz.agda:97open import cubical_agda.Corridor.Running.General.CauchySchwarz—
ReparamReal
General
verifiedloc : (p r : ℚ) → p < r → ∥ ⟦ L ⟧ p ⊎ ⟦ U ⟧ r ∥₁ loc p r p<r with p ≟ q ... | lt p<q = ∣ inl p<q ∣₁ ... | eq p≡q = ∣ inr (subst (_< r) p≡q p<r) ∣₁ ... | gt q<p = ∣…cubical_agda/RealCohesion/DedekindReal.agda:165open import cubical_agda.RealCohesion.DedekindReal—
PowerScaffold
General
verifiednormUp-from-pow : {n : ℕ} (M : Mat n n) → (M ᵀ ≡ M) → (q : ℚ) → (L : ℕ) → oneNorm (pow2 (suc L) M) < qpow (suc L) q → normUp M qcubical_agda/Corridor/Running/General/PowerScaffold.agda:69open import cubical_agda.Corridor.Running.General.PowerScaffold—
ZPhiMatrix
General
verifiedfaithful : {n : ℕ} (s s' : ZφMat n) → evalE t (zφMul s s') ≡ (evalE t s ⋆ evalE t s') faithful s s' = funExt (λ i → funExt (λ j → faithfulE s s' i j))cubical_agda/Corridor/Running/General/ZPhiMatrix.agda:131open import cubical_agda.Corridor.Running.General.ZPhiMatrix—
QuadBound
General
verifiedquadBound : {n : ℕ} (A : Mat n n) (x : Mat n 1) → ⟪ x , A ⋆ x ⟫ ≤ (oneNorm A · ⟪ x , x ⟫)cubical_agda/Corridor/Running/General/QuadBound.agda:99open import cubical_agda.Corridor.Running.General.QuadBound—
OperatorNormReal
General
verifiedᵀᵀ : {m n : ℕ} (M : Mat m n) → (M ᵀ) ᵀ ≡ Mcubical_agda/Corridor/Running/General/OperatorNormReal.agda:35open import cubical_agda.Corridor.Running.General.OperatorNormReal—
GeomGrow
General
verifiedbern : (t : ℚ) → 1 ≤ t → (L : ℕ) → (1 + (dyadicℚ L · (t - 1))) ≤ qpow L tcubical_agda/Corridor/Running/General/GeomGrow.agda:55open import cubical_agda.Corridor.Running.General.GeomGrow—
OperatorNormSpectral
General
verifiedcstarBracket : (a b d slo shi : ℚ) → 0 ≤ ((a + d) · (a + d)) → IsSqrtBracket (discriminant a b d) slo shi → IsSqrtBracket (discriminant ((a · a) + (b · b)) (b · (a + d)) ((…cubical_agda/Corridor/Running/General/OperatorNormSpectral.agda:35open import cubical_agda.Corridor.Running.General.OperatorNormSpectral—
SpectralEdgeReal
General
verifiedspecEdge : ℝ specEdge = reparamℝ φ ψ φ-mono ψ-mono φ∘ψ ψ∘φ (sqrtReal Δ 0≤Δ)cubical_agda/Corridor/Running/General/SpectralEdgeReal.agda:94open import cubical_agda.Corridor.Running.General.SpectralEdgeReal—
AffineReal
General
verifiedaffineℝ : ℝ → ℝ affineℝ = reparamℝ φ ψ φ-mono ψ-mono φ∘ψ ψ∘φcubical_agda/Corridor/Running/General/AffineReal.agda:82open import cubical_agda.Corridor.Running.General.AffineReal—
SpectralCStar
General
verifiedspectral2-cstar : (a b d λ₀ λ₁ : ℚ) → charEq ℚCommRing a b d λ₀ → charEq ℚCommRing a b d λ₁ → (‖ (λ i → twoEig λ₀ λ₁ i · twoEig λ₀ λ₁ i) ‖ ≡ ‖ twoEig λ₀ λ₁ ‖ · ‖ twoEig λ₀ λ₁ …cubical_agda/Corridor/Running/General/SpectralCStar.agda:48open import cubical_agda.Corridor.Running.General.SpectralCStar—
GeomBeat
General
verifiedgeom-beat : (q r : ℚ) → 0 < q → q < r → (C : ℚ) → ∥ Σ[ L ∈ ℕ ] ((C · qpow L q) < qpow L r) ∥₁cubical_agda/Corridor/Running/General/GeomBeat.agda:61open import cubical_agda.Corridor.Running.General.GeomBeat—
GelfandPower
General
verifiedspectralPowerBridge : {n : ℕ} (M : Mat n n) (k : ℕ) → (M ⋆ M) ^^ k ≡ M ^^ (k + k) spectralPowerBridge = sqPowcubical_agda/Corridor/Running/General/GelfandPower.agda:44open import cubical_agda.Corridor.Running.General.GelfandPower—
SpecRadiusFaithful
General
verifiedU-sound : {n' : ℕ} (M : Mat (suc n') (suc n')) (symM : M ᵀ ≡ M) (q : ℚ) → UppRaw M symM q → normUp M qcubical_agda/Corridor/Running/General/SpecRadiusFaithful.agda:31open import cubical_agda.Corridor.Running.General.SpecRadiusFaithful—
InvolutionBorrow
HottLane
verifiedborrowed-suc-transport-neg : transport (ua sucEquiv) (negsuc 0) ≡ pos 0cubical_agda/HottLane/InvolutionBorrow.agda:74open import cubical_agda.HottLane.InvolutionBorrow—
IsoToEquiv
HottLane
verifiedisoToEquiv : {A : Set ℓ} {B : Set ℓ'} → Iso A B → A ≃ Bcubical_agda/HottLane/IsoToEquiv.agda:89open import cubical_agda.HottLane.IsoToEquiv—
BridgePrelude
HottLane
verifiedcrossBiInv : BiInv crosscubical_agda/HottLane/BridgePrelude.agda:92open import cubical_agda.HottLane.BridgePrelude—
edges · proof source & what's needed
RelationStatusHandleSource (file:line)ImportShape / needs
DedekindReal ⊳ GoldenCut
construction
verifiedφcubical_agda/RealCohesion/GoldenCut.agda:418open import cubical_agda.RealCohesion.GoldenCutother
GoldenValue ⊳ GoldenCut
construction
verifiedφcubical_agda/RealCohesion/GoldenCut.agda:418open import cubical_agda.RealCohesion.GoldenCutother
RealApprox ⊳ GoldenCut
construction
verifiedφcubical_agda/RealCohesion/GoldenCut.agda:418open import cubical_agda.RealCohesion.GoldenCutother
RealNegation ⊳ GoldenCut
construction
verifiedφcubical_agda/RealCohesion/GoldenCut.agda:418open import cubical_agda.RealCohesion.GoldenCutother
DedekindReal ⊳ RealEmbedding
construction
verified-ℝ-ιcubical_agda/RealCohesion/RealEmbedding.agda:32open import cubical_agda.RealCohesion.RealEmbeddingeq
RealNegation ⊳ RealEmbedding
construction
verified-ℝ-ιcubical_agda/RealCohesion/RealEmbedding.agda:32open import cubical_agda.RealCohesion.RealEmbeddingeq
DedekindReal ⊳ RealOrder
construction
verified<ℝ-asymcubical_agda/RealCohesion/RealOrder.agda:53open import cubical_agda.RealCohesion.RealOrderother
DedekindReal ⊳ ShapeNullification
construction
verifiedshape-merges-0-1cubical_agda/RealCohesion/ShapeNullification.agda:65open import cubical_agda.RealCohesion.ShapeNullificationother
DedekindReal ⊳ GoldenConjugate
construction
verifiedφ#ψcubical_agda/RealCohesion/GoldenConjugate.agda:51open import cubical_agda.RealCohesion.GoldenConjugateother
RealNegation ⊳ GoldenConjugate
construction
verifiedφ#ψcubical_agda/RealCohesion/GoldenConjugate.agda:51open import cubical_agda.RealCohesion.GoldenConjugateother
RealTranslation ⊳ GoldenConjugate
construction
verifiedφ#ψcubical_agda/RealCohesion/GoldenConjugate.agda:51open import cubical_agda.RealCohesion.GoldenConjugateother
GoldenCut ⊳ GoldenConjugate
construction
verifiedφ#ψcubical_agda/RealCohesion/GoldenConjugate.agda:51open import cubical_agda.RealCohesion.GoldenConjugateother
RealApprox ⊳ DiagonalCStar
construction
verifiednorm-definitecubical_agda/RealCohesion/DiagonalCStar.agda:309open import cubical_agda.RealCohesion.DiagonalCStargen
RealNegation ⊳ DiagonalCStar
construction
verifiednorm-definitecubical_agda/RealCohesion/DiagonalCStar.agda:309open import cubical_agda.RealCohesion.DiagonalCStargen
RealApprox ⊳ GoldenValue
construction
verifiedquad-monocubical_agda/RealCohesion/GoldenValue.agda:88open import cubical_agda.RealCohesion.GoldenValueother
GoldenIrrational ⊳ GoldenIrrationalZ
construction
verifiedgolden-no-ℤcubical_agda/RealCohesion/GoldenIrrationalZ.agda:64open import cubical_agda.RealCohesion.GoldenIrrationalZother
GoldenRing ⊳ GoldenMatrixAlgebra
construction
verified★-antihomcubical_agda/RealCohesion/GoldenMatrixAlgebra.agda:156open import cubical_agda.RealCohesion.GoldenMatrixAlgebraeq
DedekindReal ⊳ RealApprox
construction
verifiedtrisect-ncubical_agda/RealCohesion/RealApprox.agda:150open import cubical_agda.RealCohesion.RealApproxgen
RealNegation ⊳ RealApprox
construction
verifiedtrisect-ncubical_agda/RealCohesion/RealApprox.agda:150open import cubical_agda.RealCohesion.RealApproxgen
DedekindReal ⊳ CorridorOrganism
construction
verifiedφ≢conv53cubical_agda/RealCohesion/CorridorOrganism.agda:63open import cubical_agda.RealCohesion.CorridorOrganismeq
GoldenCut ⊳ CorridorOrganism
construction
verifiedφ≢conv53cubical_agda/RealCohesion/CorridorOrganism.agda:63open import cubical_agda.RealCohesion.CorridorOrganismeq
GoldenConjugate ⊳ CorridorOrganism
construction
verifiedφ≢conv53cubical_agda/RealCohesion/CorridorOrganism.agda:63open import cubical_agda.RealCohesion.CorridorOrganismeq
GoldenIrrationalZ ⊳ CorridorOrganism
construction
verifiedφ≢conv53cubical_agda/RealCohesion/CorridorOrganism.agda:63open import cubical_agda.RealCohesion.CorridorOrganismeq
GoldenLocated ⊳ CorridorOrganism
construction
verifiedφ≢conv53cubical_agda/RealCohesion/CorridorOrganism.agda:63open import cubical_agda.RealCohesion.CorridorOrganismeq
RealOrder ⊳ CorridorOrganism
construction
verifiedφ≢conv53cubical_agda/RealCohesion/CorridorOrganism.agda:63open import cubical_agda.RealCohesion.CorridorOrganismeq
ShapeNullification ⊳ CorridorOrganism
construction
verifiedφ≢conv53cubical_agda/RealCohesion/CorridorOrganism.agda:63open import cubical_agda.RealCohesion.CorridorOrganismeq
DiagonalCStar ⊳ CorridorOrganism
construction
verifiedφ≢conv53cubical_agda/RealCohesion/CorridorOrganism.agda:63open import cubical_agda.RealCohesion.CorridorOrganismeq
GoldenAFAlgebra ⊳ CorridorOrganism
construction
verifiedφ≢conv53cubical_agda/RealCohesion/CorridorOrganism.agda:63open import cubical_agda.RealCohesion.CorridorOrganismeq
GoldenSpectrum ⊳ CorridorOrganism
construction
verifiedφ≢conv53cubical_agda/RealCohesion/CorridorOrganism.agda:63open import cubical_agda.RealCohesion.CorridorOrganismeq
DedekindReal ⊳ GoldenLocated
construction
verifiedgolden-modulus-bracketcubical_agda/RealCohesion/GoldenLocated.agda:56open import cubical_agda.RealCohesion.GoldenLocatedeq
GoldenCut ⊳ GoldenLocated
construction
verifiedgolden-modulus-bracketcubical_agda/RealCohesion/GoldenLocated.agda:56open import cubical_agda.RealCohesion.GoldenLocatedeq
GoldenMatrixAlgebra ⊳ GoldenAFAlgebra
construction
verifiedgolden-tower-propercubical_agda/RealCohesion/GoldenAFAlgebra.agda:36open import cubical_agda.RealCohesion.GoldenAFAlgebraeq
GoldenRing ⊳ GoldenSpectrum
construction
verifiedgolden-modulus-two-sidedcubical_agda/RealCohesion/GoldenSpectrum.agda:85open import cubical_agda.RealCohesion.GoldenSpectrumeq
FaithfulModulus ⊳ GoldenSpectrum
construction
verifiedgolden-modulus-two-sidedcubical_agda/RealCohesion/GoldenSpectrum.agda:85open import cubical_agda.RealCohesion.GoldenSpectrumeq
DedekindReal ⊳ RealTranslation
construction
verified_+ℚ_cubical_agda/RealCohesion/RealTranslation.agda:28open import cubical_agda.RealCohesion.RealTranslationother
DedekindReal ⊳ RealNegation
construction
verified-ℝ-involutivecubical_agda/RealCohesion/RealNegation.agda:88open import cubical_agda.RealCohesion.RealNegationeq
GoldenRing ⊳ LogicalEntropyTEEBridge
construction
verifiedh-screen-one-halfcubical_agda/Theory/LogicalEntropyTEEBridge.agda:81open import cubical_agda.Theory.LogicalEntropyTEEBridgeeq
LogicalEntropy ⊳ LogicalEntropyTEEBridge
construction
verifiedh-screen-one-halfcubical_agda/Theory/LogicalEntropyTEEBridge.agda:81open import cubical_agda.Theory.LogicalEntropyTEEBridgeeq
CStarCompletion ⊳ CStarCompletionAlgebra
construction
verifiedlaw-everywherecubical_agda/Theory/CStarCompletionAlgebra.agda:140open import cubical_agda.Theory.CStarCompletionAlgebragen
RationalField ⊳ LogicalEntropy
construction
verifiedh-three-orbitcubical_agda/Theory/LogicalEntropy.agda:139open import cubical_agda.Theory.LogicalEntropyeq
CohesiveTower ⊳ CohesionMetricSeparation
construction
verifiedpoint-no-separationcubical_agda/Theory/CohesionMetricSeparation.agda:62open import cubical_agda.Theory.CohesionMetricSeparationeq
FaithfulModulus ⊳ CompleteCorridor
construction
verifiedthe-complete-corridorcubical_agda/Corridor/CompleteCorridor.agda:58open import cubical_agda.Corridor.CompleteCorridorgen
GoldenAFColimit ⊳ CompleteCorridor
construction
verifiedthe-complete-corridorcubical_agda/Corridor/CompleteCorridor.agda:58open import cubical_agda.Corridor.CompleteCorridorgen
EntropyScreen ⊳ CompleteCorridor
construction
verifiedthe-complete-corridorcubical_agda/Corridor/CompleteCorridor.agda:58open import cubical_agda.Corridor.CompleteCorridorgen
FaithfulModulus ⊳ GoldenAFColimit
construction
verifiedgolden-af-witnesscubical_agda/Corridor/GoldenAFColimit.agda:104open import cubical_agda.Corridor.GoldenAFColimitother
FiniteCohesion ⊳ FaithfulCorridor
construction
verifiedwalls-distinct-univalentlycubical_agda/Corridor/FaithfulCorridor.agda:97open import cubical_agda.Corridor.FaithfulCorridorother
CrossingCorridor ⊳ FaithfulCorridor
construction
verifiedwalls-distinct-univalentlycubical_agda/Corridor/FaithfulCorridor.agda:97open import cubical_agda.Corridor.FaithfulCorridorother
BridgePrelude ⊳ FaithfulCorridor
construction
verifiedwalls-distinct-univalentlycubical_agda/Corridor/FaithfulCorridor.agda:97open import cubical_agda.Corridor.FaithfulCorridorother
FaithfulCorridor ⊳ FaithfulModulus
construction
verifiedthe-effective-corridorcubical_agda/Corridor/FaithfulModulus.agda:126open import cubical_agda.Corridor.FaithfulModulusother
BridgePrelude ⊳ CrossingCorridor
construction
verifiedtwo-walls-genuinely-distinctcubical_agda/Corridor/CrossingCorridor.agda:169open import cubical_agda.Corridor.CrossingCorridorgen
InvolutionBorrow ⊳ CrossingCorridor
construction
verifiedtwo-walls-genuinely-distinctcubical_agda/Corridor/CrossingCorridor.agda:169open import cubical_agda.Corridor.CrossingCorridorgen
DedekindReal ⊳ DedekindBridge
construction
verifiedruns-to-cutcubical_agda/Corridor/Running/DedekindBridge.agda:64open import cubical_agda.Corridor.Running.DedekindBridgeother
GoldenCut ⊳ DedekindBridge
construction
verifiedruns-to-cutcubical_agda/Corridor/Running/DedekindBridge.agda:64open import cubical_agda.Corridor.Running.DedekindBridgeother
Bracket ⊳ DedekindBridge
construction
verifiedruns-to-cutcubical_agda/Corridor/Running/DedekindBridge.agda:64open import cubical_agda.Corridor.Running.DedekindBridgeother
Located ⊳ DedekindBridge
construction
verifiedruns-to-cutcubical_agda/Corridor/Running/DedekindBridge.agda:64open import cubical_agda.Corridor.Running.DedekindBridgeother
CrossCut ⊳ DedekindBridge
construction
verifiedruns-to-cutcubical_agda/Corridor/Running/DedekindBridge.agda:64open import cubical_agda.Corridor.Running.DedekindBridgeother
LocatedLaw ⊳ DedekindBridge
construction
verifiedruns-to-cutcubical_agda/Corridor/Running/DedekindBridge.agda:64open import cubical_agda.Corridor.Running.DedekindBridgeother
Bracket ⊳ LocatedLaw
construction
verifiedgolden-upper-faithfulcubical_agda/Corridor/Running/LocatedLaw.agda:202open import cubical_agda.Corridor.Running.LocatedLawother
Cassini ⊳ LocatedLaw
construction
verifiedgolden-upper-faithfulcubical_agda/Corridor/Running/LocatedLaw.agda:202open import cubical_agda.Corridor.Running.LocatedLawother
Ordered ⊳ LocatedLaw
construction
verifiedgolden-upper-faithfulcubical_agda/Corridor/Running/LocatedLaw.agda:202open import cubical_agda.Corridor.Running.LocatedLawother
Bracket ⊳ Ordered
construction
verifiedlo<hicubical_agda/Corridor/Running/Ordered.agda:90open import cubical_agda.Corridor.Running.Orderedother
Cassini ⊳ Ordered
construction
verifiedlo<hicubical_agda/Corridor/Running/Ordered.agda:90open import cubical_agda.Corridor.Running.Orderedother
Bracket ⊳ Located
construction
verifiedφcubical_agda/RealCohesion/GoldenCut.agda:418open import cubical_agda.RealCohesion.GoldenCutother
Cassini ⊳ Located
construction
verifiedφcubical_agda/RealCohesion/GoldenCut.agda:418open import cubical_agda.RealCohesion.GoldenCutother
Ordered ⊳ Located
construction
verifiedφcubical_agda/RealCohesion/GoldenCut.agda:418open import cubical_agda.RealCohesion.GoldenCutother
CertifiedSqrt ⊳ SpectralEdge
construction
verifiedspecEdgeBracketcubical_agda/Corridor/Running/SpectralEdge.agda:32open import cubical_agda.Corridor.Running.SpectralEdgegen
DedekindReal ⊳ CertifiedSqrt
construction
verifiedsqrtBracketcubical_agda/Corridor/Running/CertifiedSqrt.agda:60open import cubical_agda.Corridor.Running.CertifiedSqrtgen
Bracket ⊳ CertifiedSqrt2
construction
verifiedaboveSqcubical_agda/Corridor/Running/CertifiedSqrt2.agda:108open import cubical_agda.Corridor.Running.CertifiedSqrt2other
Bracket ⊳ Forcing
construction
verifiedconstant-rate-failscubical_agda/Corridor/Running/Forcing.agda:81open import cubical_agda.Corridor.Running.Forcingother
Ordered ⊳ Forcing
construction
verifiedconstant-rate-failscubical_agda/Corridor/Running/Forcing.agda:81open import cubical_agda.Corridor.Running.Forcingother
Bracket ⊳ CrossCut
construction
verifiedlo<hi-cutcubical_agda/Corridor/Running/CrossCut.agda:54open import cubical_agda.Corridor.Running.CrossCutother
Ordered ⊳ CrossCut
construction
verifiedlo<hi-cutcubical_agda/Corridor/Running/CrossCut.agda:54open import cubical_agda.Corridor.Running.CrossCutother
Located ⊳ CrossCut
construction
verifiedlo<hi-cutcubical_agda/Corridor/Running/CrossCut.agda:54open import cubical_agda.Corridor.Running.CrossCutother
AdjointFormN ⊳ CStarRay
construction
verifiedcstar-axiomcubical_agda/Corridor/Running/General/CStarRay.agda:60open import cubical_agda.Corridor.Running.General.CStarRayother
DedekindReal ⊳ SpecBracket
construction
verifiednotRayUp-diagcubical_agda/Corridor/Running/General/SpecBracket.agda:44open import cubical_agda.Corridor.Running.General.SpecBracketother
GramPosDef ⊳ SpecBracket
construction
verifiednotRayUp-diagcubical_agda/Corridor/Running/General/SpecBracket.agda:44open import cubical_agda.Corridor.Running.General.SpecBracketother
QuadBound ⊳ SpecBracket
construction
verifiednotRayUp-diagcubical_agda/Corridor/Running/General/SpecBracket.agda:44open import cubical_agda.Corridor.Running.General.SpecBracketother
LowerBracket ⊳ SpecBracket
construction
verifiednotRayUp-diagcubical_agda/Corridor/Running/General/SpecBracket.agda:44open import cubical_agda.Corridor.Running.General.SpecBracketother
DedekindReal ⊳ SqrtReal
construction
verifieddecide2cubical_agda/Corridor/Running/General/SqrtReal.agda:116open import cubical_agda.Corridor.Running.General.SqrtRealgen
DiagonalCStar ⊳ SqrtReal
construction
verifieddecide2cubical_agda/Corridor/Running/General/SqrtReal.agda:116open import cubical_agda.Corridor.Running.General.SqrtRealgen
DedekindReal ⊳ ZPhiOperatorNorm
construction
verifiedzphiHouseNormcubical_agda/Corridor/Running/General/ZPhiOperatorNorm.agda:57open import cubical_agda.Corridor.Running.General.ZPhiOperatorNormother
OperatorNormReal ⊳ ZPhiOperatorNorm
construction
verifiedzphiHouseNormcubical_agda/Corridor/Running/General/ZPhiOperatorNorm.agda:57open import cubical_agda.Corridor.Running.General.ZPhiOperatorNormother
GeometricBoundQ ⊳ GeometricVanish
construction
verifiedpow49-vanishcubical_agda/Corridor/Running/General/GeometricVanish.agda:46open import cubical_agda.Corridor.Running.General.GeometricVanishgen
Archimedean ⊳ GeometricVanish
construction
verifiedpow49-vanishcubical_agda/Corridor/Running/General/GeometricVanish.agda:46open import cubical_agda.Corridor.Running.General.GeometricVanishgen
DiagonalCStar ⊳ GramPosDef
construction
verifiedgram-defcubical_agda/Corridor/Running/General/GramPosDef.agda:96open import cubical_agda.Corridor.Running.General.GramPosDefgen
DedekindReal ⊳ SqrtRealR
construction
verifiedPosUppercubical_agda/Corridor/Running/General/SqrtRealR.agda:27open import cubical_agda.Corridor.Running.General.SqrtRealRother
DiagonalCStar ⊳ SqrtRealR
construction
verifiedPosUppercubical_agda/Corridor/Running/General/SqrtRealR.agda:27open import cubical_agda.Corridor.Running.General.SqrtRealRother
DiagonalCStar ⊳ LocatedReal
construction
verifiedlocatedSquarecubical_agda/Corridor/Running/General/LocatedReal.agda:54open import cubical_agda.Corridor.Running.General.LocatedRealother
Bracket ⊳ LocatedReal
construction
verifiedlocatedSquarecubical_agda/Corridor/Running/General/LocatedReal.agda:54open import cubical_agda.Corridor.Running.General.LocatedRealother
Ordered ⊳ LocatedReal
construction
verifiedlocatedSquarecubical_agda/Corridor/Running/General/LocatedReal.agda:54open import cubical_agda.Corridor.Running.General.LocatedRealother
Located ⊳ LocatedReal
construction
verifiedlocatedSquarecubical_agda/Corridor/Running/General/LocatedReal.agda:54open import cubical_agda.Corridor.Running.General.LocatedRealother
EntropyRing ⊳ EntropyProvenance
construction
verifiedentropy2-symcubical_agda/Corridor/Running/General/EntropyProvenance.agda:52open import cubical_agda.Corridor.Running.General.EntropyProvenanceeq
GramPosDef ⊳ LowerBracket
construction
verifiedeRayleighcubical_agda/Corridor/Running/General/LowerBracket.agda:45open import cubical_agda.Corridor.Running.General.LowerBracketeq
DiagonalCStar ⊳ SpecCutDisjoint
construction
verifiedabsurdcubical_agda/Corridor/Running/General/SpecCutDisjoint.agda:88open import cubical_agda.Corridor.Running.General.SpecCutDisjointeq
GramPosDef ⊳ SpecCutDisjoint
construction
verifiedabsurdcubical_agda/Corridor/Running/General/SpecCutDisjoint.agda:88open import cubical_agda.Corridor.Running.General.SpecCutDisjointeq
QuadBound ⊳ SpecCutDisjoint
construction
verifiedabsurdcubical_agda/Corridor/Running/General/SpecCutDisjoint.agda:88open import cubical_agda.Corridor.Running.General.SpecCutDisjointeq
AdjointFormN ⊳ SpecCutDisjoint
construction
verifiedabsurdcubical_agda/Corridor/Running/General/SpecCutDisjoint.agda:88open import cubical_agda.Corridor.Running.General.SpecCutDisjointeq
PowerScaffold ⊳ SpecCutDisjoint
construction
verifiedabsurdcubical_agda/Corridor/Running/General/SpecCutDisjoint.agda:88open import cubical_agda.Corridor.Running.General.SpecCutDisjointeq
PowerMonotone ⊳ SpecCutDisjoint
construction
verifiedabsurdcubical_agda/Corridor/Running/General/SpecCutDisjoint.agda:88open import cubical_agda.Corridor.Running.General.SpecCutDisjointeq
OneNormSubmult ⊳ SpecCutDisjoint
construction
verifiedabsurdcubical_agda/Corridor/Running/General/SpecCutDisjoint.agda:88open import cubical_agda.Corridor.Running.General.SpecCutDisjointeq
EntropyProvenance ⊳ CorridorObservables
construction
verifiedthe-corridorcubical_agda/Corridor/Running/General/CorridorObservables.agda:78open import cubical_agda.Corridor.Running.General.CorridorObservablesother
PDTest2 ⊳ SpecRadiusCut
construction
verifiedshiftP<0cubical_agda/Corridor/Running/General/SpecRadiusCut.agda:99open import cubical_agda.Corridor.Running.General.SpecRadiusCuteq
DiagonalCStar ⊳ SpecRadiusCut
construction
verifiedshiftP<0cubical_agda/Corridor/Running/General/SpecRadiusCut.agda:99open import cubical_agda.Corridor.Running.General.SpecRadiusCuteq
DiagonalCStar ⊳ OneNormDiagBound
construction
verifiednSqcubical_agda/Corridor/Running/General/OneNormDiagBound.agda:37open import cubical_agda.Corridor.Running.General.OneNormDiagBoundother
GramPosDef ⊳ OneNormDiagBound
construction
verifiednSqcubical_agda/Corridor/Running/General/OneNormDiagBound.agda:37open import cubical_agda.Corridor.Running.General.OneNormDiagBoundother
QuadLemmas ⊳ OneNormDiagBound
construction
verifiednSqcubical_agda/Corridor/Running/General/OneNormDiagBound.agda:37open import cubical_agda.Corridor.Running.General.OneNormDiagBoundother
QuadBound ⊳ OneNormDiagBound
construction
verifiednSqcubical_agda/Corridor/Running/General/OneNormDiagBound.agda:37open import cubical_agda.Corridor.Running.General.OneNormDiagBoundother
SumOrder ⊳ OneNormDiagBound
construction
verifiednSqcubical_agda/Corridor/Running/General/OneNormDiagBound.agda:37open import cubical_agda.Corridor.Running.General.OneNormDiagBoundother
AdjointFormN ⊳ OneNormDiagBound
construction
verifiednSqcubical_agda/Corridor/Running/General/OneNormDiagBound.agda:37open import cubical_agda.Corridor.Running.General.OneNormDiagBoundother
OffDiagBound ⊳ OneNormDiagBound
construction
verifiednSqcubical_agda/Corridor/Running/General/OneNormDiagBound.agda:37open import cubical_agda.Corridor.Running.General.OneNormDiagBoundother
CertifiedSqrt ⊳ MetallicEdge
construction
verified_cubical_agda/Corridor/Running/Cassini.agda:67open import cubical_agda.Corridor.Running.Cassinieq
SpectralEdge ⊳ MetallicEdge
construction
verified_cubical_agda/Corridor/Running/Cassini.agda:67open import cubical_agda.Corridor.Running.Cassinieq
DiagonalCStar ⊳ QuadLemmas
construction
verifiedsqrt-mono-≤cubical_agda/Corridor/Running/General/QuadLemmas.agda:63open import cubical_agda.Corridor.Running.General.QuadLemmasother
GramPosDef ⊳ QuadLemmas
construction
verifiedsqrt-mono-≤cubical_agda/Corridor/Running/General/QuadLemmas.agda:63open import cubical_agda.Corridor.Running.General.QuadLemmasother
Bracket ⊳ GapBound
construction
verifiedsucℤ≡+1cubical_agda/Corridor/Running/General/GapBound.agda:24open import cubical_agda.Corridor.Running.General.GapBoundeq
LocatedLaw ⊳ GapBound
construction
verifiedsucℤ≡+1cubical_agda/Corridor/Running/General/GapBound.agda:24open import cubical_agda.Corridor.Running.General.GapBoundeq
Ordered ⊳ GapBound
construction
verifiedsucℤ≡+1cubical_agda/Corridor/Running/General/GapBound.agda:24open import cubical_agda.Corridor.Running.General.GapBoundeq
PowerScaffold ⊳ GeomGrowArch
construction
verifiedqgrowcubical_agda/Corridor/Running/General/GeomGrowArch.agda:46open import cubical_agda.Corridor.Running.General.GeomGrowArchgen
GeomGrow ⊳ GeomGrowArch
construction
verifiedqgrowcubical_agda/Corridor/Running/General/GeomGrowArch.agda:46open import cubical_agda.Corridor.Running.General.GeomGrowArchgen
Archimedean ⊳ GeomGrowArch
construction
verifiedqgrowcubical_agda/Corridor/Running/General/GeomGrowArch.agda:46open import cubical_agda.Corridor.Running.General.GeomGrowArchgen
GeometricBoundN ⊳ GeometricBoundQ
construction
verifiedpow49-boundcubical_agda/Corridor/Running/General/GeometricBoundQ.agda:50open import cubical_agda.Corridor.Running.General.GeometricBoundQother
AdjointFormN ⊳ OffDiagBound
construction
verifiedoffdiag-sqcubical_agda/Corridor/Running/General/OffDiagBound.agda:41open import cubical_agda.Corridor.Running.General.OffDiagBoundother
GramPosDef ⊳ OffDiagBound
construction
verifiedoffdiag-sqcubical_agda/Corridor/Running/General/OffDiagBound.agda:41open import cubical_agda.Corridor.Running.General.OffDiagBoundother
CauchySchwarz ⊳ OffDiagBound
construction
verifiedoffdiag-sqcubical_agda/Corridor/Running/General/OffDiagBound.agda:41open import cubical_agda.Corridor.Running.General.OffDiagBoundother
AdjointFormN ⊳ SpecLocated
construction
verified∃Fin-deccubical_agda/Corridor/Running/General/SpecLocated.agda:39open import cubical_agda.Corridor.Running.General.SpecLocatedgen
QuadBound ⊳ SpecLocated
construction
verified∃Fin-deccubical_agda/Corridor/Running/General/SpecLocated.agda:39open import cubical_agda.Corridor.Running.General.SpecLocatedgen
OneNormDiagBound ⊳ SpecLocated
construction
verified∃Fin-deccubical_agda/Corridor/Running/General/SpecLocated.agda:39open import cubical_agda.Corridor.Running.General.SpecLocatedgen
PowerScaffold ⊳ SpecLocated
construction
verified∃Fin-deccubical_agda/Corridor/Running/General/SpecLocated.agda:39open import cubical_agda.Corridor.Running.General.SpecLocatedgen
QpowMono ⊳ SpecLocated
construction
verified∃Fin-deccubical_agda/Corridor/Running/General/SpecLocated.agda:39open import cubical_agda.Corridor.Running.General.SpecLocatedgen
GeomBeat ⊳ SpecLocated
construction
verified∃Fin-deccubical_agda/Corridor/Running/General/SpecLocated.agda:39open import cubical_agda.Corridor.Running.General.SpecLocatedgen
SpecLocHelpers ⊳ SpecLocated
construction
verified∃Fin-deccubical_agda/Corridor/Running/General/SpecLocated.agda:39open import cubical_agda.Corridor.Running.General.SpecLocatedgen
DiagonalCStar ⊳ SpecLocHelpers
construction
verifiedbeat-succubical_agda/Corridor/Running/General/SpecLocHelpers.agda:47open import cubical_agda.Corridor.Running.General.SpecLocHelpersother
DedekindReal ⊳ SpecLocHelpers
construction
verifiedbeat-succubical_agda/Corridor/Running/General/SpecLocHelpers.agda:47open import cubical_agda.Corridor.Running.General.SpecLocHelpersother
GramPosDef ⊳ SpecLocHelpers
construction
verifiedbeat-succubical_agda/Corridor/Running/General/SpecLocHelpers.agda:47open import cubical_agda.Corridor.Running.General.SpecLocHelpersother
QuadLemmas ⊳ SpecLocHelpers
construction
verifiedbeat-succubical_agda/Corridor/Running/General/SpecLocHelpers.agda:47open import cubical_agda.Corridor.Running.General.SpecLocHelpersother
QpowMono ⊳ SpecLocHelpers
construction
verifiedbeat-succubical_agda/Corridor/Running/General/SpecLocHelpers.agda:47open import cubical_agda.Corridor.Running.General.SpecLocHelpersother
OneNormDiagBound ⊳ SpecLocHelpers
construction
verifiedbeat-succubical_agda/Corridor/Running/General/SpecLocHelpers.agda:47open import cubical_agda.Corridor.Running.General.SpecLocHelpersother
PowerScaffold ⊳ SpecLocHelpers
construction
verifiedbeat-succubical_agda/Corridor/Running/General/SpecLocHelpers.agda:47open import cubical_agda.Corridor.Running.General.SpecLocHelpersother
DiagonalCStar ⊳ QpowMono
construction
verifiedqpow-monocubical_agda/Corridor/Running/General/QpowMono.agda:24open import cubical_agda.Corridor.Running.General.QpowMonoother
PowerScaffold ⊳ QpowMono
construction
verifiedqpow-monocubical_agda/Corridor/Running/General/QpowMono.agda:24open import cubical_agda.Corridor.Running.General.QpowMonoother
DedekindReal ⊳ MetallicReal
construction
verifiedsqrtCorridorcubical_agda/Corridor/Running/General/MetallicReal.agda:31open import cubical_agda.Corridor.Running.General.MetallicRealother
SqrtReal ⊳ MetallicReal
construction
verifiedsqrtCorridorcubical_agda/Corridor/Running/General/MetallicReal.agda:31open import cubical_agda.Corridor.Running.General.MetallicRealother
SpectralEdgeReal ⊳ MetallicReal
construction
verifiedsqrtCorridorcubical_agda/Corridor/Running/General/MetallicReal.agda:31open import cubical_agda.Corridor.Running.General.MetallicRealother
GeometricBoundN ⊳ ApproxReal
construction
verifiedapproxℝcubical_agda/Corridor/Running/General/ApproxReal.agda:82open import cubical_agda.Corridor.Running.General.ApproxRealgen
DedekindReal ⊳ ApproxReal
construction
verifiedapproxℝcubical_agda/Corridor/Running/General/ApproxReal.agda:82open import cubical_agda.Corridor.Running.General.ApproxRealgen
RealApprox ⊳ ApproxReal
construction
verifiedapproxℝcubical_agda/Corridor/Running/General/ApproxReal.agda:82open import cubical_agda.Corridor.Running.General.ApproxRealgen
Bracket ⊳ ApproxReal
construction
verifiedapproxℝcubical_agda/Corridor/Running/General/ApproxReal.agda:82open import cubical_agda.Corridor.Running.General.ApproxRealgen
GeometricBoundQ ⊳ ApproxReal
construction
verifiedapproxℝcubical_agda/Corridor/Running/General/ApproxReal.agda:82open import cubical_agda.Corridor.Running.General.ApproxRealgen
GeometricVanish ⊳ ApproxReal
construction
verifiedapproxℝcubical_agda/Corridor/Running/General/ApproxReal.agda:82open import cubical_agda.Corridor.Running.General.ApproxRealgen
CertifiedSqrt ⊳ OperatorNormMagnitude
construction
verifiedcstarBracketAbscubical_agda/Corridor/Running/General/OperatorNormMagnitude.agda:33open import cubical_agda.Corridor.Running.General.OperatorNormMagnitudeother
SpectralEdge ⊳ OperatorNormMagnitude
construction
verifiedcstarBracketAbscubical_agda/Corridor/Running/General/OperatorNormMagnitude.agda:33open import cubical_agda.Corridor.Running.General.OperatorNormMagnitudeother
OperatorNorm ⊳ OperatorNormMagnitude
construction
verifiedcstarBracketAbscubical_agda/Corridor/Running/General/OperatorNormMagnitude.agda:33open import cubical_agda.Corridor.Running.General.OperatorNormMagnitudeother
OperatorNormSpectral ⊳ OperatorNormMagnitude
construction
verifiedcstarBracketAbscubical_agda/Corridor/Running/General/OperatorNormMagnitude.agda:33open import cubical_agda.Corridor.Running.General.OperatorNormMagnitudeother
DiagonalCStar ⊳ OperatorNormMagnitude
construction
verifiedcstarBracketAbscubical_agda/Corridor/Running/General/OperatorNormMagnitude.agda:33open import cubical_agda.Corridor.Running.General.OperatorNormMagnitudeother
DiagonalCStar ⊳ PDTest2
construction
verifiedpd-forwardcubical_agda/Corridor/Running/General/PDTest2.agda:156open import cubical_agda.Corridor.Running.General.PDTest2other
AdjointFormN ⊳ SpecNormCut
construction
verifiednotNormUp-lowcubical_agda/Corridor/Running/General/SpecNormCut.agda:41open import cubical_agda.Corridor.Running.General.SpecNormCutother
CStarRay ⊳ SpecNormCut
construction
verifiednotNormUp-lowcubical_agda/Corridor/Running/General/SpecNormCut.agda:41open import cubical_agda.Corridor.Running.General.SpecNormCutother
QuadBound ⊳ SpecNormCut
construction
verifiednotNormUp-lowcubical_agda/Corridor/Running/General/SpecNormCut.agda:41open import cubical_agda.Corridor.Running.General.SpecNormCutother
SpecBracket ⊳ SpecNormCut
construction
verifiednotNormUp-lowcubical_agda/Corridor/Running/General/SpecNormCut.agda:41open import cubical_agda.Corridor.Running.General.SpecNormCutother
Cofinal ⊳ FrontierCapstone
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
MetallicReal ⊳ FrontierCapstone
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
SpecRadiusReal ⊳ FrontierCapstone
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
SpecRadiusFaithful ⊳ FrontierCapstone
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
OperatorNormReal ⊳ FrontierCapstone
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
SqrtRealR ⊳ FrontierCapstone
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
SpectralEdgeReal ⊳ FrontierCapstone
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
CorridorObservables ⊳ FrontierCapstone
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
AffineReal ⊳ FrontierCapstone
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
ZPhiReal ⊳ FrontierCapstone
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
ApproxReal ⊳ FrontierCapstone
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
AddReal ⊳ FrontierCapstone
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
ZPhiSpectralEdge ⊳ FrontierCapstone
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
ZPhiMatrix ⊳ FrontierCapstone
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
ZPhiOperatorNorm ⊳ FrontierCapstone
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
DedekindReal ⊳ ZPhiSpectralEdge
construction
verifiedzphiSpecEdgecubical_agda/Corridor/Running/General/ZPhiSpectralEdge.agda:40open import cubical_agda.Corridor.Running.General.ZPhiSpectralEdgeeq
SqrtRealR ⊳ ZPhiSpectralEdge
construction
verifiedzphiSpecEdgecubical_agda/Corridor/Running/General/ZPhiSpectralEdge.agda:40open import cubical_agda.Corridor.Running.General.ZPhiSpectralEdgeeq
AffineReal ⊳ ZPhiSpectralEdge
construction
verifiedzphiSpecEdgecubical_agda/Corridor/Running/General/ZPhiSpectralEdge.agda:40open import cubical_agda.Corridor.Running.General.ZPhiSpectralEdgeeq
AddReal ⊳ ZPhiSpectralEdge
construction
verifiedzphiSpecEdgecubical_agda/Corridor/Running/General/ZPhiSpectralEdge.agda:40open import cubical_agda.Corridor.Running.General.ZPhiSpectralEdgeeq
ZPhiReal ⊳ ZPhiSpectralEdge
construction
verifiedzphiSpecEdgecubical_agda/Corridor/Running/General/ZPhiSpectralEdge.agda:40open import cubical_agda.Corridor.Running.General.ZPhiSpectralEdgeeq
DedekindReal ⊳ SpecRadiusReal
construction
verifiedloccubical_agda/RealCohesion/DedekindReal.agda:165open import cubical_agda.RealCohesion.DedekindRealeq
AdjointFormN ⊳ SpecRadiusReal
construction
verifiedloccubical_agda/RealCohesion/DedekindReal.agda:165open import cubical_agda.RealCohesion.DedekindRealeq
QuadBound ⊳ SpecRadiusReal
construction
verifiedloccubical_agda/RealCohesion/DedekindReal.agda:165open import cubical_agda.RealCohesion.DedekindRealeq
QpowMono ⊳ SpecRadiusReal
construction
verifiedloccubical_agda/RealCohesion/DedekindReal.agda:165open import cubical_agda.RealCohesion.DedekindRealeq
PowerScaffold ⊳ SpecRadiusReal
construction
verifiedloccubical_agda/RealCohesion/DedekindReal.agda:165open import cubical_agda.RealCohesion.DedekindRealeq
SpecCutDisjoint ⊳ SpecRadiusReal
construction
verifiedloccubical_agda/RealCohesion/DedekindReal.agda:165open import cubical_agda.RealCohesion.DedekindRealeq
SpecLocated ⊳ SpecRadiusReal
construction
verifiedloccubical_agda/RealCohesion/DedekindReal.agda:165open import cubical_agda.RealCohesion.DedekindRealeq
DiagonalCStar ⊳ AbsLemmas
construction
verifiedabs-trianglecubical_agda/Corridor/Running/General/AbsLemmas.agda:57open import cubical_agda.Corridor.Running.General.AbsLemmasother
QuadLemmas ⊳ AbsLemmas
construction
verifiedabs-trianglecubical_agda/Corridor/Running/General/AbsLemmas.agda:57open import cubical_agda.Corridor.Running.General.AbsLemmasother
QuadBound ⊳ AbsLemmas
construction
verifiedabs-trianglecubical_agda/Corridor/Running/General/AbsLemmas.agda:57open import cubical_agda.Corridor.Running.General.AbsLemmasother
DiagonalCStar ⊳ OneNormSubmult
construction
verifiedoneNorm-submultcubical_agda/Corridor/Running/General/OneNormSubmult.agda:96open import cubical_agda.Corridor.Running.General.OneNormSubmultother
GramPosDef ⊳ OneNormSubmult
construction
verifiedoneNorm-submultcubical_agda/Corridor/Running/General/OneNormSubmult.agda:96open import cubical_agda.Corridor.Running.General.OneNormSubmultother
QuadLemmas ⊳ OneNormSubmult
construction
verifiedoneNorm-submultcubical_agda/Corridor/Running/General/OneNormSubmult.agda:96open import cubical_agda.Corridor.Running.General.OneNormSubmultother
QuadBound ⊳ OneNormSubmult
construction
verifiedoneNorm-submultcubical_agda/Corridor/Running/General/OneNormSubmult.agda:96open import cubical_agda.Corridor.Running.General.OneNormSubmultother
SumOrder ⊳ OneNormSubmult
construction
verifiedoneNorm-submultcubical_agda/Corridor/Running/General/OneNormSubmult.agda:96open import cubical_agda.Corridor.Running.General.OneNormSubmultother
AbsLemmas ⊳ OneNormSubmult
construction
verifiedoneNorm-submultcubical_agda/Corridor/Running/General/OneNormSubmult.agda:96open import cubical_agda.Corridor.Running.General.OneNormSubmultother
DedekindReal ⊳ AddReal
construction
verifiedaddℝcubical_agda/Corridor/Running/General/AddReal.agda:148open import cubical_agda.Corridor.Running.General.AddRealother
ApproxReal ⊳ AddReal
construction
verifiedaddℝcubical_agda/Corridor/Running/General/AddReal.agda:148open import cubical_agda.Corridor.Running.General.AddRealother
DiagonalCStar ⊳ SquareRefine
construction
verifiedsquare-refinecubical_agda/Corridor/Running/General/SquareRefine.agda:61open import cubical_agda.Corridor.Running.General.SquareRefineother
AdjointFormN ⊳ SquareRefine
construction
verifiedsquare-refinecubical_agda/Corridor/Running/General/SquareRefine.agda:61open import cubical_agda.Corridor.Running.General.SquareRefineother
GramPosDef ⊳ SquareRefine
construction
verifiedsquare-refinecubical_agda/Corridor/Running/General/SquareRefine.agda:61open import cubical_agda.Corridor.Running.General.SquareRefineother
CauchySchwarz ⊳ SquareRefine
construction
verifiedsquare-refinecubical_agda/Corridor/Running/General/SquareRefine.agda:61open import cubical_agda.Corridor.Running.General.SquareRefineother
SpecBracket ⊳ SquareRefine
construction
verifiedsquare-refinecubical_agda/Corridor/Running/General/SquareRefine.agda:61open import cubical_agda.Corridor.Running.General.SquareRefineother
DedekindReal ⊳ Cofinal
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
GoldenCut ⊳ Cofinal
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
Bracket ⊳ Cofinal
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
Forcing ⊳ Cofinal
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
LocatedLaw ⊳ Cofinal
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
CrossCut ⊳ Cofinal
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
Archimedean ⊳ Cofinal
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
GeometricBoundQ ⊳ Cofinal
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
GapBound ⊳ Cofinal
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
QuadSqueeze ⊳ Cofinal
construction
verifiedrunning≅dedekindcubical_agda/Corridor/Running/General/Cofinal.agda:196open import cubical_agda.Corridor.Running.General.Cofinalgen
LocatedReal ⊳ LocatedEq
construction
verified≈-symcubical_agda/Corridor/Running/General/LocatedEq.agda:63open import cubical_agda.Corridor.Running.General.LocatedEqother
DiagonalCStar ⊳ CStarLocated
construction
verifiedfm2cubical_agda/Corridor/Running/General/CStarLocated.agda:163open import cubical_agda.Corridor.Running.General.CStarLocatedeq
DiagonalCStar ⊳ PowerMonotone
construction
verifiedentry≤oneNormcubical_agda/Corridor/Running/General/PowerMonotone.agda:50open import cubical_agda.Corridor.Running.General.PowerMonotoneother
GramPosDef ⊳ PowerMonotone
construction
verifiedentry≤oneNormcubical_agda/Corridor/Running/General/PowerMonotone.agda:50open import cubical_agda.Corridor.Running.General.PowerMonotoneother
QuadLemmas ⊳ PowerMonotone
construction
verifiedentry≤oneNormcubical_agda/Corridor/Running/General/PowerMonotone.agda:50open import cubical_agda.Corridor.Running.General.PowerMonotoneother
QuadBound ⊳ PowerMonotone
construction
verifiedentry≤oneNormcubical_agda/Corridor/Running/General/PowerMonotone.agda:50open import cubical_agda.Corridor.Running.General.PowerMonotoneother
DedekindReal ⊳ ZPhiReal
construction
verifiedzphiRealcubical_agda/Corridor/Running/General/ZPhiReal.agda:86open import cubical_agda.Corridor.Running.General.ZPhiRealother
GoldenCut ⊳ ZPhiReal
construction
verifiedzphiRealcubical_agda/Corridor/Running/General/ZPhiReal.agda:86open import cubical_agda.Corridor.Running.General.ZPhiRealother
AffineReal ⊳ ZPhiReal
construction
verifiedzphiRealcubical_agda/Corridor/Running/General/ZPhiReal.agda:86open import cubical_agda.Corridor.Running.General.ZPhiRealother
Cassini ⊳ Metallic
construction
verified_cubical_agda/Corridor/Running/Cassini.agda:67open import cubical_agda.Corridor.Running.Cassinieq
DiagonalCStar ⊳ CauchySchwarz
construction
verifiedcauchy-schwarzcubical_agda/Corridor/Running/General/CauchySchwarz.agda:97open import cubical_agda.Corridor.Running.General.CauchySchwarzother
GramPosDef ⊳ CauchySchwarz
construction
verifiedcauchy-schwarzcubical_agda/Corridor/Running/General/CauchySchwarz.agda:97open import cubical_agda.Corridor.Running.General.CauchySchwarzother
DedekindReal ⊳ ReparamReal
construction
verifiedloccubical_agda/RealCohesion/DedekindReal.agda:165open import cubical_agda.RealCohesion.DedekindRealeq
DiagonalCStar ⊳ PowerScaffold
construction
verifiednormUp-from-powcubical_agda/Corridor/Running/General/PowerScaffold.agda:69open import cubical_agda.Corridor.Running.General.PowerScaffoldother
AdjointFormN ⊳ PowerScaffold
construction
verifiednormUp-from-powcubical_agda/Corridor/Running/General/PowerScaffold.agda:69open import cubical_agda.Corridor.Running.General.PowerScaffoldother
GramPosDef ⊳ PowerScaffold
construction
verifiednormUp-from-powcubical_agda/Corridor/Running/General/PowerScaffold.agda:69open import cubical_agda.Corridor.Running.General.PowerScaffoldother
CStarRay ⊳ PowerScaffold
construction
verifiednormUp-from-powcubical_agda/Corridor/Running/General/PowerScaffold.agda:69open import cubical_agda.Corridor.Running.General.PowerScaffoldother
SquareRefine ⊳ PowerScaffold
construction
verifiednormUp-from-powcubical_agda/Corridor/Running/General/PowerScaffold.agda:69open import cubical_agda.Corridor.Running.General.PowerScaffoldother
QuadBound ⊳ PowerScaffold
construction
verifiednormUp-from-powcubical_agda/Corridor/Running/General/PowerScaffold.agda:69open import cubical_agda.Corridor.Running.General.PowerScaffoldother
SpecBracket ⊳ PowerScaffold
construction
verifiednormUp-from-powcubical_agda/Corridor/Running/General/PowerScaffold.agda:69open import cubical_agda.Corridor.Running.General.PowerScaffoldother
DiagonalCStar ⊳ QuadBound
construction
verifiedquadBoundcubical_agda/Corridor/Running/General/QuadBound.agda:99open import cubical_agda.Corridor.Running.General.QuadBoundother
GramPosDef ⊳ QuadBound
construction
verifiedquadBoundcubical_agda/Corridor/Running/General/QuadBound.agda:99open import cubical_agda.Corridor.Running.General.QuadBoundother
QuadLemmas ⊳ QuadBound
construction
verifiedquadBoundcubical_agda/Corridor/Running/General/QuadBound.agda:99open import cubical_agda.Corridor.Running.General.QuadBoundother
SumOrder ⊳ QuadBound
construction
verifiedquadBoundcubical_agda/Corridor/Running/General/QuadBound.agda:99open import cubical_agda.Corridor.Running.General.QuadBoundother
DedekindReal ⊳ OperatorNormReal
construction
verifiedᵀᵀcubical_agda/Corridor/Running/General/OperatorNormReal.agda:35open import cubical_agda.Corridor.Running.General.OperatorNormRealeq
AdjointFormN ⊳ OperatorNormReal
construction
verifiedᵀᵀcubical_agda/Corridor/Running/General/OperatorNormReal.agda:35open import cubical_agda.Corridor.Running.General.OperatorNormRealeq
QuadBound ⊳ OperatorNormReal
construction
verifiedᵀᵀcubical_agda/Corridor/Running/General/OperatorNormReal.agda:35open import cubical_agda.Corridor.Running.General.OperatorNormRealeq
SpecCutDisjoint ⊳ OperatorNormReal
construction
verifiedᵀᵀcubical_agda/Corridor/Running/General/OperatorNormReal.agda:35open import cubical_agda.Corridor.Running.General.OperatorNormRealeq
SpecRadiusReal ⊳ OperatorNormReal
construction
verifiedᵀᵀcubical_agda/Corridor/Running/General/OperatorNormReal.agda:35open import cubical_agda.Corridor.Running.General.OperatorNormRealeq
SqrtRealR ⊳ OperatorNormReal
construction
verifiedᵀᵀcubical_agda/Corridor/Running/General/OperatorNormReal.agda:35open import cubical_agda.Corridor.Running.General.OperatorNormRealeq
DiagonalCStar ⊳ GeomGrow
construction
verifiedberncubical_agda/Corridor/Running/General/GeomGrow.agda:55open import cubical_agda.Corridor.Running.General.GeomGrowother
DedekindReal ⊳ GeomGrow
construction
verifiedberncubical_agda/Corridor/Running/General/GeomGrow.agda:55open import cubical_agda.Corridor.Running.General.GeomGrowother
PowerScaffold ⊳ GeomGrow
construction
verifiedberncubical_agda/Corridor/Running/General/GeomGrow.agda:55open import cubical_agda.Corridor.Running.General.GeomGrowother
CertifiedSqrt ⊳ OperatorNormSpectral
construction
verifiedcstarBracketcubical_agda/Corridor/Running/General/OperatorNormSpectral.agda:35open import cubical_agda.Corridor.Running.General.OperatorNormSpectralother
SpectralEdge ⊳ OperatorNormSpectral
construction
verifiedcstarBracketcubical_agda/Corridor/Running/General/OperatorNormSpectral.agda:35open import cubical_agda.Corridor.Running.General.OperatorNormSpectralother
OperatorNorm ⊳ OperatorNormSpectral
construction
verifiedcstarBracketcubical_agda/Corridor/Running/General/OperatorNormSpectral.agda:35open import cubical_agda.Corridor.Running.General.OperatorNormSpectralother
DedekindReal ⊳ SpectralEdgeReal
construction
verifiedspecEdgecubical_agda/Corridor/Running/General/SpectralEdgeReal.agda:94open import cubical_agda.Corridor.Running.General.SpectralEdgeRealeq
DiagonalCStar ⊳ SpectralEdgeReal
construction
verifiedspecEdgecubical_agda/Corridor/Running/General/SpectralEdgeReal.agda:94open import cubical_agda.Corridor.Running.General.SpectralEdgeRealeq
SqrtReal ⊳ SpectralEdgeReal
construction
verifiedspecEdgecubical_agda/Corridor/Running/General/SpectralEdgeReal.agda:94open import cubical_agda.Corridor.Running.General.SpectralEdgeRealeq
ReparamReal ⊳ SpectralEdgeReal
construction
verifiedspecEdgecubical_agda/Corridor/Running/General/SpectralEdgeReal.agda:94open import cubical_agda.Corridor.Running.General.SpectralEdgeRealeq
DedekindReal ⊳ AffineReal
construction
verifiedaffineℝcubical_agda/Corridor/Running/General/AffineReal.agda:82open import cubical_agda.Corridor.Running.General.AffineRealeq
ReparamReal ⊳ AffineReal
construction
verifiedaffineℝcubical_agda/Corridor/Running/General/AffineReal.agda:82open import cubical_agda.Corridor.Running.General.AffineRealeq
DiagonalCStar ⊳ SpectralCStar
construction
verifiedspectral2-cstarcubical_agda/Corridor/Running/General/SpectralCStar.agda:48open import cubical_agda.Corridor.Running.General.SpectralCStareq
OperatorNorm ⊳ SpectralCStar
construction
verifiedspectral2-cstarcubical_agda/Corridor/Running/General/SpectralCStar.agda:48open import cubical_agda.Corridor.Running.General.SpectralCStareq
DedekindReal ⊳ GeomBeat
construction
verifiedgeom-beatcubical_agda/Corridor/Running/General/GeomBeat.agda:61open import cubical_agda.Corridor.Running.General.GeomBeatgen
PowerScaffold ⊳ GeomBeat
construction
verifiedgeom-beatcubical_agda/Corridor/Running/General/GeomBeat.agda:61open import cubical_agda.Corridor.Running.General.GeomBeatgen
GeomGrowArch ⊳ GeomBeat
construction
verifiedgeom-beatcubical_agda/Corridor/Running/General/GeomBeat.agda:61open import cubical_agda.Corridor.Running.General.GeomBeatgen
AdjointFormN ⊳ SpecRadiusFaithful
construction
verifiedU-soundcubical_agda/Corridor/Running/General/SpecRadiusFaithful.agda:31open import cubical_agda.Corridor.Running.General.SpecRadiusFaithfulother
CStarRay ⊳ SpecRadiusFaithful
construction
verifiedU-soundcubical_agda/Corridor/Running/General/SpecRadiusFaithful.agda:31open import cubical_agda.Corridor.Running.General.SpecRadiusFaithfulother
SpecCutDisjoint ⊳ SpecRadiusFaithful
construction
verifiedU-soundcubical_agda/Corridor/Running/General/SpecRadiusFaithful.agda:31open import cubical_agda.Corridor.Running.General.SpecRadiusFaithfulother
PowerScaffold ⊳ SpecRadiusFaithful
construction
verifiedU-soundcubical_agda/Corridor/Running/General/SpecRadiusFaithful.agda:31open import cubical_agda.Corridor.Running.General.SpecRadiusFaithfulother
SpecLocated ⊳ SpecRadiusFaithful
construction
verifiedU-soundcubical_agda/Corridor/Running/General/SpecRadiusFaithful.agda:31open import cubical_agda.Corridor.Running.General.SpecRadiusFaithfulother
BridgePrelude ⊳ InvolutionBorrow
construction
verifiedborrowed-suc-transport-negcubical_agda/HottLane/InvolutionBorrow.agda:74open import cubical_agda.HottLane.InvolutionBorroweq
IsoToEquiv ⊳ InvolutionBorrow
construction
verifiedborrowed-suc-transport-negcubical_agda/HottLane/InvolutionBorrow.agda:74open import cubical_agda.HottLane.InvolutionBorroweq
Building from this atlas. Each verified node/edge lists the file:line of its proof (click to open) and the import line to bring the handle into scope. To extend: prove the theorem a vacancy edge names (a generative theorem that the target is forced as a byproduct of the source), add a node/edge to the ledger binding it, and re-run certify_atlas.py --strict-forcing --layout forcing. The verdict is bound to the evidence digest above — re-running on the live tree re-certifies.