Framing is exactly existence of both pseudo connection pairs

Open

QAlgorithms.Papers.Independent.Intakethird100.P60.framed_iff_pseudo_connection_pairs

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $\mathbb D$ be a pseudo double category. A pseudo connection pair is a choice, for every vertical arrow, of a companion with its two cells and its two identities. A pseudo op-connection pair is the corresponding choice of conjoints. Then

\mathbb D\text{ is framed} \quad\Longleftrightarrow\quad \mathbb D\text{ admits a pseudo connection pair and a pseudo op-connection pair}.

The horizontal composition need not be strict, and no split cleavage or strict connection axiom is imposed. Both choices are part of the conclusion.

This packages the nonalgebraic existence characterization as chosen pseudo connection data.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P60

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P60

open CategoryTheory

universe u v w x

/-- Appendix A pseudo connection-pair characterization (PDF p. 72).
These are arbitrary choices in a pseudo double category, not strict connections. -/
theorem framed_iff_pseudo_connection_pairs {V : Type u} [Category.{v} V]
    (D : DoubleData.{u,v,w,x} V) (hD : DoubleCoherence D) :
    IsFramed D ↔ Nonempty (PseudoConnectionPair D) ∧ Nonempty (PseudoOpConnectionPair D) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P60

Source

Framed bicategories and monoidal fibrations, arXiv:0706.1286v2, PDF p. 72, AppendixA: pseudo connection-pair characterization

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $V$ be any category and $D$ any of the specified double data, with arbitrary universe sizes. Write $H(A,B)$ for horizontal-arrow types and $C_{f,g}(M,N)$ for squares, where $M\in H(A,B)$ , $N\in H(C,E)$ , $f:A\to C$ , and $g:B\to E$ . Write $U_A$ for horizontal units, $MN$ for horizontal products, $1_M$ for identity squares, $U_f$ for squares on horizontal units, $s;t$ for vertical composition in that order, and $s\otimes t$ for horizontal square composition; for identity-boundary squares, simplify composites of identity morphisms in $s;t$ . Write $\alpha_{M,N,P}:(MN)P\to M(NP)$ , its specified reverse $\bar\alpha_{M,N,P}$ , and $\lambda_M:U_AM\to M$ , $\bar\lambda_M:M\to U_AM$ , $\rho_M:MU_B\to M$ , $\bar\rho_M:M\to MU_B$ for the specified squares with identity vertical boundaries. Assume the supplied coherence proof: universally over all well-typed configurations,

\begin{gathered} (a;b);c\doteq a;(b;c),\qquad 1_M;a\doteq a,\qquad a;1_N\doteq a,\\ U_{1_A}=1_{U_A},\qquad U_{g\circ f}=U_f;U_g,\qquad 1_M\otimes1_N=1_{MN},\\ (a\otimes b);(c\otimes d)=(a;c)\otimes(b;d),\\ \alpha_{M,N,P};\bar\alpha_{M,N,P}=1_{(MN)P},\qquad \bar\alpha_{M,N,P};\alpha_{M,N,P}=1_{M(NP)},\\ \lambda_M;\bar\lambda_M=1_{U_AM},\qquad \bar\lambda_M;\lambda_M=1_M,\qquad \rho_M;\bar\rho_M=1_{MU_B},\qquad \bar\rho_M;\rho_M=1_M,\\ ((a\otimes b)\otimes c);\alpha_{Q,R,S} \doteq\alpha_{M,N,P};(a\otimes(b\otimes c)),\\ (U_f\otimes a);\lambda_N\doteq\lambda_M;a,\qquad (a\otimes U_g);\rho_N\doteq\rho_M;a,\\ \bigl((\alpha_{M,N,P}\otimes1_Q);\alpha_{M,NP,Q}\bigr); (1_M\otimes\alpha_{N,P,Q}) =\alpha_{MN,P,Q};\alpha_{M,N,PQ},\\ \alpha_{M,U_B,N};(1_M\otimes\lambda_N) =\rho_M\otimes1_N. \end{gathered}

Here $\doteq$ means heterogeneous equality; in associativity naturality, $a:M\to Q$ , $b:N\to R$ , $c:P\to S$ have matching adjoining vertical boundaries, and in unit naturality $a:M\to N$ has boundaries $f,g$ . The theorem asserts that the following unique-factorization condition is equivalent to the conjunction of the existence of the two assignment structures described below: for every $A,B,C,E$ , $f:A\to C$ , $g:B\to E$ , and $N\in H(C,E)$ , there exist $M\in H(A,B)$ and $a\in C_{f,g}(M,N)$ such that, for every $P,Q$ , $h:P\to A$ , $k:Q\to B$ , $T\in H(P,Q)$ , and $b\in C_{f\circ h,g\circ k}(T,N)$ , there exists exactly one $c\in C_{h,k}(T,M)$ with $c;a=b$ . The first assignment structure chooses, for every $A,B$ and $f:A\to B$ , a horizontal arrow $F_f\in H(A,B)$ , squares

u_f\in C_{1_A,f}(U_A,F_f),\qquad e_f\in C_{f,1_B}(F_f,U_B),

and proofs that

u_f;e_f\doteq U_f,\qquad (\bar\lambda_{F_f};(u_f\otimes e_f));\rho_{F_f}=1_{F_f}.

The second assignment structure chooses, for every $A,B$ and $f:A\to B$ , a horizontal arrow $G_f\in H(B,A)$ , squares

v_f\in C_{f,1_A}(U_A,G_f),\qquad d_f\in C_{1_B,f}(G_f,U_B),

and proofs that

v_f;d_f\doteq U_f,\qquad (\bar\rho_{G_f};(d_f\otimes v_f));\lambda_{G_f}=1_{G_f}.

Existence of each complete assignment structure is asserted, without a uniqueness claim. Every morphism, including identities, is covered. The category may be empty, making the indexed requirements vacuous; a test square type containing no $b$ imposes no factorization requirement.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph